internlm/Lean-Github huggingface dataset:
Theorem: Continuous.potential
Proof state before:
case 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 : ℂ
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, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
rcases Filter.exists_le_of_tendsto_atTop (Nat.tendsto_pow_atTop_atTop_of_one_lt s.d1) 0 k
  with ⟨n, _, nk⟩
Proof 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 : ℂ
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
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Theorem: Continuous.potential
Proof 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 : ℂ
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
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
use n
Proof state after:
case h
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 : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Theorem: Continuous.potential
Proof state before:
case h
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 : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
refine b.barrier.mp (eventually_of_forall fun e h z m py ↦ ?_)
Proof state after:
case h
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
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
Proof state before:
case h
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
⊢ (e, z) ∈ b.fast n
Tactic:
rcases h z (not_mem_compl_iff.mpr m) za with ⟨o, oh⟩
Proof state after:
case h.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 : ℂ
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
⊢ (e, z) ∈ b.fast n
Theorem: Continuous.potential
Proof state before:
case h.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 : ℂ
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
⊢ (e, z) ∈ b.fast n
Tactic:
by_cases no : n ≤ o
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
⊢ (e, z) ∈ b.fast n

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
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
⊢ Attracts (f e) z a
Tactic:
by_cases r : ∃ n, (e, (f e)^[n] z) ∈ s.near
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
r : ∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a

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
r : ¬∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
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
r : ¬∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
simp only [not_exists] at r
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
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
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
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
Tactic:
rw [s.potential_eq_one r] at py
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 : 1 ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
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 : 1 ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
Tactic:
linarith
Proof state after:
no goals
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
r : ∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
rcases r with ⟨n, r⟩
Proof state after:
case pos.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 : ℂ
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
n : ℕ
r : (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Theorem: Continuous.potential
Proof state before:
case pos.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 : ℂ
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
n : ℕ
r : (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
exact s.attracts r
Proof state after:
no goals
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
⊢ (e, z) ∈ b.fast n
Tactic:
have pyo : s.potential e z ^ d ^ o ≤ y ^ d ^ o := by bound
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 z ^ d ^ o ≤ y ^ 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 z ^ d ^ o ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
rw [← s.potential_eqn_iter o] at pyo
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
⊢ (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
⊢ (e, z) ∈ b.fast n
Tactic:
have ryo : r ≤ y ^ d ^ o := _root_.trans (rt _ _ oh) pyo
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
⊢ (e, z) ∈ b.fast n