Theorem: Continuous.potential (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
⊢ Continuous (uncurry s.potential)
Tactic:
refine continuous_iff_lower_upperSemicontinuous.mpr ⟨?_, UpperSemicontinuous.potential s⟩
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
⊢ LowerSemicontinuous (uncurry s.potential)

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
⊢ LowerSemicontinuous (uncurry s.potential)
Tactic:
intro ⟨c, z⟩
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
c : ℂ
z : S
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
by_cases re : ∃ n, (c, (f c)^[n] z) ∈ s.near
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
exact (ContinuousAt.potential_of_reaches s re).lowerSemicontinuousAt
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
simp only [not_exists] at re
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
intro y y1
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < uncurry s.potential (c, z)
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < uncurry s.potential x'

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < uncurry s.potential (c, z)
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < uncurry s.potential x'
Tactic:
simp only [ContinuousAt, uncurry, s.potential_eq_one re] at y1 ⊢
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < 1
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
y : ℝ
y1 : y < 1
⊢ ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2
Tactic:
contrapose re
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ¬∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ¬∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), y < s.potential x'.1 x'.2
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
Tactic:
simp only [Filter.not_eventually, not_lt] at re
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
⊢ ¬∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
Tactic:
simp only [not_forall, not_not] at re ⊢
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
by_cases za : z = a
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : z = a
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
have sn : {(c, a)}ᶜ ∈ 𝓝 (c, z) :=
  compl_singleton_mem_nhds
    (by simp only [za, Ne, Prod.mk.inj_iff, and_false_iff, not_false_iff])
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases (Filter.hasBasis_iff.mp (compact_basis_nhds (c, z)) ({(c, a)}ᶜ)).mp sn with
  ⟨u, ⟨un, uc⟩, ua⟩
State after:
case neg.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
ua : u ⊆ {(c, a)}ᶜ
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
ua : u ⊆ {(c, a)}ᶜ
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
simp only [Set.subset_compl_singleton_iff] at ua
State after:
case neg.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases s.barrier (uᶜ) uc.isClosed.isOpen_compl (Set.mem_compl ua) with ⟨t, b⟩
State after:
case neg.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases b.potential_large with ⟨r, rp, rt⟩
State after:
case neg.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
en : ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases en with ⟨n, h⟩
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases eventually_nhds_iff.mp h with ⟨v, vh, vo, vc⟩
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
have ev : ∀ᶠ p : ℂ × S in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ := by
  simp only [Filter.eventually_iff, Set.setOf_mem_eq]
  exact Filter.inter_mem un ((vo.prod isOpen_univ).mem_nhds (Set.mk_mem_prod vc (Set.mem_univ _)))
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
have ef : ∃ᶠ p in 𝓝 (c, z), p ∈ b.fast n := by
  refine (re.and_eventually ev).mp (eventually_of_forall ?_)
  intro ⟨e, z⟩ ⟨zy, m⟩
  simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true_iff] at m
  exact vh e m.2 z m.1 zy
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
rcases b.mem_fast.mp (ef.mem_of_closed (b.closed_fast _)) with ⟨n, _, r⟩
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
n✝ : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n✝
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n✝
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n✝
n : ℕ
left✝ : n < n✝
r : (c, (f c)^[n] z) ∈ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
n✝ : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n✝
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n✝
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
ef : ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n✝
n : ℕ
left✝ : n < n✝
r : (c, (f c)^[n] z) ∈ t
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
exact ⟨n, b.near r⟩
State after:
no goals

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : z = a
⊢ ∃ x, (c, (f c)^[x] z) ∈ s.near
Tactic:
use 0
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near
Tactic:
simp only [za, Function.iterate_zero_apply, s.mem_near c]
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
⊢ (c, z) ≠ (c, a)
Tactic:
simp only [za, Ne, Prod.mk.inj_iff, and_false_iff, not_false_iff]
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
rcases exists_pow_lt_of_lt_one rp y1 with ⟨k, ky⟩
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
rcases Filter.exists_le_of_tendsto_atTop (Nat.tendsto_pow_atTop_atTop_of_one_lt s.d1) 0 k
  with ⟨n, _, nk⟩
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
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n

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
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
⊢ ∃ n, ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
use n
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
Tactic:
refine b.barrier.mp (eventually_of_forall fun e h z m py ↦ ?_)
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
⊢ (e, z) ∈ b.fast n

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
⊢ (e, z) ∈ b.fast n
Tactic:
rcases h z (not_mem_compl_iff.mpr m) za with ⟨o, oh⟩
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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
⊢ (e, z) ∈ b.fast n

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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
⊢ (e, z) ∈ b.fast n
Tactic:
by_cases no : n ≤ o
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
⊢ (e, z) ∈ b.fast n

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : ¬n ≤ o
⊢ (e, z) ∈ b.fast 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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
⊢ Attracts (f e) z a
Tactic:
by_cases r : ∃ n, (e, (f e)^[n] z) ∈ s.near
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ¬∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ¬∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
simp only [not_exists] at r
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
Tactic:
rw [s.potential_eq_one r] at py
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : 1 ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : 1 ≤ y
r : ∀ (x : ℕ), (e, (f e)^[x] z) ∉ s.near
⊢ Attracts (f e) z a
Tactic:
linarith
State after:
no goals

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
r : ∃ n, (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
rcases r with ⟨n, r⟩
State after:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n✝ : ℕ
left✝ : n✝ ≥ 0
nk : k ≤ d ^ n✝
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
n : ℕ
r : (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a

State before:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝¹ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r✝ : ℝ
rp : r✝ > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r✝ ≤ s.potential e z
k : ℕ
ky : y ^ k < r✝
n✝ : ℕ
left✝ : n✝ ≥ 0
nk : k ≤ d ^ n✝
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
n : ℕ
r : (e, (f e)^[n] z) ∈ s.near
⊢ Attracts (f e) z a
Tactic:
exact s.attracts r
State after:
no goals

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
⊢ (e, z) ∈ b.fast n
Tactic:
have pyo : s.potential e z ^ d ^ o ≤ y ^ d ^ o := by bound
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e z ^ d ^ o ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e z ^ d ^ o ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
rw [← s.potential_eqn_iter o] at pyo
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
have ryo : r ≤ y ^ d ^ o := _root_.trans (rt _ _ oh) pyo
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
have kdo : k ≤ d ^ o := _root_.trans nk (Nat.pow_le_pow_of_le_right s.dp no)
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
⊢ (e, z) ∈ b.fast n

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
⊢ (e, z) ∈ b.fast n
Tactic:
have ryk : r ≤ y ^ k :=
  _root_.trans ryo (pow_le_pow_of_le_one (_root_.trans s.potential_nonneg py) y1.le kdo)
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
ryk : r ≤ y ^ k
⊢ (e, z) ∈ b.fast n

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
pyo : s.potential e ((f e)^[o] z) ≤ y ^ d ^ o
ryo : r ≤ y ^ d ^ o
kdo : k ≤ d ^ o
ryk : r ≤ y ^ k
⊢ (e, z) ∈ b.fast n
Tactic:
linarith
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : n ≤ o
⊢ s.potential e z ^ d ^ o ≤ y ^ d ^ o
Tactic:
bound
State after:
no goals

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : ¬n ≤ o
⊢ (e, z) ∈ b.fast n
Tactic:
simp only [not_le] at no
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ (e, z) ∈ b.fast n

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ (e, z) ∈ b.fast n
Tactic:
rw [b.mem_fast]
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ ∃ n_1 < n, (e, (f e)^[n_1] z) ∈ t

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za✝ : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
k : ℕ
ky : y ^ k < r
n : ℕ
left✝ : n ≥ 0
nk : k ≤ d ^ n
e : ℂ
h : ∀ (z : S), (e, z) ∉ uᶜ → Attracts (f e) z a → ∃ n, (e, (f e)^[n] z) ∈ t
z : S
m : (e, z) ∈ u
py : s.potential e z ≤ y
za : Attracts (f e) z a
o : ℕ
oh : (e, (f e)^[o] z) ∈ t
no : o < n
⊢ ∃ n_1 < n, (e, (f e)^[n_1] z) ∈ t
Tactic:
use o, no, oh
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
Tactic:
simp only [Filter.eventually_iff, Set.setOf_mem_eq]
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
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ u ∩ v ×ˢ univ ∈ 𝓝 (c, z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
⊢ u ∩ v ×ˢ univ ∈ 𝓝 (c, z)
Tactic:
exact Filter.inter_mem un ((vo.prod isOpen_univ).mem_nhds (Set.mk_mem_prod vc (Set.mem_univ _)))
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∃ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ b.fast n
Tactic:
refine (re.and_eventually ev).mp (eventually_of_forall ?_)
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
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∀ (x : ℂ × S), s.potential x.1 x.2 ≤ y ∧ x ∈ u ∩ v ×ˢ univ → x ∈ b.fast 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
c : ℂ
z : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z), s.potential x.1 x.2 ≤ y
za : ¬z = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ
⊢ ∀ (x : ℂ × S), s.potential x.1 x.2 ≤ y ∧ x ∈ u ∩ v ×ˢ univ → x ∈ b.fast n
Tactic:
intro ⟨e, z⟩ ⟨zy, m⟩
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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∩ v ×ˢ univ
⊢ (e, z) ∈ b.fast 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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∩ v ×ˢ univ
⊢ (e, z) ∈ b.fast n
Tactic:
simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true_iff] at m
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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∧ e ∈ v
⊢ (e, z) ∈ b.fast 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
c : ℂ
z✝ : S
y : ℝ
y1 : y < 1
re : ∃ᶠ (x : ℂ × S) in 𝓝 (c, z✝), s.potential x.1 x.2 ≤ y
za : ¬z✝ = a
sn : {(c, a)}ᶜ ∈ 𝓝 (c, z✝)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, z✝)
uc : IsCompact u
ua : (c, a) ∉ u
t : Set (ℂ × S)
b : Barrier s c uᶜ t
r : ℝ
rp : r > 0
rt : ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
n : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (z : S), (e, z) ∈ u → s.potential e z ≤ y → (e, z) ∈ b.fast n
v : Set ℂ
vh : ∀ x ∈ v, ∀ (z : S), (x, z) ∈ u → s.potential x z ≤ y → (x, z) ∈ b.fast n
vo : IsOpen v
vc : c ∈ v
ev : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z✝), p ∈ u ∩ v ×ˢ univ
e : ℂ
z : S
zy : s.potential (e, z).1 (e, z).2 ≤ y
m : (e, z) ∈ u ∧ e ∈ v
⊢ (e, z) ∈ b.fast n
Tactic:
exact vh e m.2 z m.1 zy
State after:
no goals