Theorem: osgoodManifold (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Holomorphic (I.prod I) I f
Tactic:
rw [holomorphic_iff]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Continuous f ∧
    ∀ (x : S × T),
      AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ Continuous f ∧
    ∀ (x : S × T),
      AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Tactic:
use fc
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ ∀ (x : S × T),
    AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
⊢ ∀ (x : S × T),
    AnalyticAt ℂ (↑(extChartAt I (f x)) ∘ f ∘ ↑(extChartAt (I.prod I) x).symm) (↑(extChartAt (I.prod I) x) x)
Tactic:
intro p
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ AnalyticAt ℂ (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p)

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ AnalyticAt ℂ (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p)
Tactic:
apply osgood_at'
State after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2

State before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Tactic:
have fm : ∀ᶠ q in 𝓝 (extChartAt II p p),
    f ((extChartAt II p).symm q) ∈ (extChartAt I (f p)).source := by
  refine (fc.continuousAt.comp (continuousAt_extChartAt_symm II p)).eventually_mem
      ((isOpen_extChartAt_source I (f p)).mem_nhds ?_)
  simp only [Function.comp, (extChartAt II p).left_inv (mem_extChartAt_source _ _)]
  apply mem_extChartAt_source
State after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2

State before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Tactic:
apply ((isOpen_extChartAt_target II p).eventually_mem (mem_extChartAt_target II p)).mp
State after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    x ∈ (extChartAt (I.prod I) p).target →
      ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
          AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2

State before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    x ∈ (extChartAt (I.prod I) p).target →
      ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
          AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Tactic:
refine fm.mp (eventually_of_forall fun q fm m ↦ ⟨?_, ?_, ?_⟩)
State after:
case right.h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) q

case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1

case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
Tactic:
refine (fc.continuousAt.comp (continuousAt_extChartAt_symm II p)).eventually_mem
    ((isOpen_extChartAt_source I (f p)).mem_nhds ?_)
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ (f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p) ∈ (extChartAt I (f p)).source

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ (f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p) ∈ (extChartAt I (f p)).source
Tactic:
simp only [Function.comp, (extChartAt II p).left_inv (mem_extChartAt_source _ _)]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ f p ∈ (extChartAt I (f p)).source

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ f p ∈ (extChartAt I (f p)).source
Tactic:
apply mem_extChartAt_source
State after:
no goals

State before:
case right.h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) q
Tactic:
exact (continuousAt_extChartAt' I fm).comp_of_eq
    (fc.continuousAt.comp (continuousAt_extChartAt_symm'' _ m)) rfl
State after:
no goals

State before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
apply HolomorphicAt.analyticAt I I
State after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1

State before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
refine (HolomorphicAt.extChartAt fm).comp_of_eq ?_ rfl
State after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1

State before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
rw [extChartAt_prod] at m
State after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1

State before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
simp only [Function.comp, extChartAt_prod, PartialEquiv.prod_symm, PartialEquiv.prod_coe,
  PartialEquiv.prod_target, mem_prod_eq] at m ⊢
State after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm z, ↑(extChartAt I p.2).symm q.2)) q.1

State before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm z, ↑(extChartAt I p.2).symm q.2)) q.1
Tactic:
exact (f0 _ _).comp (HolomorphicAt.extChartAt_symm m.1)
State after:
no goals

State before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
apply HolomorphicAt.analyticAt I I
State after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2

State before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
refine (HolomorphicAt.extChartAt fm).comp_of_eq ?_ rfl
State after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2

State before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
rw [extChartAt_prod] at m
State after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2

State before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
simp only [Function.comp, extChartAt_prod, PartialEquiv.prod_symm, PartialEquiv.prod_coe,
  PartialEquiv.prod_target, mem_prod_eq] at m ⊢
State after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm q.1, ↑(extChartAt I p.2).symm z)) q.2

State before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm q.1, ↑(extChartAt I p.2).symm z)) q.2
Tactic:
exact (f1 _ _).comp (HolomorphicAt.extChartAt_symm m.2)
State after:
no goals