internlm/Lean-Github huggingface dataset:
Theorem: mfderiv_ne_zero_eventually'
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
f0 : ¬deriv (g (c, z).1) (↑(extChartAt I z) (c, z).2) ≠ 0
⊢ ¬mfderiv I I (f c) z ≠ 0
Tactic:
simp only [not_not, Function.comp] at f0 ⊢
Proof state after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ mfderiv I I (f c) z = 0
Theorem: mfderiv_ne_zero_eventually'
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ mfderiv I I (f c) z = 0
Tactic:
rw [g0.self_of_nhds]
Proof state after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ deriv (inChart f c z (c, z).1) (↑(extChartAt I z) (c, z).2) = 0
Theorem: mfderiv_ne_zero_eventually'
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ deriv (inChart f c z (c, z).1) (↑(extChartAt I z) (c, z).2) = 0
Tactic:
exact f0
Proof state after:
no goals
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
set c : ℂ := 0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
set g : ℂ → S → T := fun _ z ↦ f z
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
have ga : HolomorphicAt II I (uncurry g) (c, z) := by
  have e : uncurry g = f ∘ fun p ↦ p.2 := rfl; rw [e]
  apply HolomorphicAt.comp_of_eq fa holomorphicAt_snd; simp only
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
have pc : Tendsto (fun z ↦ (c, z)) (𝓝 z) (𝓝 (c, z)) := continuousAt_const.prod continuousAt_id
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
pc : Tendsto (fun z => (c, z)) (𝓝 z) (𝓝 (c, z))
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
pc : Tendsto (fun z => (c, z)) (𝓝 z) (𝓝 (c, z))
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
exact pc.eventually (mfderiv_ne_zero_eventually' ga f0)
Proof state after:
no goals
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)
Tactic:
have e : uncurry g = f ∘ fun p ↦ p.2 := rfl
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)
Tactic:
rw [e]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (f ∘ fun p => p.2) (c, z)
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (f ∘ fun p => p.2) (c, z)
Tactic:
apply HolomorphicAt.comp_of_eq fa holomorphicAt_snd
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ (c, z).2 = z
Theorem: mfderiv_ne_zero_eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ (c, z).2 = z
Tactic:
simp only
Proof state after:
no goals
Theorem: isOpen_noncritical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
⊢ IsOpen {p | ¬Critical (f p.1) p.2}
Tactic:
rw [isOpen_iff_eventually]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
⊢ ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
Theorem: isOpen_noncritical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
⊢ ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
Tactic:
intro ⟨c, z⟩ m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : ℂ
z : S
m : (c, z) ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | ¬Critical (f p.1) p.2}
Theorem: isOpen_noncritical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : ℂ
z : S
m : (c, z) ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | ¬Critical (f p.1) p.2}
Tactic:
exact mfderiv_ne_zero_eventually' (fa _) m
Proof state after:
no goals
Theorem: isClosed_critical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
have c := (isOpen_noncritical fa).isClosed_compl
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {p | ¬Critical (f p.1) p.2}ᶜ
⊢ IsClosed {p | Critical (f p.1) p.2}
Theorem: isClosed_critical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {p | ¬Critical (f p.1) p.2}ᶜ
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
simp only [compl_setOf, not_not] at c
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {a | Critical (f a.1) a.2}
⊢ IsClosed {p | Critical (f p.1) p.2}
Theorem: isClosed_critical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {a | Critical (f a.1) a.2}
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
exact c
Proof state after:
no goals
Theorem: osgoodManifold
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Holomorphic (I.prod I) I f
Tactic:
rw [holomorphic_iff]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Continuous f ∧
    ∀ (x : S × T),
      AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Theorem: osgoodManifold
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Continuous f ∧
    ∀ (x : S × T),
      AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Tactic:
use fc
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ ∀ (x : S × T),
    AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Theorem: osgoodManifold
Proof state before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ ∀ (x : S × T),
    AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Tactic:
intro p
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ AnalyticAt ℂ (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p)
Theorem: osgoodManifold
Proof state before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ AnalyticAt ℂ (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p)
Tactic:
apply osgood_at'
Proof state after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Theorem: osgoodManifold
Proof state before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Tactic:
have fm : ∀ᶠ q in 𝓝 (extChartAt II p p),
    f ((extChartAt II p).symm q) ∈ (extChartAt I (f p)).source := by
  refine (fc.continuousAt.comp (continuousAt_extChartAt_symm II p)).eventually_mem
      ((isOpen_extChartAt_source I (f p)).mem_nhds ?_)
  simp only [Function.comp, (extChartAt II p).left_inv (mem_extChartAt_source _ _)]
  apply mem_extChartAt_source
Proof state after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2