Theorem: Super.potential_basis (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 : ℂ
t : Set S
n : t ∈ 𝓝 a
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
rcases mem_nhds_iff.mp n with ⟨t', tt, o, m⟩
State after:
case intro.intro.intro
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case intro.intro.intro
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
rcases s.potential_basis' c (o.mem_nhds m) o with ⟨p, pp, sub⟩
State after:
case intro.intro.intro.intro.intro
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
p : ℝ
pp : 0 < p
sub : {z | s.potential c z < p} ⊆ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case intro.intro.intro.intro.intro
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
p : ℝ
pp : 0 < p
sub : {z | s.potential c z < p} ⊆ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
use p, pp, _root_.trans sub tt
State after:
no goals