internlm/Lean-Github huggingface dataset:
Theorem: Super.f_noncritical_near_a
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun x => f e (↑(extChartAt I a).symm x)) (↑(extChartAt I a) 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Tactic:
apply (s.fa _).along_snd.comp
Proof state after:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun x => ↑(extChartAt I a).symm x) (↑(extChartAt I a) 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Theorem: Super.f_noncritical_near_a
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun x => ↑(extChartAt I a).symm x) (↑(extChartAt I a) 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Tactic:
exact HolomorphicAt.extChartAt_symm (PartialEquiv.map_source _ zm)
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Theorem: Super.f_noncritical_near_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Tactic:
simp only [PartialEquiv.left_inv _ zm, s.f0]
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e z ∈ (extChartAt I a).source
Theorem: Super.f_noncritical_near_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e z ∈ (extChartAt I a).source
Tactic:
exact ezm
Proof state after:
no goals
Theorem: Super.f_noncritical_near_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
apply DifferentiableAt.comp
Proof state after:
case hg
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)

case hf
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Theorem: Super.f_noncritical_near_a
Proof state before:
case hg
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)

case hf
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
simp only [sub_add_cancel, dg]
Proof state after:
case hf
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Theorem: Super.f_noncritical_near_a
Proof state before:
case hf
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
exact differentiableAt_id.add (differentiableAt_const _)
Proof state after:
no goals
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a) *
        deriv (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Tactic:
simp only [deriv_add_const, deriv_sub_const, deriv_id'', mul_one, sub_add_cancel, Function.comp]
Proof state after:
no goals
Theorem: Super.f_noncritical_near_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)
Tactic:
simp only [sub_add_cancel, dg]
Proof state after:
no goals
Theorem: Super.f_noncritical_near_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
exact differentiableAt_id.add (differentiableAt_const _)
Proof state after:
no goals
Theorem: Super.isClosed_critical_not_a
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 : S
d n : ℕ
s : Super f d a
⊢ IsClosed {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}
Tactic:
rw [← isOpen_compl_iff]
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 : S
d n : ℕ
s : Super f d a
⊢ IsOpen {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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 : S
d n : ℕ
s : Super f d a
⊢ IsOpen {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
rw [isOpen_iff_eventually]
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 : S
d n : ℕ
s : Super f d a
⊢ ∀ x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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 : S
d n : ℕ
s : Super f d a
⊢ ∀ x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
intro ⟨c, z⟩ m
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
by_cases za : z = a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ 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
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
rw [za]
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, a), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, a), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
refine (s.f_noncritical_near_a c).mp (eventually_of_forall ?_)
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ (x : ℂ × S), (Critical (f x.1) x.2 ↔ x.2 = a) → x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ (x : ℂ × S), (Critical (f x.1) x.2 ↔ x.2 = a) → x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
intro ⟨e, w⟩ h
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f (e, w).1) (e, w).2 ↔ (e, w).2 = a
⊢ (e, w) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f (e, w).1) (e, w).2 ↔ (e, w).2 = a
⊢ (e, w) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
simp only [mem_compl_iff, mem_setOf, not_and, not_not] at h ⊢
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f e) w ↔ w = a
⊢ Critical (f e) w → w = a
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f e) w ↔ w = a
⊢ Critical (f e) w → w = a
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
have o := isOpen_iff_eventually.mp (isOpen_noncritical s.fa)
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
o : ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
o : ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
simp only [za, mem_compl_iff, mem_setOf, not_and, not_not, imp_false] at m o ⊢
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), Critical (f y.1) y.2 → y.2 = a
Theorem: Super.isClosed_critical_not_a
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), Critical (f y.1) y.2 → y.2 = a
Tactic:
refine (o (c, z) m).mp (eventually_of_forall ?_)
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → Critical (f x.1) x.2 → x.2 = a