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

State before:
x a₂ b₂ c ea eb : ℝ
h : 0 < x
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * c
Tactic:
subst_vars
State after:
x a₂ b₂ ea eb : ℝ
h : 0 < x
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)

State before:
x a₂ b₂ ea eb : ℝ
h : 0 < x
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
Tactic:
rw [rpow_add h, mul_mul_mul_comm]
State after:
no goals