Theorem: iterates_at_zero (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), f^[n] 0 = 0
Tactic:
intro n
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ f^[n] 0 = 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ f^[n] 0 = 0
Tactic:
induction' n with n h
State after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f^[0] 0 = 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0

State before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f^[0] 0 = 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0
Tactic:
simp only [Function.iterate_zero, id]
State after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0
Tactic:
simp only [Function.iterate_succ', Function.comp_apply, h, s.f0]
State after:
no goals