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 : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹
simp only [cpow_def, neg_eq_zero, mul_neg]
no goals
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 [exp_neg]