case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ↑abs (z ^ w) = ↑abs z ^ w.re / Real.exp (arg z * w.im)
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact abs_cpow_of_ne_zero hz w; rw [map_zero]]
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)

case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
cases' eq_or_ne w.re 0 with hw hw
no goals
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
simp [hw, h rfl hw]
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ↑abs (0 ^ w) = 0 ^ w.re / Real.exp (arg 0 * w.im)
rw [Real.zero_rpow hw, zero_div, zero_cpow, map_zero]
no goals
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0
exact ne_of_apply_ne re hw