x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else exp (log 1 * x)) = 1
x : ℂ
⊢ 1 ^ x = 1
rw [cpow_def]
no goals
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else exp (log 1 * x)) = 1
split_ifs <;> simp_all [one_ne_zero]