-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderiv_prod_eq_add_apply {f : M × M' → M''} {p : M × M'} {v : TangentSpace (I.prod I') p}
    (hf : MDifferentiableAt (I.prod I') I'' f p) :
    mfderiv (I.prod I') I'' f p v =
      mfderiv I I'' (fun z : M => f (z, p.2)) p.1 v.1 +
      mfderiv I' I'' (fun z : M' => f (p.1, z)) p.2 v.2

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
v : TangentSpace (I.prod I') p
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ (mfderiv (I.prod I') I'' f p) v =
    (mfderiv I I'' (fun z => f (z, p.2)) p.1) v.1 + (mfderiv I' I'' (fun z => f (p.1, z)) p.2) v.2

Tactic:
rw [mfderiv_prod_eq_add_comp hf]

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
v : TangentSpace (I.prod I') p
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ ((mfderiv I I'' (fun z => f (z, p.2)) p.1).comp (id (ContinuousLinearMap.fst 𝕜 E E')) +
        (mfderiv I' I'' (fun z => f (p.1, z)) p.2).comp (id (ContinuousLinearMap.snd 𝕜 E E')))
      v =
    (mfderiv I I'' (fun z => f (z, p.2)) p.1) v.1 + (mfderiv I' I'' (fun z => f (p.1, z)) p.2) v.2

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
v : TangentSpace (I.prod I') p
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ ((mfderiv I I'' (fun z => f (z, p.2)) p.1).comp (id (ContinuousLinearMap.fst 𝕜 E E')) +
        (mfderiv I' I'' (fun z => f (p.1, z)) p.2).comp (id (ContinuousLinearMap.snd 𝕜 E E')))
      v =
    (mfderiv I I'' (fun z => f (z, p.2)) p.1) v.1 + (mfderiv I' I'' (fun z => f (p.1, z)) p.2) v.2

Tactic:
rfl

Result:
no goals