α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.exp (Complex.log x.fst * x.snd)) p
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
rw [continuousAt_congr (cpow_eq_nhds' hp_fst_ne_zero)]
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.log x.fst * x.snd) p
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.exp (Complex.log x.fst * x.snd)) p
refine' continuous_exp.continuousAt.comp _
no goals
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.log x.fst * x.snd) p
exact
  ContinuousAt.mul
    (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
    continuous_snd.continuousAt
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
α : Type ?u.293132
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
intro h
case inr
α : Type ?u.293132
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0.im ≠ 0
⊢ False
case inr
α : Type ?u.293132
p : ℂ × ℂ
h : p.fst = 0
hp_fst : p.fst.im ≠ 0
⊢ False
rw [h] at hp_fst
no goals
case inr
α : Type ?u.293132
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0.im ≠ 0
⊢ False
simp at hp_fst