case mk
z w : ℂ
h₁ : 0 ≤ (z, w).fst.re ∨ (z, w).fst.im ≠ 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
p : ℂ × ℂ
h₁ : 0 ≤ p.fst.re ∨ p.fst.im ≠ 0
h₂ : 0 < p.snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
cases' p with z w
case mk
z w : ℂ
h₁ : (0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0) ∨ (z, w).fst = 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
case mk
z w : ℂ
h₁ : 0 ≤ (z, w).fst.re ∨ (z, w).fst.im ≠ 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne.def, Classical.not_not,
  not_le_zero_iff] at h₁
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).snd.re
h₁ : 0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)

case mk.inr
w : ℂ
h₂ : 0 < (0, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, w)
case mk
z w : ℂ
h₁ : (0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0) ∨ (z, w).fst = 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
rcases h₁ with (h₁ | (rfl : z = 0))
no goals
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).snd.re
h₁ : 0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)

case mk.inr
w : ℂ
h₂ : 0 < (0, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, w)
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]