Theorem: Smt.Reconstruct.Arith.castEQ (Smt/Reconstruct/Arith/SumBounds/Tactic.lean)

State before:
⊢ ∀ {a b : ℤ}, a = b → ↑a = ↑b
Tactic:
intros a b h
State after:
a b : ℤ
h : a = b
⊢ ↑a = ↑b

State before:
a b : ℤ
h : a = b
⊢ ↑a = ↑b
Tactic:
rw [h]
State after:
no goals