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

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

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