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. It also takes `[Ord α]` as an argument and uses them for `compare`
fields. See `LinearOrder.lift` for a version that autogenerates `compare` fields, and
`LinearOrder.liftWithOrd'` for one that auto-generates `min` and `max` fields.
fields. See note [reducible non-instances]. -/
abbrev liftWithOrd [LinearOrder β] [Max α] [Min α] [Ord α] (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))
(compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
letI _instLE : LE α := ⟨fun a b ↦ f a ≤ f b⟩
letI _instLE : LT α := ⟨fun a b ↦ 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 _ _ => (compare_f _ _).symm)
