Theorem: Smt.Reconstruct.Arith.trichotomy₃ (Smt/Reconstruct/Arith/Trichotomy/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a < b → ¬a > b → a = b
Tactic:
intros h₁ h₂
State after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
⊢ a = b

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
⊢ a = b
Tactic:
have tr := lt_trichotomy a b
State after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
have tr': a < b ∨ b < a ∨ a = b  := by permutateOr tr, [0, 2, 1]
State after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b
Tactic:
exact (orImplies₃ ((orImplies₃ tr') h₁)) h₂
State after:
no goals

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b ∨ b < a ∨ a = b
Tactic:
permutateOr tr, [0, 2, 1]
State after:
no goals