feat: pushing Lattice and predecessors through Equiv (leanprover-community#37605)

The point is to transfer as cheaply as possible instances over to type synonyms. Note that we already have these for most of the algebraic hierarchy even when they "generalise" from an equiv to a structure-preserving injective function (note that the equiv needn't be structure-preserving, precisely because said structure needn't exist already).

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib/Logic/Equiv/Defs.lean

@@ -896,6 +896,7 @@ def finTwoEquiv : Fin 2 ≃ Bool where
   right_inv b := by grind
 
 namespace Equiv
+
 variable {α β : Type*}
 
 /-- The left summand of `α ⊕ β` is equivalent to `α`. -/
@@ -912,4 +913,46 @@ def sumIsRight : {x : α ⊕ β // x.isRight} ≃ β where
   invFun b := ⟨.inr b, Sum.isRight_inr⟩
   left_inv | ⟨.inr _b, _⟩ => rfl
 
+variable (e : α ≃ β)
+
+/-- Transfer `LE` across an `Equiv`. -/
+protected abbrev le [LE β] : LE α where
+  le a b := e a ≤ e b
+
+lemma le_def [LE β] (a b : α) :
+    letI := e.le
+    e a ≤ e b ↔ a ≤ b := Iff.rfl
+
+/-- Transfer `LT` across an `Equiv`. -/
+protected abbrev lt [LT β] : LT α where
+  lt a b := e a < e b
+
+lemma lt_def [LT β] (a b : α) :
+    letI := e.lt
+    e a < e b ↔ a < b := Iff.rfl
+
+/-- Transfer `Max` across an `Equiv`. -/
+protected abbrev max [Max β] : Max α where
+  max a b := e.symm (max (e a) (e b))
+
+lemma max_def [Max β] (a b : α) :
+    letI := e.max
+    max a b = e.symm (max (e a) (e b)) := rfl
+
+/-- Transfer `Min` across an `Equiv`. -/
+protected abbrev min [Min β] : Min α where
+  min a b := e.symm (min (e a) (e b))
+
+lemma min_def [Min β] (a b : α) :
+    letI := e.min
+    min a b = e.symm (min (e a) (e b)) := rfl
+
+/-- Transfer `Ord` across an `Equiv`. -/
+protected abbrev ord [Ord β] : Ord α where
+  compare a b := compare (e a) (e b)
+
+lemma ord_def [Ord β] (a b : α) :
+    letI := e.ord
+    compare a b = compare (e a) (e b) := rfl
+
 end Equiv

Mathlib/Order/Lattice.lean

@@ -992,6 +992,54 @@ protected abbrev Subtype.distribLattice [DistribLattice α] {P : α → Prop}
   letI := Subtype.lattice Psup Pinf
   Subtype.coe_injective.distribLattice _ coe_le_coe coe_lt_coe (coe_sup Psup) (coe_inf Pinf)
 
+namespace Equiv
+
+variable (e : α ≃ β)
+
+/-- Transfer `Preorder` across an `Equiv`. -/
+protected abbrev preorder [Preorder β] : Preorder α := by
+  let le := e.le
+  let lt := e.lt
+  apply Function.Injective.preorder e <;> intros <;> rfl
+
+/-- Transfer `PartialOrder` across an `Equiv`. -/
+protected abbrev partialOrder [PartialOrder β] : PartialOrder α := by
+  let preorder := e.preorder
+  apply e.injective.partialOrder <;> intros <;> rfl
+
+/-- Transfer `LinearOrder` across an `Equiv`. -/
+protected abbrev linearOrder [LinearOrder β] [DecidableEq α] : LinearOrder α := by
+  let max := e.max
+  let min := e.min
+  let preorder := e.preorder
+  let compare := e.ord
+  apply e.injective.linearOrder <;> intros <;> first | rfl | exact e.apply_symm_apply _
+
+/-- Transfer `SemilatticeSup` across an `Equiv`. -/
+protected abbrev semilatticeSup [SemilatticeSup β] : SemilatticeSup α := by
+  let max := e.max
+  let partialOrder := e.partialOrder
+  apply e.injective.semilatticeSup <;> intros <;> first | rfl | exact e.apply_symm_apply _
+
+/-- Transfer `SemilatticeInf` across an `Equiv`. -/
+protected abbrev semilatticeInf [SemilatticeInf β] : SemilatticeInf α := by
+  let min := e.min
+  let partialOrder := e.partialOrder
+  apply e.injective.semilatticeInf <;> intros <;> first | rfl | exact e.apply_symm_apply _
+
+/-- Transfer `Lattice` across an `Equiv`. -/
+protected abbrev lattice [Lattice β] : Lattice α := by
+  let semilatticeSup := e.semilatticeSup
+  let semilatticeInf := e.semilatticeInf
+  apply e.injective.lattice <;> intros <;> first | rfl | exact e.apply_symm_apply _
+
+/-- Transfer `DistribLattice` across an `Equiv`. -/
+protected abbrev distribLattice [DistribLattice β] : DistribLattice α := by
+  let lattice := e.lattice
+  apply e.injective.distribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _
+
+end Equiv
+
 end lift
 
 namespace ULift