Theorem: osgoodManifold
Proof state before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
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 ↦ ⟨?_, ?_, ?_⟩)
Proof 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