Commit 2025-12-02 12:55 a2f9dca9

chore(Order/Basic): use @[to_dual] (#31903) This PR uses @[to_dual] in the rest of Mathlib.Order.Basic. I noticed that it was annoying to have to manually specify the reorder argument when it was very obvious what it should be, when using to_dual self. So, I created #31902 to do this automatically. Eq.trans_ge is not what the lemma name would make me think it is. So for now I've left it and similar lemmas without a tag, to avoid unnecessarily creating new lemmas. There are some lemmas like Function.Injective.linearOrder that have a hypothesis of the form ∀ {x y}, f x ≤ f y ↔ x ≤ y. In order to dualize this, we need to swap x and y, but it is not yet possible to reorder arguments of arguments.