x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ abs (x ^ y) = abs x ^ y
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ abs (x ^ y) = abs x ^ y
have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg_of_nonneg hx_nonneg _
no goals
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ abs (x ^ y) = abs x ^ y
rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]