rw [← Real.rpow_natCast]
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ 3 = x✝.log ^ 3
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ ↑3 = x✝.log ^ 3