Theorem: Super.nonempty_ps (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
⊢ 1 ∈ s.ps c
Tactic:
simp only [Super.ps, mem_setOf, eq_self_iff_true, true_or_iff]
State after:
no goals