Theorem: Super.basin_post (Ray/Dynamics/Postcritical.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
rcases tendsto_atTop_nhds.mp (s.basin_attracts m) {z | (c, z) ∈ s.post} (s.post_a c)
    (s.isOpen_post.snd_preimage c) with ⟨n, h⟩
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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
specialize h n (le_refl n)
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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (f c)^[n] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (f c)^[n] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
simp only [mem_setOf] at h
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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
use n, h
State after:
no goals