Lean4
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version auto-generates `min` and `max` 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 doesn't auto-generate
`min` and `max` fields. fields. See note [reducible non-instances]. -/
abbrev liftWithOrd' [LinearOrder β] [Ord α] (f : α → β) (inj : Injective f)
(compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
@LinearOrder.liftWithOrd α β _ ⟨fun x y ↦ if f x ≤ f y then y else x⟩ ⟨fun x y ↦ if f x ≤ f y then x else y⟩ _ f inj
(fun _ _ ↦ (apply_ite f _ _ _).trans (max_def _ _).symm) (fun _ _ ↦ (apply_ite f _ _ _).trans (min_def _ _).symm)
compare_f
