internlm/Lean-Github huggingface dataset:
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
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
Tactic:
have ni1 : (f e)^[n] z ∈ i1 := Nat.find_spec en
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
ni1 : (f e)^[n] z ∈ i1
⊢ (e, (f e)^[n - 1] 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
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
⊢ (e, (f e)^[n - 1] z) ∈ t
Tactic:
have n0 : n ≠ 0 := by
  contrapose zm; simp only [Set.not_not_mem]
  simp only [Nat.sub, Ne, Nat.find_eq_zero en, Function.iterate_zero, id,
    Set.not_not_mem] at zm
  exact us.1 (ii.1 (Set.mk_mem_prod em zm))
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
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
⊢ (e, (f e)^[n - 1] 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
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
⊢ (e, (f e)^[n - 1] z) ∈ t
Tactic:
have nt : (f e)^[n-1] z ∉ i1 := Nat.find_min en (Nat.pred_lt n0)
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
ni1 : (f e)^[n] z ∈ i1
n0 : n ≠ 0
nt : (f e)^[n - 1] z ∉ i1
⊢ (e, (f e)^[n - 1] 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
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) ∈ t
Tactic:
apply Set.mem_diff_of_mem
Proof state after:
case h.h1
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) ∈ u

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
Theorem: Super.barrier
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✝ : 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
⊢ n ≠ 0
Tactic:
contrapose zm
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✝ : 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
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
zm : ¬n ≠ 0
⊢ ¬(e, z) ∉ n✝
Theorem: Super.barrier
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✝ : 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
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
zm : ¬n ≠ 0
⊢ ¬(e, z) ∉ n✝
Tactic:
simp only [Set.not_not_mem]
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✝ : 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
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
zm : ¬n ≠ 0
⊢ (e, z) ∈ n✝
Theorem: Super.barrier
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✝ : 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
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
zm : ¬n ≠ 0
⊢ (e, z) ∈ n✝
Tactic:
simp only [Nat.sub, Ne, Nat.find_eq_zero en, Function.iterate_zero, id,
  Set.not_not_mem] at zm
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✝ : 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
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
zm : z ∈ i1
⊢ (e, z) ∈ n✝
Theorem: Super.barrier
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✝ : 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
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
zm : z ∈ i1
⊢ (e, z) ∈ n✝
Tactic:
exact us.1 (ii.1 (Set.mk_mem_prod em zm))
Proof state after:
no goals
Theorem: Super.barrier
Proof state before:
case h.h1
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) ∈ u
Tactic:
apply interior_subset
Proof state after:
case h.h1.a
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) ∈ interior u
Theorem: Super.barrier
Proof state before:
case h.h1.a
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) ∈ interior u
Tactic:
apply ih (e, (f e)^[n] z) (ii.2 (Set.mk_mem_prod em ni1))
Proof state after:
case h.h1.a.a
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] z) = s.fp (e, (f e)^[n - 1] z)
Theorem: Super.barrier
Proof state before:
case h.h1.a.a
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] z) = s.fp (e, (f e)^[n - 1] z)
Tactic:
simp only [Super.fp]
Proof state after:
case h.h1.a.a
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] z) = (e, f e ((f e)^[n - 1] z))
Theorem: Super.barrier
Proof state before:
case h.h1.a.a
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] z) = (e, f e ((f e)^[n - 1] z))
Tactic:
rw [← Function.iterate_succ_apply' (f e) (n - 1)]
Proof state after:
case h.h1.a.a
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] z) = (e, (f e)^[(n - 1).succ] z)
Theorem: Super.barrier
Proof state before:
case h.h1.a.a
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] z) = (e, (f e)^[(n - 1).succ] z)
Tactic:
simp only [Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.one_le_of_lt (Nat.pos_of_ne_zero n0))]
Proof state after:
no goals