Theorem: MDifferentiableAt.hasMFDerivAt_comp2
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
g : M → N
h : M → O
x : M
fd : MDifferentiableAt (J.prod K) L (uncurry f) (g x, h x)
dg : TangentSpace I x →L[𝕜] TangentSpace J (g x)
gh : HasMFDerivAt I J g x dg
dh : TangentSpace I x →L[𝕜] TangentSpace K (h x)
hh : HasMFDerivAt I K h x dh
df0 : TangentSpace J (g x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh0 : HasMFDerivAt J L (fun y => f y (h x)) (g x) df0
df1 : TangentSpace K (h x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh1 : HasMFDerivAt K L (fun y => f (g x) y) (h x) df1
⊢ HasMFDerivAt I L (fun y => f (g y) (h y)) x (df0.comp dg + df1.comp dh)
Tactic:
have fh := (fd.hasMFDerivAt_uncurry fh0 fh1).comp x (gh.prod hh)
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
g : M → N
h : M → O
x : M
fd : MDifferentiableAt (J.prod K) L (uncurry f) (g x, h x)
dg : TangentSpace I x →L[𝕜] TangentSpace J (g x)
gh : HasMFDerivAt I J g x dg
dh : TangentSpace I x →L[𝕜] TangentSpace K (h x)
hh : HasMFDerivAt I K h x dh
df0 : TangentSpace J (g x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh0 : HasMFDerivAt J L (fun y => f y (h x)) (g x) df0
df1 : TangentSpace K (h x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh1 : HasMFDerivAt K L (fun y => f (g x) y) (h x) df1
fh :
  HasMFDerivAt I L (uncurry f ∘ fun y => (g y, h y)) x
    ((df0.comp (ContinuousLinearMap.fst 𝕜 (TangentSpace J (g x)) (TangentSpace K (h x))) +
          df1.comp (ContinuousLinearMap.snd 𝕜 (TangentSpace J (g x)) (TangentSpace K (h x)))).comp
      (dg.prod dh))
⊢ HasMFDerivAt I L (fun y => f (g y) (h y)) x (df0.comp dg + df1.comp dh)