α : Type ?u.1960
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0

case this
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0
suffices : ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0
case this
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0

case this
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
exact
  this.mono fun x hx => by
    dsimp only
    rw [zero_cpow hx, Pi.zero_apply]
no goals
case this
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
exact IsOpen.eventually_mem isOpen_ne hb
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = OfNat.ofNat 0 x
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => 0 ^ x) x = OfNat.ofNat 0 x
dsimp only
no goals
α : Type ?u.1960
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = OfNat.ofNat 0 x
rw [zero_cpow hx, Pi.zero_apply]