Theorem: Super.lowerSemicontinuous_p (Ray/Dynamics/Postcritical.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
⊢ LowerSemicontinuous s.p
Tactic:
intro c p h
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : p < s.p c
⊢ ∀ᶠ (x' : ℂ) in 𝓝 c, p < s.p x'

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : p < s.p c
⊢ ∀ᶠ (x' : ℂ) in 𝓝 c, p < s.p x'
Tactic:
contrapose h
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ¬∀ᶠ (x' : ℂ) in 𝓝 c, p < s.p x'
⊢ ¬p < s.p c

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ¬∀ᶠ (x' : ℂ) in 𝓝 c, p < s.p x'
⊢ ¬p < s.p c
Tactic:
simp only [not_lt, Filter.not_eventually] at h ⊢
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
⊢ s.p c ≤ p

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
⊢ s.p c ≤ p
Tactic:
apply le_of_forall_lt'
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
⊢ ∀ (c_1 : ℝ), p < c_1 → s.p c < c_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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
⊢ ∀ (c_1 : ℝ), p < c_1 → s.p c < c_1
Tactic:
intro q' pq'
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
⊢ s.p c < q'

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
⊢ s.p c < q'
Tactic:
rcases exists_between pq' with ⟨q, pq, qq⟩
State after:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qq : q < q'
⊢ s.p c < q'

State before:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qq : q < q'
⊢ s.p c < q'
Tactic:
refine lt_of_le_of_lt ?_ qq
State after:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qq : q < q'
⊢ s.p c ≤ q

State before:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qq : q < q'
⊢ s.p c ≤ q
Tactic:
clear qq pq' q'
State after:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
⊢ s.p c ≤ q

State before:
case H.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
⊢ s.p c ≤ q
Tactic:
by_cases q1 : 1 ≤ q
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : 1 ≤ q
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : ¬1 ≤ q
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : 1 ≤ q
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : ¬1 ≤ q
⊢ s.p c ≤ q
Tactic:
exact _root_.trans s.p_le_one q1
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : ¬1 ≤ q
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : ¬1 ≤ q
⊢ s.p c ≤ q
Tactic:
simp only [not_le] at q1
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
⊢ s.p c ≤ q
Tactic:
set t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
⊢ s.p c ≤ q
Tactic:
have ct : IsClosed t :=
  (isClosed_le (Continuous.potential s) continuous_const).inter s.isClosed_critical_not_a
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
⊢ s.p c ≤ q
Tactic:
set u := Prod.fst '' t
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
⊢ s.p c ≤ q
Tactic:
have cu : IsClosed u := isClosedMap_fst_of_compactSpace _ ct
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ s.p c ≤ q

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ s.p c ≤ q
Tactic:
suffices m : c ∈ u by
  rcases(mem_image _ _ _).mp m with ⟨⟨c', z⟩, ⟨zp, zc, za⟩, cc⟩
  simp only at cc za zc zp; simp only [cc] at za zc zp; clear cc c'
  simp only [Ne, ← s.potential_eq_zero_of_onePreimage c] at za
  refine _root_.trans (csInf_le s.bddBelow_ps ?_) zp; right; use za, z, rfl, zc
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ c ∈ u

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ c ∈ u
Tactic:
refine Filter.Frequently.mem_of_closed ?_ cu
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ ∃ᶠ (x : ℂ) in 𝓝 c, x ∈ u

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
⊢ ∃ᶠ (x : ℂ) in 𝓝 c, x ∈ u
Tactic:
refine h.mp (eventually_of_forall fun e h ↦ ?_)
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
⊢ e ∈ u

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
⊢ e ∈ u
Tactic:
rcases exists_lt_of_csInf_lt s.nonempty_ps (lt_of_le_of_lt h pq) with ⟨r, m, rq⟩
State after:
case neg.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
m : r ∈ s.ps e
rq : r < q
⊢ e ∈ u

State before:
case neg.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
m : r ∈ s.ps e
rq : r < q
⊢ e ∈ u
Tactic:
cases' m with m m
State after:
case neg.intro.intro.inl
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r = 1
⊢ e ∈ u

case neg.intro.intro.inr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r ≠ 0 ∧ ∃ z, s.potential e z = r ∧ Critical (f e) z
⊢ e ∈ u

State before:
case neg.intro.intro.inl
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r = 1
⊢ e ∈ u

case neg.intro.intro.inr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r ≠ 0 ∧ ∃ z, s.potential e z = r ∧ Critical (f e) z
⊢ e ∈ u
Tactic:
linarith
State after:
case neg.intro.intro.inr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r ≠ 0 ∧ ∃ z, s.potential e z = r ∧ Critical (f e) z
⊢ e ∈ u

State before:
case neg.intro.intro.inr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
m : r ≠ 0 ∧ ∃ z, s.potential e z = r ∧ Critical (f e) z
⊢ e ∈ u
Tactic:
rcases m with ⟨r0, z, zr, zc⟩
State after:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
r0 : r ≠ 0
z : S
zr : s.potential e z = r
zc : Critical (f e) z
⊢ e ∈ u

State before:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
r0 : r ≠ 0
z : S
zr : s.potential e z = r
zc : Critical (f e) z
⊢ e ∈ u
Tactic:
rw [← zr, Ne, s.potential_eq_zero_of_onePreimage] at r0
State after:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ e ∈ u

State before:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ e ∈ u
Tactic:
rw [mem_image]
State after:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ ∃ x ∈ t, x.1 = e

State before:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ ∃ x ∈ t, x.1 = e
Tactic:
refine ⟨(e, z), ⟨?_, zc, r0⟩, rfl⟩
State after:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ s.potential (e, z).1 (e, z).2 ≤ q

State before:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ s.potential (e, z).1 (e, z).2 ≤ q
Tactic:
simp only [zr]
State after:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ r ≤ q

State before:
case neg.intro.intro.inr.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h✝ : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
e : ℂ
h : s.p e ≤ p
r : ℝ
rq : r < q
z : S
r0 : ¬z = a
zr : s.potential e z = r
zc : Critical (f e) z
⊢ r ≤ q
Tactic:
exact rq.le
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
⊢ s.p c ≤ q
Tactic:
rcases(mem_image _ _ _).mp m with ⟨⟨c', z⟩, ⟨zp, zc, za⟩, cc⟩
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : (c', z).1 = c
zp : s.potential (c', z).1 (c', z).2 ≤ q
zc : Critical (f (c', z).1) (c', z).2
za : (c', z).2 ≠ a
⊢ s.p c ≤ q

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : (c', z).1 = c
zp : s.potential (c', z).1 (c', z).2 ≤ q
zc : Critical (f (c', z).1) (c', z).2
za : (c', z).2 ≠ a
⊢ s.p c ≤ q
Tactic:
simp only at cc za zc zp
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : c' = c
zp : s.potential c' z ≤ q
zc : Critical (f c') z
za : z ≠ a
⊢ s.p c ≤ q

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : c' = c
zp : s.potential c' z ≤ q
zc : Critical (f c') z
za : z ≠ a
⊢ s.p c ≤ q
Tactic:
simp only [cc] at za zc zp
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : c' = c
za : z ≠ a
zc : Critical (f c) z
zp : s.potential c z ≤ q
⊢ s.p c ≤ q

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
c' : ℂ
z : S
cc : c' = c
za : z ≠ a
zc : Critical (f c) z
zp : s.potential c z ≤ q
⊢ s.p c ≤ q
Tactic:
clear cc c'
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
za : z ≠ a
zc : Critical (f c) z
zp : s.potential c z ≤ q
⊢ s.p c ≤ q

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
za : z ≠ a
zc : Critical (f c) z
zp : s.potential c z ≤ q
⊢ s.p c ≤ q
Tactic:
simp only [Ne, ← s.potential_eq_zero_of_onePreimage c] at za
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.p c ≤ q

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.p c ≤ q
Tactic:
refine _root_.trans (csInf_le s.bddBelow_ps ?_) zp
State after:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.potential c z ∈ s.ps c

State before:
case intro.mk.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.potential c z ∈ s.ps c
Tactic:
right
State after:
case intro.mk.intro.intro.intro.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.potential c z ≠ 0 ∧ ∃ z_1, s.potential c z_1 = s.potential c z ∧ Critical (f c) z_1

State before:
case intro.mk.intro.intro.intro.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✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
p : ℝ
h : ∃ᶠ (x : ℂ) in 𝓝 c, s.p x ≤ p
q : ℝ
pq : p < q
q1 : q < 1
t : Set (ℂ × S) := {x | s.potential x.1 x.2 ≤ q ∧ Critical (f x.1) x.2 ∧ x.2 ≠ a}
ct : IsClosed t
u : Set ℂ := Prod.fst '' t
cu : IsClosed u
m : c ∈ u
z : S
zc : Critical (f c) z
zp : s.potential c z ≤ q
za : ¬s.potential c z = 0
⊢ s.potential c z ≠ 0 ∧ ∃ z_1, s.potential c z_1 = s.potential c z ∧ Critical (f c) z_1
Tactic:
use za, z, rfl, zc
State after:
no goals