Theorem: MDifferentiableAt.hasMFDerivAt_uncurry (Ray/AnalyticManifold/AnalyticManifold.lean)

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
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
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z)
    (df0.comp (ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)) +
      df1.comp (ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)))
Tactic:
set fst := ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
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
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)
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z)
    (df0.comp fst + df1.comp (ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)))

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
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)
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z)
    (df0.comp fst + df1.comp (ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)))
Tactic:
set snd := ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
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
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)
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)

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
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)
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
generalize hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
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
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
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)

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
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
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
have fh := fd.hasMFDerivAt
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
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) (mfderiv (J.prod K) L (uncurry f) (y, z))
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)

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
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) (mfderiv (J.prod K) L (uncurry f) (y, z))
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
rw [hdf] at fh
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
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
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)

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
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
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
suffices e : df = df0.comp fst + df1.comp snd by rw [e] at fh; exact fh
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
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
⊢ df = df0.comp fst + df1.comp snd

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
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
⊢ df = df0.comp fst + df1.comp snd
Tactic:
apply ContinuousLinearMap.ext
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
⊢ ∀ (x : TangentSpace (J.prod K) (y, z)), df x = (df0.comp fst + df1.comp snd) x

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
⊢ ∀ (x : TangentSpace (J.prod K) (y, z)), df x = (df0.comp fst + df1.comp snd) x
Tactic:
intro ⟨u, v⟩
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
⊢ df (u, v) = (df0.comp fst + df1.comp snd) (u, v)

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
⊢ df (u, v) = (df0.comp fst + df1.comp snd) (u, v)
Tactic:
simp only [Function.uncurry_apply_pair, ContinuousLinearMap.add_apply,
  ContinuousLinearMap.comp_apply]
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
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))

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
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
have hu : ∀ u : TangentSpace J y, df (u, 0) = df0 u := by
  intro u
  have d : HasMFDerivAt J L (uncurry f ∘ fun x ↦ (x, z)) y
      (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0)) :=
    fh.comp y ((hasMFDerivAt_id _ _).prod (hasMFDerivAt_const _ _ _ _))
  simp only [hasMFDerivAt_unique fh0 d]
  refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm
  refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm
  simp only [ContinuousLinearMap.zero_apply, Prod.mk.injEq, and_true]
  exact rfl
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
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))

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⟩
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))

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
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
have e : (u, v) = (u, 0) + (0, v) := by simp only [Prod.mk_add_mk, add_zero, zero_add]
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
e : (u, v) = (u, 0) + (0, v)
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))

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
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
e : (u, v) = (u, 0) + (0, v)
⊢ df (u, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
nth_rw 1 [e]
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
e : (u, v) = (u, 0) + (0, v)
⊢ df ((u, 0) + (0, v)) = df0 (fst (u, v)) + df1 (snd (u, v))

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
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
e : (u, v) = (u, 0) + (0, v)
⊢ df ((u, 0) + (0, v)) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
rw [map_add]
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
e : (u, v) = (u, 0) + (0, v)
⊢ df (u, 0) + df (0, v) = df0 (fst (u, v)) + df1 (snd (u, v))

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
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
e : (u, v) = (u, 0) + (0, v)
⊢ df (u, 0) + df (0, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
exact congr_arg₂ _ (hu u) (hv v)
State after:
no goals

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
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
e : df = df0.comp fst + df1.comp snd
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
rw [e] at fh
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
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) (df0.comp fst + df1.comp snd)
e : df = df0.comp fst + df1.comp snd
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)

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
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) (df0.comp fst + df1.comp snd)
e : df = df0.comp fst + df1.comp snd
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
exact fh
State after:
no goals

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
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
⊢ ∀ (u : TangentSpace J y), df (u, 0) = df0 u
Tactic:
intro u
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
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
u : TangentSpace J y
⊢ df (u, 0) = df0 u

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
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
u : TangentSpace J y
⊢ df (u, 0) = df0 u
Tactic:
have d : HasMFDerivAt J L (uncurry f ∘ fun x ↦ (x, z)) y
    (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0)) :=
  fh.comp y ((hasMFDerivAt_id _ _).prod (hasMFDerivAt_const _ _ _ _))
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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ df (u, 0) = df0 u

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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ df (u, 0) = df0 u
Tactic:
simp only [hasMFDerivAt_unique fh0 d]
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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ df (u, 0) = (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0)) u

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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ df (u, 0) = (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0)) u
Tactic:
refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm
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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ (u, 0) = ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0) u

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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ (u, 0) = ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0) u
Tactic:
refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm
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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ (u, 0) = ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)) u, 0 u)

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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ (u, 0) = ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)) u, 0 u)
Tactic:
simp only [ContinuousLinearMap.zero_apply, Prod.mk.injEq, and_true]
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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ u = (ContinuousLinearMap.id 𝕜 (TangentSpace J y)) u

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
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
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ u = (ContinuousLinearMap.id 𝕜 (TangentSpace J y)) u
Tactic:
exact rfl
State after:
no goals

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
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
⊢ ∀ (v : TangentSpace K z), df (0, v) = df1 v
Tactic:
intro v
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
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
v : TangentSpace K z
⊢ df (0, v) = df1 v

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
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
v : TangentSpace K z
⊢ df (0, v) = df1 v
Tactic:
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 _ _))
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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ df (0, v) = df1 v

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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ df (0, v) = df1 v
Tactic:
rw [hasMFDerivAt_unique fh1 d]
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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ df (0, v) = (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z)))) v

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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ df (0, v) = (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z)))) v
Tactic:
refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm
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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ (0, v) = (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))) v

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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ (0, v) = (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))) v
Tactic:
refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm
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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ (0, v) = (0 v, (ContinuousLinearMap.id 𝕜 (TangentSpace K z)) v)

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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ (0, v) = (0 v, (ContinuousLinearMap.id 𝕜 (TangentSpace K z)) v)
Tactic:
simp only [Prod.mk.injEq]
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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ 0 = 0 v ∧ v = (ContinuousLinearMap.id 𝕜 (TangentSpace K z)) v

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
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
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ 0 = 0 v ∧ v = (ContinuousLinearMap.id 𝕜 (TangentSpace K z)) v
Tactic:
exact ⟨(ContinuousLinearMap.zero_apply _).symm, rfl⟩
State after:
no goals

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
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
⊢ (u, v) = (u, 0) + (0, v)
Tactic:
simp only [Prod.mk_add_mk, add_zero, zero_add]
State after:
no goals