Lean4
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version takes `[Max α]` and `[Min α]` as arguments, then uses
them for `max` and `min` fields. See `LinearOrder.lift'` for a version that autogenerates `min` and
`max` fields, and `LinearOrder.liftWithOrd` for one that does not auto-generate `compare`
fields.
See also `Function.Injective.linearOrder` when only the proof fields need to be transferred.
See note [reducible non-instances]. -/
abbrev lift [LinearOrder β] [Max α] [Min α] (f : α → β) (inj : Injective f) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) : LinearOrder α :=
letI _instLE : LE α := ⟨fun a b ↦ f a ≤ f b⟩
letI _instLT : LT α := ⟨fun a b ↦ f a < f b⟩
letI _instOrdα : Ord α := ⟨fun a b ↦ compare (f a) (f b)⟩
letI _decidableLE := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
letI _decidableLT := fun x y ↦ (inferInstance : Decidable (f x < f y))
letI _decidableEq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
inj.linearOrder _ .rfl .rfl hinf hsup (fun _ _ => rfl)
