Lean4
/-- Construct a linear order from an `IsStrictTotalOrder` relation.
See note [reducible non-instances]. -/
abbrev linearOrderOfSTO (r) [IsStrictTotalOrder α r] [DecidableRel r] : LinearOrder α :=
let hD : DecidableRel (fun x y => x = y ∨ r x y) := fun x y =>
decidable_of_iff (¬r y x)
⟨fun h => ((trichotomous_of r y x).resolve_left h).imp Eq.symm id, fun h =>
h.elim (fun h => h ▸ irrefl_of _ _) (asymm_of r)⟩
{ __ := partialOrderOfSO r
le_total := fun x y =>
match y, trichotomous_of r x y with
| _, Or.inl h => Or.inl (Or.inr h)
| _, Or.inr (Or.inl rfl) => Or.inl (Or.inl rfl)
| _, Or.inr (Or.inr h) => Or.inr (Or.inr h),
toMin := minOfLe, toMax := maxOfLe, toDecidableLE := hD }
