-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
simp :
  Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u))
    ((↑(tensorTensorTensorComm R (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u)
              (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) P P) :
          (↑(of R M ⊗ of R N).toModuleCat : Type u) ⊗[R] (↑(of R M ⊗ of R N).toModuleCat : Type u) ⊗[R] (P ⊗[R] P) →ₗ[R]
            (↑(of R M ⊗ of R N).toModuleCat : Type u) ⊗[R] P ⊗[R] ((↑(of R M ⊗ of R N).toModuleCat : Type u) ⊗[R] P)) ∘ₗ
        ModuleCat.Hom.hom
          (CategoryStruct.comp (Y :=
              tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R M) (ModuleCat.of R M))
                (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R N) (ModuleCat.of R N)))
              (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul)
              (ModuleCat.ofHom
                (↑(tensorTensorTensorComm R M M N N) : M ⊗[R] M ⊗[R] (N ⊗[R] N) →ₗ[R] M ⊗[R] N ⊗[R] (M ⊗[R] N))) ⊗ₘ
            Quiver.Hom.unop MonObj.mul) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P)))
              (toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P)))) :
          Type u))
    ((↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) :
          M ⊗[R] N ⊗[R] (M ⊗[R] N) ⊗[R] (P ⊗[R] P) →ₗ[R] M ⊗[R] N ⊗[R] P ⊗[R] (M ⊗[R] N ⊗[R] P)) ∘ₗ
        AlgebraTensorModule.map
          ((↑(tensorTensorTensorComm R M M N N) : M ⊗[R] M ⊗[R] (N ⊗[R] N) →ₗ[R] M ⊗[R] N ⊗[R] (M ⊗[R] N)) ∘ₗ
            AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)
          CoalgebraStruct.comul :
      M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] N ⊗[R] P ⊗[R] (M ⊗[R] N ⊗[R] P))
⊢ Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u))
    (ModuleCat.Hom.hom
        (Quiver.Hom.unop
          (tensorμ (Opposite.op (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))))
            (Opposite.op (ModuleCat.of R P)) (Opposite.op (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))))
            (Opposite.op (ModuleCat.of R P)))) ∘ₗ
      ModuleCat.Hom.hom
        ((Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul) ≫
            Quiver.Hom.unop
              (tensorμ (Opposite.op (ModuleCat.of R M)) (Opposite.op (ModuleCat.of R N))
                (Opposite.op (ModuleCat.of R M)) (Opposite.op (ModuleCat.of R N))) ⊗ₘ
          Quiver.Hom.unop MonObj.mul))
    CoalgebraStruct.comul

Tactic:
simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]

Premises used: TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def