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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ AnalyticAt ℂ (gl d c) 0
Tactic:
apply (analyticAt_const.add (analyticAt_const.mul ((analyticAt_id _ _).pow _))).inv
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ((fun x => 1) + fun x => c * id x ^ d) 0 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ((fun x => 1) + fun x => c * id x ^ d) 0 ≠ 0
Tactic:
simp only [Pi.pow_apply, id_eq, Pi.add_apply, ne_eq, zero_pow (d_ne_zero _), mul_zero, add_zero,
  one_ne_zero, not_false_eq_true]
State after:
no goals