case a
x✝ y✝ z x : ℝ
hx : 0 < x
y : ℝ
⊢ exp (log (x ^ y)) = exp (y * log x)
x✝ y✝ z x : ℝ
hx : 0 < x
y : ℝ
⊢ log (x ^ y) = y * log x
apply exp_injective
no goals
case a
x✝ y✝ z x : ℝ
hx : 0 < x
y : ℝ
⊢ exp (log (x ^ y)) = exp (y * log x)
rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]