internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
Tactic:
apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      (fun w =>
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
          x =
        f x
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      (fun w =>
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
          x =
        f x
Tactic:
apply (n.holomorphicAt.continuousAt.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        (fun w =>
              ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
                (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
            x =
          f x
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        (fun w =>
              ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
                (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
            x =
          f x
Tactic:
refine eventually_of_forall fun w fm m ↦ ?_
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ (fun w =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
      w =
    f w
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ (fun w =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
      w =
    f w
Tactic:
simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ fm]
Proof state after:
no goals
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)
⊢ 𝓝 (c, f c z) = Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
refine le_antisymm ?_ (continuousAt_fst.prod fa.continuousAt)
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)
⊢ 𝓝 (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)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
generalize hg : (fun e x ↦ extChartAt I (f c z) (f e ((extChartAt I z).symm x))) = g
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
⊢ 𝓝 (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
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
have ga : AnalyticAt ℂ (uncurry g) (c, extChartAt I z z) := by
  rw [← hg]; exact (holomorphicAt_iff.mp fa).2
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)
⊢ 𝓝 (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)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
have gn : NontrivialHolomorphicAt (g c) (extChartAt I z z) := by rw [← hg]; exact n.inCharts
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)
⊢ 𝓝 (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)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
have h := gn.nhds_le_map_nhds_param' ga
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 : 𝓝 (c, g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) 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 : 𝓝 (c, g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
simp only [nhds_prod_eq, ← extChartAt_map_nhds' I z, Filter.map_map, Filter.prod_map_id_map_eq,
  Function.comp] at h
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 :
  𝓝 c ×ˢ 𝓝 (g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤
    Filter.map (fun x => (x.1, g x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2))) (𝓝 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 :
  𝓝 c ×ˢ 𝓝 (g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤
    Filter.map (fun x => (x.1, g x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2))) (𝓝 c ×ˢ 𝓝 z)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
replace h := @Filter.map_mono _ _ (fun p : ℂ × ℂ ↦ (p.1, (extChartAt I (f c z)).symm p.2)) _ _ h
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 ×ˢ 𝓝 (g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map (fun x => (x.1, g x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2))) (𝓝 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 ×ˢ 𝓝 (g c (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) ≤
    Filter.map (fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2))
      (Filter.map (fun x => (x.1, g x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2))) (𝓝 c ×ˢ 𝓝 z))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
simp only [← hg] at h
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 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(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))
⊢ 𝓝 (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 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(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))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
rw [PartialEquiv.left_inv _ (mem_extChartAt_source I z)] at h
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))
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))