-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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'
s : Set M
g : M' → M''
u : Set M'
p : TangentBundle I M
hg : MDifferentiableWithinAt I' I'' g u (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableWithinAt I I' f s (p.proj (E := TangentSpace I))
h : s ⊆ f ⁻¹' u
hps : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
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))))
              (mfderivWithin I' I'' g u (f (p.proj (E := TangentSpace I))))
              (mfderivWithin I I' f s (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)))))
    (((mfderivWithin I' I'' g u (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)))
        (((mfderivWithin I I' f s (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)))))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderivWithin I I'' (g ∘ f) s (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)))))
    (((mfderivWithin I' I'' g u (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)))
        (((mfderivWithin I I' f s (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 [mfderivWithin_comp p.1 hg hf h hps]

Premises used: Bundle.TotalSpace.proj, mfderivWithin_comp