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