Theorem: SuperAt.d0 (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ d ≠ 0
Tactic:
have h := s.d2
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
h : 2 ≤ d
⊢ d ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
h : 2 ≤ d
⊢ d ≠ 0
Tactic:
omega
State after:
no goals