Theorem: Super.potential_eq_one (Ray/Dynamics/Potential.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✝
a : ∀ (n : ℕ), (c, (f c)^[n] z) ∉ s.near
⊢ s.potential c z = 1
Tactic:
simp only [Super.potential, not_exists.mpr a, not_false_iff, dif_neg, and_false_iff]
State after:
no goals