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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ leadingCoeff (fl (f d) ∞ c) 0 = 1
Tactic:
rw [fl_f', analyticAt_gl.monomial_mul_leadingCoeff gl_frequently_ne_zero, leadingCoeff_of_ne_zero]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 = 1

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 = 1

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
exact gl_zero
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:
rw [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