x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else exp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y))⁻¹
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
simp only [rpow_def_of_nonneg hx]
no goals
x✝ y✝ z x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else exp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y))⁻¹
split_ifs <;> simp_all [exp_neg]