Theorem: SuperNear.f_ne_zero (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z ≠ 0
⊢ f z ≠ 0
Tactic:
simp only [s.fg, mul_ne_zero (pow_ne_zero _ z0) (s.g_ne_zero zt), Ne, not_false_iff]
State after:
no goals