Theorem: Super.iter_stays_near (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
⊢ (c, (f c)^[n] z) ∈ s.near
Tactic:
induction' n with n h
State after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near

State before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
simp only [Function.iterate_zero, id, m]
State after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near

State before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
simp only [Nat.add_succ, Function.iterate_succ', s.stays_near h, Function.comp]
State after:
no goals