Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic (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.prod I) ↑i.he.symm (c, i.fz')
Tactic:
apply AnalyticAt.holomorphicAt
State after:
case fa
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.he.symm (c, i.fz')

State before:
case fa
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.he.symm (c, i.fz')
Tactic:
have d : ContDiffAt ℂ ⊤ i.he.symm _ :=
  ContDiffAt.to_localInverse i.ha.contDiffAt i.has_dhe le_top
State after:
case fa
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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')

State before:
case fa
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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
have e : i.h (c, i.z') = (c, i.fz') := by
  simp only [Cinv.h, Cinv.fz', Cinv.f']
  simp only [Cinv.z', (extChartAt I z).left_inv (mem_extChartAt_source _ _)]
State after:
case fa
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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')

State before:
case fa
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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
rw [e] at d
State after:
case fa
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
d : ContDiffAt ℂ ⊤ ↑i.he.symm (c, i.fz')
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')

State before:
case fa
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
d : ContDiffAt ℂ ⊤ ↑i.he.symm (c, i.fz')
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
exact (contDiffAt_iff_analytic_at2 le_top).mp d
State after:
no goals

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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ i.h (c, i.z') = (c, i.fz')
Tactic:
simp only [Cinv.h, Cinv.fz', Cinv.f']
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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ (c, ↑(extChartAt I (f c z)) (f c (↑(extChartAt I z).symm i.z'))) = (c, ↑(extChartAt I (f c z)) (f c 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
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ (c, ↑(extChartAt I (f c z)) (f c (↑(extChartAt I z).symm i.z'))) = (c, ↑(extChartAt I (f c z)) (f c z))
Tactic:
simp only [Cinv.z', (extChartAt I z).left_inv (mem_extChartAt_source _ _)]
State after:
no goals