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✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b] z) ∈ s.near
Tactic:
rw [← Nat.sub_add_cancel ab, Function.iterate_add_apply]
State after:
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✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b - a] ((f c)^[a] z)) ∈ s.near

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✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b - a] ((f c)^[a] z)) ∈ s.near
Tactic:
exact s.iter_stays_near m _
State after:
no goals