-- 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 :
  Eq (α := (↑A : 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.whiskerRight (↟(mul' 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))
                        (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)) (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)) :
      (↑(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)) :
      (↑(of R (↑A : Type u)) : Type u))
⊢ Eq (α := (↑A : Type u))
    (((Hom.hom
              (CategoryStruct.comp (Y :=
                MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u)))
                (↟(mul' 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]
              (↑(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)) →
            (↑A : 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) ⊗[R]
            (↑A : Type u)) :
      (↑A : Type u))
    (((Hom.hom
              (Iso.hom
                  (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u)) (of R (↑A : Type u))) ≫
                CategoryStruct.comp (Y :=
                  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                  (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u))))
                  (↟(mul' 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]
              (↑(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)) →
            (↑A : 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) ⊗[R]
            (↑A : Type u)) :
      (↑A : Type u))

Tactic:
rw [hom_comp, LinearMap.comp_apply, hom_comp, LinearMap.comp_apply, hom_comp,
        LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, ModuleCat.hom_comp