α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)

case this
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
suffices : ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0
case this
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)

case this
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
no goals
case this
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
exact IsOpen.eventually_mem isOpen_ne ha
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = Complex.exp (Complex.log x * b)
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => x ^ b) x = (fun x => Complex.exp (Complex.log x * b)) x
dsimp only
no goals
α : Type ?u.3016
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = Complex.exp (Complex.log x * b)
rw [cpow_def_of_ne_zero hx]