internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
have pe := Filter.prod_map_id_map_eq (f := 𝓝 c) (g := 𝓝 (extChartAt I (f c z) (f c z)))
  (m := fun x ↦ (extChartAt I (f c z)).symm x)
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 c ×ˢ Filter.map (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm x) (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 c ×ˢ Filter.map (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm x) (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
rw [extChartAt_symm_map_nhds', ←nhds_prod_eq] at pe
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 (c, f c z) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 (c, f c z) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
refine _root_.trans (le_of_eq pe) (_root_.trans h (le_of_eq ?_))
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 (c, f c z) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z))
pe :
  𝓝 (c, f c z) =
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (𝓝 c ×ˢ 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f c z)))
⊢ Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
clear h pe
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map
        (fun x =>
          (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
        (𝓝 c ×ˢ 𝓝 z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
rw [←nhds_prod_eq, Filter.map_map]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ Filter.map
      ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (𝓝 (c, z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ Filter.map
      ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (𝓝 (c, z)) =
    Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
apply Filter.map_congr
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (𝓝 (c, z)).EventuallyEq
    ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
      (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
    fun p => (p.1, f p.1 p.2)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (𝓝 (c, z)).EventuallyEq
    ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
      (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
    fun p => (p.1, f p.1 p.2)
Tactic:
apply ((isOpen_extChartAt_source II (c, z)).eventually_mem (mem_extChartAt_source II (c, z))).mp
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
      ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
            (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
          x =
        (fun p => (p.1, f p.1 p.2)) x
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
      ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
            (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
          x =
        (fun p => (p.1, f p.1 p.2)) x
Tactic:
apply (fa.continuousAt.eventually_mem (extChartAt_source_mem_nhds I (f c z))).mp
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    uncurry f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source →
      x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
        ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
              (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
            x =
          (fun p => (p.1, f p.1 p.2)) x
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    uncurry f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source →
      x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
        ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
              (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
            x =
          (fun p => (p.1, f p.1 p.2)) x
Tactic:
apply eventually_of_forall
Proof state after:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ (x : ℂ × S),
    uncurry f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source →
      x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
        ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
              (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
            x =
          (fun p => (p.1, f p.1 p.2)) x
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ (x : ℂ × S),
    uncurry f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source →
      x ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source →
        ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
              (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
            x =
          (fun p => (p.1, f p.1 p.2)) x
Tactic:
intro ⟨e, w⟩ fm m
Proof state after:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
e : ℂ
w : S
fm : uncurry f (e, w) ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : (e, w) ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source
⊢ ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (e, w) =
    (fun p => (p.1, f p.1 p.2)) (e, w)