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, [1, 2, 0]
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, [1, 2, 0]
State after:
no goals