internlm/Lean-Github huggingface dataset:
Theorem: Super.barrier
Proof state before:
case 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
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
⊢ ∃ t, Barrier s c n t
Tactic:
rcases mem_nhds_prod_iff'.mp (Filter.inter_mem un (io.mem_nhds ia)) with
  ⟨i0, i1, i0o, i0m, i1o, i1m, ii⟩
Proof state after:
case 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
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 ∩ i
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof state before:
case 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
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 ∩ i
⊢ ∃ t, Barrier s c n t
Tactic:
simp only [Set.subset_inter_iff] at ii
Proof state after:
case 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
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, Barrier s c n t
Theorem: Super.barrier
Proof state before:
case 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
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, Barrier s c n t
Tactic:
set t := u \ univ ×ˢ i1
Proof state after:
case 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
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
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof state before:
case 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
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
⊢ ∃ t, Barrier s c n t
Tactic:
have ta : ∀ e, (e, a) ∉ t := fun e ↦
  Set.not_mem_diff_of_mem (Set.mk_mem_prod (Set.mem_univ _) i1m)
Proof state after:
case 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
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
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof state before:
case 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
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
⊢ ∃ t, Barrier s c n t
Tactic:
use t
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 : 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
⊢ Barrier s c n t
Theorem: Super.barrier
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 : 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
⊢ Barrier s c n t
Tactic:
refine ⟨uc.diff (isOpen_univ.prod i1o), _root_.trans (Set.diff_subset _ _) us.1,
    _root_.trans (Set.diff_subset _ _) us.2, ta, ?_⟩
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 : 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 : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∉ n → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
Theorem: Super.barrier
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 : 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 : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∉ n → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
Tactic:
rw [eventually_nhds_iff]
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 : 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
⊢ ∃ t_1, (∀ x ∈ t_1, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t) ∧ IsOpen t_1 ∧ c ∈ t_1
Theorem: Super.barrier
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 : 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
⊢ ∃ t_1, (∀ x ∈ t_1, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t) ∧ IsOpen t_1 ∧ c ∈ t_1
Tactic:
use i0
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 : 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
⊢ (∀ x ∈ i0, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t) ∧ IsOpen i0 ∧ c ∈ i0
Theorem: Super.barrier
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 : 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
⊢ (∀ x ∈ i0, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t) ∧ IsOpen i0 ∧ c ∈ i0
Tactic:
refine ⟨?_, i0o, i0m⟩
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 : 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
⊢ ∀ x ∈ i0, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t
Theorem: Super.barrier
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 : 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
⊢ ∀ x ∈ i0, ∀ (z : S), (x, z) ∉ n → Attracts (f x) z a → ∃ n, (x, (f x)^[n] z) ∈ t
Tactic:
intro e em z zm za
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 : 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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Theorem: Super.barrier
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 : 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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Tactic:
rcases tendsto_atTop_nhds.mp za i1 i1m i1o with ⟨m, mh⟩
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
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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Theorem: Super.barrier
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
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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Tactic:
have en : ∃ n, (f e)^[n] z ∈ i1 := ⟨m, mh m (le_refl _)⟩
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
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, (e, (f e)^[n] z) ∈ t
Theorem: Super.barrier
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
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, (e, (f e)^[n] z) ∈ t
Tactic:
set n := Nat.find en
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
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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Theorem: Super.barrier
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
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
⊢ ∃ n, (e, (f e)^[n] z) ∈ t
Tactic:
use n - 1
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✝ : 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
⊢ (e, (f e)^[n - 1] z) ∈ t