Theorem: Postcritical.eventually (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 : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), Postcritical s p.1 p.2
Tactic:
refine (s.isOpen_post.eventually_mem ?_).mp (eventually_of_forall fun _ m ↦ 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 z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ (c, z) ∈ s.post

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 : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ (c, z) ∈ s.post
Tactic:
exact p
State after:
no goals