Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param (Ray/AnalyticManifold/OpenMapping.lean)

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)
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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
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))

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)
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))

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
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))

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 ?_))
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))

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
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))

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]
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))

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
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)

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
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

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
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

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
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

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
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)

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)
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)
Tactic:
simp only [Function.comp, uncurry, extChartAt_prod, PartialEquiv.prod_source, mem_prod_eq] at fm m
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 : f e w ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : e ∈ (extChartAt 𝓘(ℂ, ℂ) c).source ∧ w ∈ (extChartAt 𝓘(ℂ, ℂ) 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)

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)
e : ℂ
w : S
fm : f e w ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : e ∈ (extChartAt 𝓘(ℂ, ℂ) c).source ∧ w ∈ (extChartAt 𝓘(ℂ, ℂ) 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)
Tactic:
simp only [Function.comp, PartialEquiv.left_inv _ m.2, PartialEquiv.left_inv _ fm]
State after:
no goals

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
⊢ AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
rw [← hg]
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
⊢ AnalyticAt ℂ (uncurry fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)

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
⊢ AnalyticAt ℂ (uncurry fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
exact (holomorphicAt_iff.mp fa).2
State after:
no goals

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)
⊢ NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
rw [← hg]
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)
⊢ NontrivialHolomorphicAt ((fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) c)
    (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

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)
⊢ NontrivialHolomorphicAt ((fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) c)
    (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
exact n.inCharts
State after:
no goals