Lean4
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version autogenerates `min` and `max` fields. See `LinearOrder.lift`
for a version that takes `[Max α]` and `[Min α]`, then uses them as `max` and `min`. See
`LinearOrder.liftWithOrd'` for a version which does not auto-generate `compare` fields.
See note [reducible non-instances]. -/
abbrev lift' [LinearOrder β] (f : α → β) (inj : Injective f) : LinearOrder α :=
@LinearOrder.lift α β _ ⟨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
