Theorem: Super.basin_stays (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
m : (c, z) ∈ s.basin
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
simp only [Super.basin, Set.mem_setOf] at m
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
m : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] 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
m : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
rcases m with ⟨n, m⟩
State after:
case intro
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near

State before:
case intro
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
rw [Filter.eventually_atTop]
State after:
case intro
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ a_1, ∀ b ≥ a_1, (c, (f c)^[b] z) ∈ s.near

State before:
case intro
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ a_1, ∀ b ≥ a_1, (c, (f c)^[b] z) ∈ s.near
Tactic:
use n
State after:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ b ≥ n, (c, (f c)^[b] z) ∈ s.near

State before:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ b ≥ n, (c, (f c)^[b] z) ∈ s.near
Tactic:
intro k kn
State after:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k] z) ∈ s.near

State before:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k] z) ∈ s.near
Tactic:
rw [← Nat.sub_add_cancel kn, Function.iterate_add_apply]
State after:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k - n] ((f c)^[n] z)) ∈ s.near

State before:
case h
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k - n] ((f c)^[n] z)) ∈ s.near
Tactic:
exact s.iter_stays_near m _
State after:
no goals