internlm/Lean-Github huggingface dataset:
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
have kdo : k ≤ d ^ o := _root_.trans nk (Nat.pow_le_pow_of_le_right s.dp no)
Proof 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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
have ryk : r ≤ y ^ k :=
  _root_.trans ryo (pow_le_pow_of_le_one (_root_.trans s.potential_nonneg py) y1.le kdo)
Proof 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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
ryk : r ≤ y ^ k
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
ryk : r ≤ y ^ k
⊢ (e, z) ∈ b.fast n
Tactic:
linarith
Proof state after:
no goals
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
⊢ s.potential e z ^ d ^ o ≤ y ^ d ^ o
Tactic:
bound
Proof state after:
no goals
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : ¬n ≤ o
⊢ (e, z) ∈ b.fast n
Tactic:
simp only [not_le] at no
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ (e, z) ∈ b.fast n
Tactic:
rw [b.mem_fast]
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ ∃ n_1 < n, (e, (f e)^[n_1] z) ∈ t
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ ∃ n_1 < n, (e, (f e)^[n_1] z) ∈ t
Tactic:
use o, no, oh
Proof state after:
no goals
Theorem: Continuous.potential
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
Tactic:
simp only [Filter.eventually_iff, Set.setOf_mem_eq]
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ u ∩ v ×ˢ univ ∈ 𝓝 (c, z)
Theorem: Continuous.potential
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ u ∩ v ×ˢ univ ∈ 𝓝 (c, z)
Tactic:
exact Filter.inter_mem un ((vo.prod isOpen_univ).mem_nhds (Set.mk_mem_prod vc (Set.mem_univ _)))
Proof state after:
no goals
Theorem: Continuous.potential
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
Tactic:
refine (re.and_eventually ev).mp (eventually_of_forall ?_)
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∀ (x : ℂ × S), s.potential x.1 x.2 ≤ y ∧ x ∈ u ∩ v ×ˢ univ → x ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∀ (x : ℂ × S), s.potential x.1 x.2 ≤ y ∧ x ∈ u ∩ v ×ˢ univ → x ∈ b.fast n
Tactic:
intro ⟨e, z⟩ ⟨zy, 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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∩ v ×ˢ univ
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∩ v ×ˢ univ
⊢ (e, z) ∈ b.fast n
Tactic:
simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true_iff] 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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∧ e ∈ v
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
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 : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∧ e ∈ v
⊢ (e, z) ∈ b.fast n
Tactic:
exact vh e m.2 z m.1 zy
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
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
by_cases ne : tᶜ = ∅
Proof 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
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 : ¬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)
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
⊢ ∃ 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
⊢ ∃ 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
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
⊢ ∃ 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
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
have below : BddBelow (s.potential c '' tᶜ) := bddBelow_def.mpr ⟨0, pos⟩
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ᶜ)
⊢ ∃ 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ᶜ)
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
generalize hq : sInf (s.potential c '' tᶜ) = q
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
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t