Theorem: attracts_shift (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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Attracts f (f^[k] z) a ↔ Attracts f z a
Tactic:
simp only [Attracts, ← 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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Tendsto (fun n => f^[n + k] z) atTop (𝓝 a) ↔ Tendsto (fun n => f^[n] z) atTop (𝓝 a)

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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Tendsto (fun n => f^[n + k] z) atTop (𝓝 a) ↔ Tendsto (fun n => f^[n] z) atTop (𝓝 a)
Tactic:
apply @Filter.tendsto_add_atTop_iff_nat _ fun n ↦ f^[n] z
State after:
no goals