Theorem: gl_frequently_ne_zero (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ᶠ (z : ℂ) in 𝓝 0, gl d c z ≠ 0
Tactic:
refine (analyticAt_gl.continuousAt.eventually_ne ?_).frequently
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
simp only [gl_zero]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
State after:
no goals