internlm/Lean-Github huggingface dataset:
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
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
intro y y1
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
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < uncurry s.potential (c, z)
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < uncurry s.potential x'
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
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < uncurry s.potential (c, z)
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < uncurry s.potential x'
Tactic:
simp only [ContinuousAt, uncurry, s.potential_eq_one re] at y1 ⊢
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
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < 1
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2
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
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < 1
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2
Tactic:
contrapose re
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), y < s.potential x'.1 x'.2
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
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), y < s.potential x'.1 x'.2
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
Tactic:
simp only [Filter.not_eventually, not_lt] at re
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
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
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
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
Tactic:
simp only [not_forall, not_not] at re ⊢
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
by_cases za : z = a
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
have sn : {(c, a)}ᶜ ∈ 𝓝 (c, z) :=
  compl_singleton_mem_nhds
    (by simp only [za, Ne, Prod.mk.inj_iff, and_false_iff, not_false_iff])
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)
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
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)
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases (Filter.hasBasis_iff.mp (compact_basis_nhds (c, z)) ({(c, a)}ᶜ)).mp sn with
  ⟨u, ⟨un, uc⟩, ua⟩
Proof state after:
case neg.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)
ua : u ⊆ {(c, a)}ᶜ
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.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)
ua : u ⊆ {(c, a)}ᶜ
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
simp only [Set.subset_compl_singleton_iff] at ua
Proof state after:
case neg.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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases s.barrier (uᶜ) uc.isClosed.isOpen_compl (Set.mem_compl ua) with ⟨t, b⟩
Proof state after:
case neg.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases b.potential_large with ⟨r, rp, rt⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
en : ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases en with ⟨n, h⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases eventually_nhds_iff.mp h with ⟨v, vh, vo, vc⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
have ev : ∀ᶠ p : ℂ × S in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ := by
  simp only [Filter.eventually_iff, Set.setOf_mem_eq]
  exact Filter.inter_mem un ((vo.prod isOpen_univ).mem_nhds (Set.mk_mem_prod vc (Set.mem_univ _)))
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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, (c, (f c)^[x] z) ∈ s.near
Tactic:
have ef : ∃ᶠ p in 𝓝 (c, z), p ∈ b.fast n := by
  refine (re.and_eventually ev).mp (eventually_of_forall ?_)
  intro ⟨e, z⟩ ⟨zy, m⟩
  simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true_iff] at m
  exact vh e m.2 z m.1 zy
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases b.mem_fast.mp (ef.mem_of_closed (b.closed_fast _)) with ⟨n, _, r⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n✝
n : ℕ
left✝ : n < n✝
r : (c, (f c)^[n] z) ∈ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Theorem: Continuous.potential
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
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
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n✝
n : ℕ
left✝ : n < n✝
r : (c, (f c)^[n] z) ∈ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
exact ⟨n, b.near 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
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
use 0
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
⊢ (c, (f c)^[0] z) ∈ s.near
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
⊢ (c, (f c)^[0] z) ∈ s.near
Tactic:
simp only [za, Function.iterate_zero_apply, s.mem_near c]
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
⊢ (c, z) ≠ (c, a)
Tactic:
simp only [za, Ne, Prod.mk.inj_iff, and_false_iff, not_false_iff]
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, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
rcases exists_pow_lt_of_lt_one rp y1 with ⟨k, ky⟩
Proof state after:
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