Theorem: ComplexInverseFun.Cinv.has_df' (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
⊢ HasMFDerivAt (I.prod I) I i.f' (c, i.z') i.df'
Tactic:
apply HasMFDerivAt.comp (I' := I) (c, i.z')
State after:
case hg
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
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 (↑(extChartAt I z).symm (c, i.z').2)) i.de'

case hf
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
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z') i.df

State before:
case hg
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
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 (↑(extChartAt I z).symm (c, i.z').2)) i.de'
Tactic:
rw [i.zz]
State after:
case hg
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
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 z) i.de'

State before:
case hg
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
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 z) i.de'
Tactic:
exact (HolomorphicAt.extChartAt (mem_extChartAt_source _ _)).mdifferentiableAt.hasMFDerivAt
State after:
no goals

State before:
case hf
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
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z') i.df
Tactic:
simp only [Cinv.df]
State after:
case hf
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
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z')
    (i.dfc.comp dc + i.dfz.comp (i.de.comp dz))

State before:
case hf
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
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z')
    (i.dfc.comp dc + i.dfz.comp (i.de.comp dz))
Tactic:
apply MDifferentiableAt.hasMFDerivAt_comp2 (J := I) (co := cms)
State after:
case hf.fd
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
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, ↑(extChartAt I z).symm (c, i.z').2)

case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.fd
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
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, ↑(extChartAt I z).symm (c, i.z').2)

case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
rw [i.zz]
State after:
case hf.fd
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
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, z)

case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.fd
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
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, z)

case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact i.fa.mdifferentiableAt
State after:
case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
apply hasMFDerivAt_fst
State after:
case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
refine HasMFDerivAt.comp _ ?_ (hasMFDerivAt_snd _ _ _)
State after:
case hf.hh
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
⊢ HasMFDerivAt I I ↑(extChartAt I z).symm (c, i.z').2 i.de

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.hh
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
⊢ HasMFDerivAt I I ↑(extChartAt I z).symm (c, i.z').2 i.de

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt.hasMFDerivAt
State after:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
rw [i.zz]
State after:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y z) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y z) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact i.fa.along_fst.mdifferentiableAt.hasMFDerivAt
State after:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz

State before:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
rw [i.zz]
State after:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) z i.dfz

State before:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) z i.dfz
Tactic:
exact i.fa.along_snd.mdifferentiableAt.hasMFDerivAt
State after:
no goals