no goals
x : ℝ
hx : 0 < x
y : ℂ
⊢ ↑abs (↑x ^ y) = x ^ y.re
rw [abs_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le,
  MulZeroClass.zero_mul, Real.exp_zero, div_one, abs_of_nonneg hx.le]