Theorem: Smt.Reconstruct.Arith.arith_mul_pos_eq (Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ c > 0 ∧ a = b → c * a = c * b
Tactic:
intros h
State after:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c > 0 ∧ a = b
⊢ c * a = c * b

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c > 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
State after:
no goals