-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
x : M
V : Type u_18
inst_6 : NormedAddCommGroup V
inst_7 : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiffAt f x
hg : MDiffAt g x
rw :
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
      (↑(fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, V) ((f • g) x) →L[𝕜] V)
      (HAdd.hAdd (β :=
        ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
        (HSMul.hSMul (β :=
          ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
            (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
          (f x)
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
              (↑(ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x))) : V →L[𝕜] TangentSpace 𝓘(𝕜, V) ((f • g) x))
              ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
              (TangentSpace 𝓘(𝕜, V) ((f • g) x))))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (toSpanSingleton 𝕜
                ((ContinuousLinearEquiv.symm (fromTangentSpace ((f • g) x)) :
                    (a : V) → TangentSpace 𝓘(𝕜, V) ((f • g) x))
                  (g x)) :
              ContinuousLinearMap.{u_1, u_1, u_1, u_18} (RingHom.id 𝕜) 𝕜 (TangentSpace 𝓘(𝕜, V) ((f • g) x)))
            (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
                (↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) :
          ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x)
            (TangentSpace 𝓘(𝕜, V) ((f • g) x)))) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V) (f x)
        ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) +
      ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 (g x))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
          (↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x))
⊢ ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, V) ((f • g) x))
      (↑(fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, V) ((f • g) x) →L[𝕜] V) (mfderiv% (f • g) x) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_18} (RingHom.id 𝕜) (TangentSpace I x) V) (f x)
        ((↑(fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, V) (g x) →L[𝕜] V) ∘SL mfderiv% g x) +
      ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 (g x))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
          (↑(fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x))

Tactic:
rw [mfderiv_smul hf hg]

Premises used: mfderiv_smul