α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
case inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b

case inr.inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b
split_ifs <;> simp only []
case inr.inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
case inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b

case inr.inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
case _ h   => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
case inr.inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
case _ _ h => exact true_iff_iff.2 h
no goals
case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
case _ _ h => exact false_iff_iff.2 h
no goals
α : Type u
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b
exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
no goals
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b
exact true_iff_iff.2 h
no goals
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b
exact false_iff_iff.2 h