Commit 2026-03-26 18:37 f05773da

feat(OrderDual): fix leaky instances (#37195) This PR fixes the leaky OrderDual instances. It is not necessarily obvious at first that this possible to do. The heuristic for making these changes is as follows:

• Start at the data instances (LE, Max, One) and define them with the data field in eta-expanded form, with the lambda binders matching the type.. For example, the previous verion

instance instSup (α : Type*) [Min α] : Max αᵒᵈ :=
  ⟨((· ⊓ ·) : α → α → α)⟩

was bad, because the lambda binder had type α instead of αᵒᵈ. This would cause unification failures in type class search.

• For structures with child structures, use where notation, and fill in the proof fields manually. This PR removes 25 uses of backward.isDefEq.respectTransparency. We should think about writing a metaprogram that can make these obvious instances for type wrappers/synonyms, which would save us the manual effort. Because in principle, we will have to do the same refactor for Lex, Colex, Additive, Multiplicate and any other such types. In one place a proof broke due to this change, which was caused by stuff unifying in the default transparency before type class synthesis had finished. I fixed by with a by exact, which delays that elaboration/unification.