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

State before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
⊢ a = b
Tactic:
have tr := Int.lt_trichotomy a b
State after:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b

State before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂)
State after:
no goals