internlm/Lean-Github huggingface dataset:
Theorem: Super.barrier
Proof state before:
case h.h2
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
n✝ : Set (ℂ × S)
no : IsOpen n✝
na : (c, a) ∈ n✝
n' : Set (ℂ × S) := n✝ ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n✝ ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
i0 : Set ℂ
i1 : Set S
i0o : IsOpen i0
i0m : c ∈ i0
i1o : IsOpen i1
i1m : a ∈ i1
ii : i0 ×ˢ i1 ⊆ u ∧ i0 ×ˢ i1 ⊆ i
t : Set (ℂ × S) := u \ univ ×ˢ i1
ta : ∀ (e : ℂ), (e, a) ∉ t
e : ℂ
em : e ∈ i0
z : S
zm : (e, z) ∉ n✝
za : Attracts (f e) z a
m : ℕ
mh : ∀ (n : ℕ), m ≤ n → (f e)^[n] z ∈ i1
en : ∃ n, (f e)^[n] z ∈ i1
n : ℕ := Nat.find en
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : (f e)^[n - 1] z ∉ i1
⊢ (e, (f e)^[n - 1] z) ∉ univ ×ˢ i1
Tactic:
contrapose nt
Proof state after:
case h.h2
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
n✝ : Set (ℂ × S)
no : IsOpen n✝
na : (c, a) ∈ n✝
n' : Set (ℂ × S) := n✝ ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n✝ ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
i0 : Set ℂ
i1 : Set S
i0o : IsOpen i0
i0m : c ∈ i0
i1o : IsOpen i1
i1m : a ∈ i1
ii : i0 ×ˢ i1 ⊆ u ∧ i0 ×ˢ i1 ⊆ i
t : Set (ℂ × S) := u \ univ ×ˢ i1
ta : ∀ (e : ℂ), (e, a) ∉ t
e : ℂ
em : e ∈ i0
z : S
zm : (e, z) ∉ n✝
za : Attracts (f e) z a
m : ℕ
mh : ∀ (n : ℕ), m ≤ n → (f e)^[n] z ∈ i1
en : ∃ n, (f e)^[n] z ∈ i1
n : ℕ := Nat.find en
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : ¬(e, (f e)^[n - 1] z) ∉ univ ×ˢ i1
⊢ ¬(f e)^[n - 1] z ∉ i1
Theorem: Super.barrier
Proof state before:
case h.h2
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
n✝ : Set (ℂ × S)
no : IsOpen n✝
na : (c, a) ∈ n✝
n' : Set (ℂ × S) := n✝ ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n✝ ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
i0 : Set ℂ
i1 : Set S
i0o : IsOpen i0
i0m : c ∈ i0
i1o : IsOpen i1
i1m : a ∈ i1
ii : i0 ×ˢ i1 ⊆ u ∧ i0 ×ˢ i1 ⊆ i
t : Set (ℂ × S) := u \ univ ×ˢ i1
ta : ∀ (e : ℂ), (e, a) ∉ t
e : ℂ
em : e ∈ i0
z : S
zm : (e, z) ∉ n✝
za : Attracts (f e) z a
m : ℕ
mh : ∀ (n : ℕ), m ≤ n → (f e)^[n] z ∈ i1
en : ∃ n, (f e)^[n] z ∈ i1
n : ℕ := Nat.find en
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : ¬(e, (f e)^[n - 1] z) ∉ univ ×ˢ i1
⊢ ¬(f e)^[n - 1] z ∉ i1
Tactic:
simp only [Set.prod_mk_mem_set_prod_eq, not_and, not_forall, Set.not_not_mem,
  exists_prop] at nt ⊢
Proof state after:
case h.h2
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
n✝ : Set (ℂ × S)
no : IsOpen n✝
na : (c, a) ∈ n✝
n' : Set (ℂ × S) := n✝ ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n✝ ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
i0 : Set ℂ
i1 : Set S
i0o : IsOpen i0
i0m : c ∈ i0
i1o : IsOpen i1
i1m : a ∈ i1
ii : i0 ×ˢ i1 ⊆ u ∧ i0 ×ˢ i1 ⊆ i
t : Set (ℂ × S) := u \ univ ×ˢ i1
ta : ∀ (e : ℂ), (e, a) ∉ t
e : ℂ
em : e ∈ i0
z : S
zm : (e, z) ∉ n✝
za : Attracts (f e) z a
m : ℕ
mh : ∀ (n : ℕ), m ≤ n → (f e)^[n] z ∈ i1
en : ∃ n, (f e)^[n] z ∈ i1
n : ℕ := Nat.find en
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : e ∈ univ ∧ (f e)^[n - 1] z ∈ i1
⊢ (f e)^[n - 1] z ∈ i1
Theorem: Super.barrier
Proof state before:
case h.h2
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
n✝ : Set (ℂ × S)
no : IsOpen n✝
na : (c, a) ∈ n✝
n' : Set (ℂ × S) := n✝ ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n✝ ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
i0 : Set ℂ
i1 : Set S
i0o : IsOpen i0
i0m : c ∈ i0
i1o : IsOpen i1
i1m : a ∈ i1
ii : i0 ×ˢ i1 ⊆ u ∧ i0 ×ˢ i1 ⊆ i
t : Set (ℂ × S) := u \ univ ×ˢ i1
ta : ∀ (e : ℂ), (e, a) ∉ t
e : ℂ
em : e ∈ i0
z : S
zm : (e, z) ∉ n✝
za : Attracts (f e) z a
m : ℕ
mh : ∀ (n : ℕ), m ≤ n → (f e)^[n] z ∈ i1
en : ∃ n, (f e)^[n] z ∈ i1
n : ℕ := Nat.find en
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : e ∈ univ ∧ (f e)^[n - 1] z ∈ i1
⊢ (f e)^[n - 1] z ∈ i1
Tactic:
exact nt.2
Proof state after:
no goals
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
by_cases t0 : 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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : ¬t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : ¬t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
simp only [← ne_eq, ← Set.nonempty_iff_ne_empty] at t0
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
have pc : ContinuousOn (uncurry s.potential) t := by
  refine ContinuousOn.mono ?_ b.near
  intro ⟨c, z⟩ m; apply ContinuousAt.continuousWithinAt
  apply ContinuousAt.potential_of_reaches s; use 0; simpa only [Function.iterate_zero_apply]
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
rcases b.compact.exists_isMinOn t0 pc with ⟨⟨e, z⟩, ps, pm⟩
Proof state after:
case neg.intro.mk.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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Theorem: Barrier.potential_large
Proof state before:
case neg.intro.mk.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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
use s.potential e z
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0 ∧ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0 ∧ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Tactic:
constructor
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0

case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∀ (e : ℂ) (z : S), (e, z) ∈ t → 1 ≤ s.potential e z
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∀ (e : ℂ) (z : S), (e, z) ∈ t → 1 ≤ s.potential e z
Tactic:
simp only [t0, gt_iff_lt, Set.mem_empty_iff_false, IsEmpty.forall_iff, forall_const,
  imp_true_iff, and_true_iff]
Proof state after:
no goals
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) t
Tactic:
refine ContinuousOn.mono ?_ b.near
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) s.near
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) s.near
Tactic:
intro ⟨c, z⟩ 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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousWithinAt (uncurry s.potential) s.near (c, z)
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousWithinAt (uncurry s.potential) s.near (c, z)
Tactic:
apply ContinuousAt.continuousWithinAt
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousAt (uncurry s.potential) (c, z)
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
apply ContinuousAt.potential_of_reaches s
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] 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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near
Theorem: Barrier.potential_large
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
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near
Tactic:
simpa only [Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0
Tactic:
have h := b.hole e
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : (e, a) ∉ t
⊢ s.potential e z > 0
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : (e, a) ∉ t
⊢ s.potential e z > 0
Tactic:
contrapose h
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : ¬s.potential e z > 0
⊢ ¬(e, a) ∉ t
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : ¬s.potential e z > 0
⊢ ¬(e, a) ∉ t
Tactic:
simp only [not_lt] at h
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
⊢ ¬(e, a) ∉ t
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
⊢ ¬(e, a) ∉ t
Tactic:
have h' := le_antisymm h s.potential_nonneg
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : s.potential e z = 0
⊢ ¬(e, a) ∉ t
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : s.potential e z = 0
⊢ ¬(e, a) ∉ t
Tactic:
simp only [s.potential_eq_zero, s.preimage_eq, exists_const] at h'
Proof state after:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : z = a
⊢ ¬(e, a) ∉ t
Theorem: Barrier.potential_large
Proof state before:
case h.left
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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : z = a
⊢ ¬(e, a) ∉ t
Tactic:
simp only [not_not, ← h', ps]
Proof state after:
no goals
Theorem: Barrier.potential_large
Proof state before:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Tactic:
intro e z m
Proof state after:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
pm : IsMinOn (uncurry s.potential) t (e✝, z✝)
e : ℂ
z : S
m : (e, z) ∈ t
⊢ s.potential e✝ z✝ ≤ s.potential e z