Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
case h
𝕜 : 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
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u : F
v : G
hu : ∀ (u : TangentSpace J y), df (u, 0) = df0 u
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
have hv : ∀ v : TangentSpace K z, df (0, v) = df1 v := by
  intro v
  have d : HasMFDerivAt K L (uncurry f ∘ fun x ↦ (y, x)) z (df.comp
      ((0 : TangentSpace K z →L[𝕜] TangentSpace J y).prod
        (ContinuousLinearMap.id 𝕜 (TangentSpace K z)))) :=
    fh.comp z ((hasMFDerivAt_const _ _ _ _).prod (hasMFDerivAt_id _ _))
  rw [hasMFDerivAt_unique fh1 d]
  refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm
  refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm
  simp only [Prod.mk.injEq]
  exact ⟨(ContinuousLinearMap.zero_apply _).symm, rfl⟩
Proof state after:
case h
𝕜 : 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
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u : F
v : G
hu : ∀ (u : TangentSpace J y), df (u, 0) = df0 u
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))