α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)

case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)
suffices : ∀ᶠ x : ℂ × ℂ in 𝓝 p, x.1 ≠ 0
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)

case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen fun x => x.fst = 0 → False
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
refine' IsOpen.eventually_mem _ hp_fst
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen ({x | x.fst = 0}ᶜ)
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen fun x => x.fst = 0 → False
change IsOpen ({ x : ℂ × ℂ | x.1 = 0 }ᶜ)
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsClosed {x | x.fst = 0}
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen ({x | x.fst = 0}ᶜ)
rw [isOpen_compl_iff]
no goals
case this
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsClosed {x | x.fst = 0}
exact isClosed_eq continuous_fst continuous_const
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ x.fst ^ x.snd = Complex.exp (Complex.log x.fst * x.snd)
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => Complex.exp (Complex.log x.fst * x.snd)) x
dsimp only
no goals
α : Type ?u.99046
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ x.fst ^ x.snd = Complex.exp (Complex.log x.fst * x.snd)
rw [cpow_def_of_ne_zero hx]