Commit 2026-03-06 00:15 d3be269a

feat(to_dual): support recursively reordering arguments (#34863) This PR implements the feature of recursively reordering arguments of arguments in to_dual. All of the material on reorderings has been put in the new file Mathlib.Tactic.Translate.Reorder. Ideally, when tagging a structure with to_dual, it will try to automatically add the correct reorder arguments. But this is only a small quality of life improvement, so I will leave that for a potential future PR. Currently, you have to manually re-tag the projections and constructor if you want them to get a reorder. This PR also improves the trace messages of trace.translate_detail. This PR also adds new error messages for when the given (reorder := ...) is malformed.