-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
v : TangentSpace (I.prod I') p
hf : MDiffAt f p
⊢ (mfderiv% f p : (a : TangentSpace (I.prod I') p) → TangentSpace I'' (f p)) v =
    HAdd.hAdd (α := TangentSpace I'' (f (p.1, p.2))) (β := TangentSpace I'' (f (p.1, p.2)))
      ((((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1 :
              ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I p.1)
                (TangentSpace I'' (f (p.1, p.2)))) :
            (a : TangentSpace I p.1) → TangentSpace I'' (f (p.1, p.2)))
          v.1 :
        TangentSpace I'' (f (p.1, p.2)))
      ((((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2 :
              ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' p.2)
                (TangentSpace I'' (f (p.1, p.2)))) :
            (a : TangentSpace I' p.2) → TangentSpace I'' (f (p.1, p.2)))
          v.2 :
        TangentSpace I'' (f (p.1, p.2)))
have rw : (HAdd.hAdd (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) (β :=
        TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I p.1)
            ((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1) (id (ContinuousLinearMap.fst 𝕜 E E')) :
          TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2)))
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := TangentSpace I' p.2)
            ((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2) (id (ContinuousLinearMap.snd 𝕜 E E')) :
          TangentSpace (I.prod I') p →L[𝕜] TangentSpace I'' (f (p.1, p.2))) :
      (a : TangentSpace (I.prod I') p) → TangentSpace I'' (f p))
    v =
  HAdd.hAdd (α := TangentSpace I'' (f (p.1, p.2))) (β := TangentSpace I'' (f (p.1, p.2)))
    ((((mfderiv% fun (z : M) ↦ f (z, p.2)) p.1 :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I p.1)
              (TangentSpace I'' (f (p.1, p.2)))) :
          (a : TangentSpace I p.1) → TangentSpace I'' (f (p.1, p.2)))
        v.1 :
      TangentSpace I'' (f (p.1, p.2)))
    ((((mfderiv% fun (z : M') ↦ f (p.1, z)) p.2 :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' p.2)
              (TangentSpace I'' (f (p.1, p.2)))) :
          (a : TangentSpace I' p.2) → TangentSpace I'' (f (p.1, p.2)))
        v.2 :
      TangentSpace I'' (f (p.1, p.2)))
Tactic: rw [mfderiv_prod_eq_add_comp hf]