Theorem: Super.barrier (Ray/Dynamics/Potential.lean)

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
⊢ ∃ t, Barrier s c n t
Tactic:
set n' := n ∩ s.near
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
⊢ ∃ t, Barrier s c n t

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
⊢ ∃ t, Barrier s c n t
Tactic:
have nn' : n' ∈ 𝓝 (c, a) :=
  Filter.inter_mem (no.mem_nhds na) (s.isOpen_near.mem_nhds (s.mem_near c))
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)
⊢ ∃ t, Barrier s c n t

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)
⊢ ∃ t, Barrier s c n t
Tactic:
rcases (Filter.hasBasis_iff.mp (compact_basis_nhds (c, a)) n').mp nn' with ⟨u, ⟨un, uc⟩, us⟩
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
us : u ⊆ n'
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
⊢ ∃ t, Barrier s c n t

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
us : u ⊆ n'
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
⊢ ∃ t, Barrier s c n t
Tactic:
simp only [Set.subset_inter_iff, n'] at us
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
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
⊢ ∃ t, Barrier s c n t

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
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
⊢ ∃ t, Barrier s c n t
Tactic:
rcases eventually_nhds_iff.mp
    (s.no_jump c (interior u) isOpen_interior (mem_interior_iff_mem_nhds.mpr un)) with
  ⟨i, ih, io, ia⟩
State after:
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

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⟩
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

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
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

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
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

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)
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

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
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

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, ?_⟩
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

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]
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

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
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

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⟩
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

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
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

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⟩
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

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 _)⟩
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

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
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

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
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

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
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

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))
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

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)
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

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
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

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
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✝

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]
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✝

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
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✝

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))
State after:
no goals

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
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

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))
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)

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]
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))

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)]
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)

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))]
State after:
no goals

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
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

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 ⊢
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

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
State after:
no goals