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

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

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

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

State before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ f^[0] t
Tactic:
simp only [Function.iterate_zero]
State after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ id t

State before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ id t
Tactic:
exact analyticOn_id _
State after:
no goals

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

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
⊢ AnalyticOn ℂ (f ∘ f^[n]) t
Tactic:
intro z zt
State after:
case succ
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (f ∘ f^[n]) z

State before:
case succ
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (f ∘ f^[n]) z
Tactic:
exact (s.fa _ (s.mapsTo n zt)).comp (h z zt)
State after:
no goals