Theorem: Super.potential_pos (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
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ z ≠ a
Tactic:
rw [← s.potential_ne_zero c]
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 : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ s.potential c z ≠ 0

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
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ s.potential c z ≠ 0
Tactic:
use ne_of_gt, fun ne ↦ ne.symm.lt_of_le s.potential_nonneg
State after:
no goals