Theorem: Super.mem_ext (Ray/Dynamics/Ray.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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ (c, 0) ∈ s.ext
Tactic:
simp only [Super.ext, mem_setOf, Complex.abs.map_zero, s.p_pos c]
State after:
no goals