Theorem: Smt.Reconstruct.Arith.castNeg (Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ a < 0, a < 0
Tactic:
intros a h
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a < 0
⊢ a < 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a < 0
⊢ a < 0
Tactic:
simp [h]
State after:
no goals