Theorem: ComplexInverseFun.Cinv.has_dh (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.prod I) i.h (c, i.z') i.dh
Tactic:
refine HasMFDerivAt.prod ?_ i.has_df'
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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

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 (fun y => y.1) (c, i.z') dc
Tactic:
apply hasMFDerivAt_fst
State after:
no goals