-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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'
g : M' → M''
p : TangentBundle I M
hg : MDifferentiableAt I' I'' g (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableAt I I' f (p.proj (E := TangentSpace I))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderiv I I'' (g ∘ f) (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I'' ((g ∘ f) (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderiv I' I'' g (f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
        (((mfderiv I I' f (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
have rw : Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
  (((ContinuousLinearMap.comp (M₂ := TangentSpace I' (f (p.proj (E := TangentSpace I))))
            (mfderiv I' I'' g (f (p.proj (E := TangentSpace I)))) (mfderiv I I' f (p.proj (E := TangentSpace I))) :
          ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
            (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
        (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
      (p.snd (E := TangentSpace I)) :
    TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
  (((mfderiv I' I'' g (f (p.proj (E := TangentSpace I))) :
          ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
            (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
        (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
      (((mfderiv I I' f (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I))) :
    TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
Tactic: rw [mfderiv_comp p.1 hg hf]