Commit 2026-01-29 15:56 54200f1f

feat(Order/ModularLattice): add to_dual annotations (#34247)

Summary

• Register modular lattice classes as duals and add @[to_dual] to applicable theorems/instances.
• Remove several manually-written duals where to_dual now generates them; in some cases this creates new dual declarations.
• All generated declarations are identical to the ones they replace.

New lemmas

• sup_inf_le_assoc_of_le is a projection lemma for IsModularLattice.sup_inf_le_assoc_of_le.
• inf_sup_le_assoc_of_le is the to_dual companion.