internlm/Lean-Github huggingface dataset:
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof state after:
no goals
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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]
Proof 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
Theorem: Super.potential_basis'
Proof 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 _
Proof state after:
no goals
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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⟩
Proof 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
Theorem: Super.potential_basis'
Proof 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]
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof state after:
no goals
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof 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
Theorem: Super.potential_basis'
Proof 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]
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ
Theorem: Super.potential_basis'
Proof 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]
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof state after:
no goals
Theorem: Super.potential_basis'
Proof 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]
Proof 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ᶜ)
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ)
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ)
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ)
Theorem: Super.potential_basis'
Proof 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⟩
Proof 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ᶜ)
Theorem: Super.potential_basis'
Proof 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]
Proof 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
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ
Theorem: Super.potential_basis'
Proof 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
Proof 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ᶜ