Commit 2026-09-04 09:44 cb03454a

chore(Order/WithBot): remove defeq between WithBot.LE/LT and WithTop.LE/LT (#42622) This PR removes the defeq between WithBot.LE and WithTop.LE, and between WithBot.LT and WithTop.LT, by making them separate inductive types. This is a follow up to #19668, which turned these into inductive types in the first place. This is a step towards making WithBot and WithTop be not defeq to eachother at all. This is something that the FRO wants (or at least wanted) for their interval arithmetic tactic. A lot of proofs broke that were relying on some higher order unification. In particular these were unification problems of the form a ≤ b =?= c ≤ d such that a =?= c got stuck but unifiying b =?= d and then a =?= c succeeded. These previously succeeded because the ≤ relation could be unfolded, flipping the order of its arguments, allowing b =?= d to be unified before a =?= c. This PR removes that unfolding opportunity, hence making the unification fail. Almost all of these could be fixed by using grw [←], forcing Lean to first unify the RHS b =?= d.