α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.gt ↔ a > b
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ 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.gt ↔ a > b
split_ifs <;> simp only [*, lt_irrefl, not_lt_of_gt]
no goals
case inr.inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ a > b
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  exact true_iff_iff.2 h
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b
have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
no goals
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b
exact true_iff_iff.2 h