Lean4
instance instLinearOrder (α : Type*) [LinearOrder α] : LinearOrder αᵒᵈ
where
__ := inferInstanceAs (PartialOrder αᵒᵈ)
__ := inferInstanceAs (Ord αᵒᵈ)
le_total := fun a b : α ↦ le_total b a
max := fun a b ↦ (min a b : α)
min := fun a b ↦ (max a b : α)
min_def := fun a b ↦ show (max .. : α) = _ by rw [max_comm, max_def]; rfl
max_def := fun a b ↦ show (min .. : α) = _ by rw [min_comm, min_def]; rfl
toDecidableLE := (inferInstance : DecidableRel (fun a b : α ↦ b ≤ a))
toDecidableLT := (inferInstance : DecidableRel (fun a b : α ↦ b < a))
toDecidableEq := (inferInstance : DecidableEq α)
compare_eq_compareOfLessAndEq a
b := by
simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]
rfl
