Theorem: ComplexInverseFun.Cinv.fa' (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
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
have fa := i.fa
State after:
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
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ AnalyticAt ℂ i.f' (c, i.z')

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
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
simp only [holomorphicAt_iff, uncurry, extChartAt_prod, Function.comp, PartialEquiv.prod_coe_symm,
  PartialEquiv.prod_coe] at fa
State after:
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
fa :
  ContinuousAt (uncurry f) (c, z) ∧
    AnalyticAt ℂ (fun x => ↑(extChartAt I (f c z)) (f (↑(extChartAt I c).symm x.1) (↑(extChartAt I z).symm x.2)))
      (↑(extChartAt I c) c, ↑(extChartAt I z) z)
⊢ AnalyticAt ℂ i.f' (c, i.z')

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
fa :
  ContinuousAt (uncurry f) (c, z) ∧
    AnalyticAt ℂ (fun x => ↑(extChartAt I (f c z)) (f (↑(extChartAt I c).symm x.1) (↑(extChartAt I z).symm x.2)))
      (↑(extChartAt I c) c, ↑(extChartAt I z) z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
exact fa.2
State after:
no goals