internlm/Lean-Github huggingface dataset:
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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⟩
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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]
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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⟩
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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]
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
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
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⟩
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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'
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof 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
Theorem: Super.lowerSemicontinuous_p
Proof 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
Proof state after:
no goals
Theorem: Postcritical.not_precritical
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 : Super f d a
p : Postcritical s c z
p0 : s.potential c z ≠ 0
⊢ ¬Precritical (f c) z
Tactic:
contrapose p
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 : Super f d a
p0 : s.potential c z ≠ 0
p : ¬¬Precritical (f c) z
⊢ ¬Postcritical s c z
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
p : ¬¬Precritical (f c) z
⊢ ¬Postcritical s c z
Tactic:
simp only [Postcritical, not_not, not_forall, not_lt] at p ⊢
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 : Super f d a
p0 : s.potential c z ≠ 0
p : Precritical (f c) z
⊢ s.p c ≤ s.potential c z
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
p : Precritical (f c) z
⊢ s.p c ≤ s.potential c z
Tactic:
rcases p with ⟨n, p⟩
Proof 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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c z
Theorem: Postcritical.not_precritical
Proof 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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c z
Tactic:
trans s.potential c ((f c)^[n] z)
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c ((f c)^[n] z)

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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≤ s.potential c z
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c ((f c)^[n] z)
Tactic:
refine csInf_le s.bddBelow_ps (Or.inr ⟨?_, (f c)^[n] z, rfl, p⟩)
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≠ 0
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≠ 0
Tactic:
simp only [s.potential_eqn_iter]
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≠ 0
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≠ 0
Tactic:
exact pow_ne_zero _ p0
Proof state after:
no goals
Theorem: Postcritical.not_precritical
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≤ s.potential c z
Tactic:
simp only [s.potential_eqn_iter]
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≤ s.potential c z