-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x y z : (↑(of R (↑A : Type u)) : Type u)
hf :
  x * y * z =
    (Hom.hom (↟(mul' R (↑A : Type u))) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u)) → (↑A : Type u))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u)))) :
            (a :
                (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u))
                      (MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u)))) :
                  Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u))
          (((Hom.hom
                  (Iso.hom
                    (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u))
                      (of R (↑A : Type u)))) :
                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
                        (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u)))
                        (of R (↑A : Type u))) :
                    Type u) →ₗ[R]
                  (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                        (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u)))) :
                    Type u)) :
              (a :
                  (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                    (↑A : Type u)) →
                (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u))
                      (MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u)))) :
                  Type u))
            ((((TensorProduct.mk R
                        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                              (of R (↑A : Type u))) :
                          Type u)
                        (↑A : Type u) :
                      (a : (↑A : Type u) ⊗[R] (↑A : Type u)) →
                        (↑A : Type u) →ₗ[R]
                          (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                            (↑A : Type u))
                    (x ⊗ₜ[R] y) :
                  (↑A : Type u) →ₗ[R]
                    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                            (of R (↑A : Type u))) :
                        Type u) ⊗[R]
                      (↑A : Type u)) :
                (a : (↑A : Type u)) →
                  (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                    (↑A : Type u))
              z)) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
          Type u))
⊢ HMul.hMul (β := (↑A : Type u)) (x * y)
      ((LinearMap.id : (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u)) (x ⊗ₜ[R] y, z).2 :
        (↑(of R (↑A : Type u)) : Type u)) =
    (Hom.hom (↟(mul' R (↑A : Type u))) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u)) →
          (↑(of R (↑A : Type u)) : Type u))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u)))) :
            (a :
                (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u))
                      (MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u)))) :
                  Type u)) →
              (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u))
          (((Hom.hom
                  (Iso.hom
                    (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u))
                      (of R (↑A : Type u)))) :
                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
                        (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u)))
                        (of R (↑A : Type u))) :
                    Type u) →ₗ[R]
                  (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                        (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u)))) :
                    Type u)) :
              (a :
                  (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                    (↑A : Type u)) →
                (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u))
                      (MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u)))) :
                  Type u))
            ((((TensorProduct.mk R
                        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                              (of R (↑A : Type u))) :
                          Type u)
                        (↑A : Type u) :
                      (a : (↑A : Type u) ⊗[R] (↑A : Type u)) →
                        (↑A : Type u) →ₗ[R]
                          (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                            (↑A : Type u))
                    (x ⊗ₜ[R] y) :
                  (↑A : Type u) →ₗ[R]
                    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                            (of R (↑A : Type u))) :
                        Type u) ⊗[R]
                      (↑A : Type u)) :
                (a : (↑A : Type u)) →
                  (↑(MonoidalCategoryStruct.tensorObj (of R (↑A : Type u)) (of R (↑A : Type u))) : Type u) ⊗[R]
                    (↑A : Type u))
              z)) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u))) :
          Type u))

Tactic:
dsimp only [id_coe, id_eq]

Premises used: LinearMap.id_coe, id_eq