Theorem: ComplexInverseFun.Cinv.ga (Ray/AnalyticManifold/Inverse.lean)

State before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (uncurry i.g) (c, f c z)
Tactic:
apply (HolomorphicAt.extChartAt_symm (mem_extChartAt_target I z)).comp_of_eq
State after:
case gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)

case e
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2 = ↑(extChartAt I z) z

State before:
case gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)
Tactic:
refine holomorphicAt_snd.comp (i.he_symm_holomorphic.comp_of_eq ?_ ?_)
State after:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)

case gh.refine_2
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) = (c, i.fz')

State before:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
apply holomorphicAt_fst.prod
State after:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)

State before:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Tactic:
refine (HolomorphicAt.extChartAt ?_).comp holomorphicAt_snd
State after:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ (c, f c z).2 ∈ (extChartAt I (f c z)).source

State before:
case gh.refine_1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ (c, f c z).2 ∈ (extChartAt I (f c z)).source
Tactic:
exact mem_extChartAt_source _ _
State after:
no goals

State before:
case gh.refine_2
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) = (c, i.fz')
Tactic:
rfl
State after:
no goals

State before:
case e
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2 = ↑(extChartAt I z) z
Tactic:
exact i.inv_at
State after:
no goals