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
o : IsOpen t
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
by_cases ne : tᶜ = ∅
State after:
case pos
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
o : IsOpen t
ne : tᶜ = ∅
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

case neg
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
o : IsOpen t
ne : ¬tᶜ = ∅
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : ¬tᶜ = ∅
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
replace ne := Set.Nonempty.image (s.potential c) (nonempty_iff_ne_empty.mpr ne)
State after:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
have pos : ∀ p : ℝ, p ∈ s.potential c '' tᶜ → 0 ≤ p := by
  intro p m; simp only [mem_image] at m; rcases m with ⟨z, _, e⟩; rw [← e]
  exact s.potential_nonneg
State after:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
have below : BddBelow (s.potential c '' tᶜ) := bddBelow_def.mpr ⟨0, pos⟩
State after:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
generalize hq : sInf (s.potential c '' tᶜ) = q
State after:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
have qt : ∀ z, s.potential c z < q → z ∈ t := by
  intro z i; contrapose i; simp only [not_lt, ← hq]; apply csInf_le below
  simp only [mem_image]; use z, i
State after:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t

State before:
case neg
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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
qp : 0 < q
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
use q, qp, qt
State after:
no goals

State before:
case pos
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
o : IsOpen t
ne : tᶜ = ∅
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
use 1, zero_lt_one
State after:
case right
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
o : IsOpen t
ne : tᶜ = ∅
⊢ {z | s.potential c z < 1} ⊆ t

State before:
case right
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
o : IsOpen t
ne : tᶜ = ∅
⊢ {z | s.potential c z < 1} ⊆ t
Tactic:
simp only [compl_empty_iff] at ne
State after:
case right
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
o : IsOpen t
ne : t = univ
⊢ {z | s.potential c z < 1} ⊆ t

State before:
case right
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
o : IsOpen t
ne : t = univ
⊢ {z | s.potential c z < 1} ⊆ t
Tactic:
rw [ne]
State after:
case right
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
o : IsOpen t
ne : t = univ
⊢ {z | s.potential c z < 1} ⊆ univ

State before:
case right
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
o : IsOpen t
ne : t = univ
⊢ {z | s.potential c z < 1} ⊆ univ
Tactic:
exact subset_univ _
State after:
no goals

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
⊢ ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
Tactic:
intro p m
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
m : p ∈ s.potential c '' tᶜ
⊢ 0 ≤ p

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
m : p ∈ s.potential c '' tᶜ
⊢ 0 ≤ p
Tactic:
simp only [mem_image] at m
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
m : ∃ x ∈ tᶜ, s.potential c x = p
⊢ 0 ≤ p

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
m : ∃ x ∈ tᶜ, s.potential c x = p
⊢ 0 ≤ p
Tactic:
rcases m with ⟨z, _, e⟩
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
z : S
left✝ : z ∈ tᶜ
e : s.potential c z = p
⊢ 0 ≤ p

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
z : S
left✝ : z ∈ tᶜ
e : s.potential c z = p
⊢ 0 ≤ p
Tactic:
rw [← e]
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
z : S
left✝ : z ∈ tᶜ
e : s.potential c z = p
⊢ 0 ≤ s.potential c z

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
p : ℝ
z : S
left✝ : z ∈ tᶜ
e : s.potential c z = p
⊢ 0 ≤ s.potential c z
Tactic:
exact s.potential_nonneg
State after:
no goals

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
⊢ ∀ (z : S), s.potential c z < q → z ∈ t
Tactic:
intro z i
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : s.potential c z < q
⊢ z ∈ t

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : s.potential c z < q
⊢ z ∈ t
Tactic:
contrapose i
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ ¬s.potential c z < q

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ ¬s.potential c z < q
Tactic:
simp only [not_lt, ← hq]
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ sInf (s.potential c '' tᶜ) ≤ s.potential c z

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ sInf (s.potential c '' tᶜ) ≤ s.potential c z
Tactic:
apply csInf_le below
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ s.potential c z ∈ s.potential c '' tᶜ

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ s.potential c z ∈ s.potential c '' tᶜ
Tactic:
simp only [mem_image]
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ ∃ x ∈ tᶜ, s.potential c x = s.potential c z

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
z : S
i : z ∉ t
⊢ ∃ x ∈ tᶜ, s.potential c x = s.potential c z
Tactic:
use z, i
State after:
no goals

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
⊢ 0 < q
Tactic:
simp only [← hq]
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
⊢ 0 < sInf (s.potential c '' tᶜ)

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
⊢ 0 < sInf (s.potential c '' tᶜ)
Tactic:
have mc := csInf_mem_closure ne below
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ closure (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ closure (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)
Tactic:
rw [IsClosed.closure_eq] at mc
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ s.potential c '' tᶜ
⊢ 0 < sInf (s.potential c '' tᶜ)

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ closure (s.potential c '' tᶜ)
⊢ IsClosed (s.potential c '' tᶜ)

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ s.potential c '' tᶜ
⊢ 0 < sInf (s.potential c '' tᶜ)
Tactic:
simp only [mem_image] at mc
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 : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : ∃ x ∈ tᶜ, s.potential c x = sInf (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : ∃ x ∈ tᶜ, s.potential c x = sInf (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)
Tactic:
rcases mc with ⟨z, m, e⟩
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
m : z ∈ tᶜ
e : s.potential c z = sInf (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
m : z ∈ tᶜ
e : s.potential c z = sInf (s.potential c '' tᶜ)
⊢ 0 < sInf (s.potential c '' tᶜ)
Tactic:
rw [← e]
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
m : z ∈ tᶜ
e : s.potential c z = sInf (s.potential c '' tᶜ)
⊢ 0 < s.potential c z

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
m : z ∈ tᶜ
e : s.potential c z = sInf (s.potential c '' tᶜ)
⊢ 0 < s.potential c z
Tactic:
contrapose m
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : ¬0 < s.potential c z
⊢ z ∉ tᶜ

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : ¬0 < s.potential c z
⊢ z ∉ tᶜ
Tactic:
replace m := le_antisymm (not_lt.mp m) s.potential_nonneg
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : s.potential c z = 0
⊢ z ∉ tᶜ

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : s.potential c z = 0
⊢ z ∉ tᶜ
Tactic:
rw [s.potential_eq_zero_of_onePreimage] at m
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ z ∉ tᶜ

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ z ∉ tᶜ
Tactic:
simp only [m, not_mem_compl_iff]
State after:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ a ∈ t

State before:
case 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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ a ∈ t
Tactic:
exact mem_of_mem_nhds n
State after:
no goals

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
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ closure (s.potential c '' tᶜ)
⊢ IsClosed (s.potential c '' tᶜ)
Tactic:
exact (o.isClosed_compl.isCompact.image (Continuous.potential s).along_snd).isClosed
State after:
no goals