Theorem: Mathlib.Tactic.RPowRing.mul_pf_left (PrimeNumberTheoremAnd/Tactic/RPowSimp.lean)

State before:
a₂ b c a₁ : ℝ
x✝ : a₂ * b = c
⊢ a₁ * a₂ * b = a₁ * c
Tactic:
subst_vars
State after:
a₂ b a₁ : ℝ
⊢ a₁ * a₂ * b = a₁ * (a₂ * b)

State before:
a₂ b a₁ : ℝ
⊢ a₁ * a₂ * b = a₁ * (a₂ * b)
Tactic:
rw [mul_assoc]
State after:
no goals