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

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

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

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

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

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo f^[n + 1] t t
Tactic:
rw [Function.iterate_succ']
State after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo (f ∘ f^[n]) t t

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo (f ∘ f^[n]) t t
Tactic:
exact s.ft.comp h
State after:
no goals