α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
no goals
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
split_ifs <;> simp only [*, lt_irrefl]