Theorem: Smt.Reconstruct.Int.arith_mul_pos_eq (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
⊢ c > 0 ∧ a = b → c * a = c * b
Tactic:
intros h
State after:
a b c d : Int
h : c > 0 ∧ a = b
⊢ c * a = c * b

State before:
a b c d : Int
h : c > 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
State after:
no goals