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

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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ mfderiv (I.prod I') I'' f p =
    (mfderiv (I.prod I') I'' f (p.1, p.2)).comp
      ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
        ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)))

Tactic:
symm

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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ (mfderiv (I.prod I') I'' f (p.1, p.2)).comp
      ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
        ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2))) =
    mfderiv (I.prod I') I'' f p

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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ (mfderiv (I.prod I') I'' f (p.1, p.2)).comp
      ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
        ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2))) =
    mfderiv (I.prod I') I'' f p

Tactic:
convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2)

Result:
case h.e'_2.h.e'_24
𝕜 : 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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
      ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ mfderiv (I.prod I') I'' f p =
    mfderiv (I.prod I') I'' (fun z => f (z.1, p.2)) p + mfderiv (I.prod I') I'' (fun z => f (p.1, z.2)) p

Tactic:
erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prod_mk mdifferentiableAt_const) rfl,
  mfderiv_comp_of_eq hf (mdifferentiableAt_const.prod_mk mdifferentiableAt_snd) rfl,
  ← ContinuousLinearMap.comp_add,
  mdifferentiableAt_fst.mfderiv_prod mdifferentiableAt_const,
  mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_snd, mfderiv_fst,
  mfderiv_snd, mfderiv_const, mfderiv_const]

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'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ mfderiv (I.prod I') I'' f p =
    (mfderiv (I.prod I') I'' f (p.1, p.2)).comp
      ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
        ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)))