internlm/Lean-Github huggingface dataset:
Theorem: Super.ps_pos
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
p : ℝ
m : p ∈ s.ps c
⊢ 0 < p
Tactic:
cases' m with m m
Proof state after:
case 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
c : ℂ
p : ℝ
m : p = 1
⊢ 0 < p

case 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
c : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Theorem: Super.ps_pos
Proof state before:
case 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
c : ℂ
p : ℝ
m : p = 1
⊢ 0 < p

case 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
c : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Tactic:
simp only [m, zero_lt_one]
Proof state after:
case 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
c : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Theorem: Super.ps_pos
Proof state before:
case 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
c : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Tactic:
rcases m with ⟨p0, z, e, c⟩
Proof state after:
case 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
c✝ : ℂ
p : ℝ
p0 : p ≠ 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < p
Theorem: Super.ps_pos
Proof state before:
case 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
c✝ : ℂ
p : ℝ
p0 : p ≠ 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < p
Tactic:
rw [← e] at p0 ⊢
Proof state after:
case 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
c✝ : ℂ
p : ℝ
z : S
p0 : s.potential c✝ z ≠ 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < s.potential c✝ z
Theorem: Super.ps_pos
Proof state before:
case 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
c✝ : ℂ
p : ℝ
z : S
p0 : s.potential c✝ z ≠ 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < s.potential c✝ z
Tactic:
exact p0.symm.lt_of_le s.potential_nonneg
Proof state after:
no goals
Theorem: Super.mem_ps
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ s.ps c
Tactic:
rw [← s.compact_ps.isClosed.closure_eq]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ closure (s.ps c)
Theorem: Super.mem_ps
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ closure (s.ps c)
Tactic:
exact csInf_mem_closure s.nonempty_ps s.bddBelow_ps
Proof state after:
no goals
Theorem: Super.lowerSemicontinuous_p
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
⊢ LowerSemicontinuous s.p
Tactic:
intro c p h
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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'
Theorem: Super.lowerSemicontinuous_p
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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
Theorem: Super.lowerSemicontinuous_p
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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 ⊢
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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
Theorem: Super.lowerSemicontinuous_p
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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'
Proof state after:
case H
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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
Theorem: Super.lowerSemicontinuous_p
Proof state before:
case H
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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'
Proof state after:
case H
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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'
Theorem: Super.lowerSemicontinuous_p
Proof state before:
case H
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z 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⟩
Proof 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'
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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'
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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}
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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 ↦ ?_)
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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⟩
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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