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

State before:
a b b' : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
x✝ : b ^ e₂ = b'
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b'
Tactic:
subst_vars
State after:
a b : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b ^ e₂

State before:
a b : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b ^ e₂
Tactic:
rw [mul_rpow (rpow_pos_of_pos ha e₁).le hb.le, rpow_mul ha.le]
State after:
no goals