-- 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) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
    ((↑(tensorTensorTensorComm R M M (↑(toModuleCat (tensorObj (𝒞 := category) (of R N) (of R P))) : Type u)
              (↑(toModuleCat (tensorObj (𝒞 := category) (of R N) (of R P))) : Type u)) :
          M ⊗[R] M ⊗[R] ((↑(of R N ⊗ of R P).toModuleCat : Type u) ⊗[R] (↑(of R N ⊗ of R P).toModuleCat : Type u)) →ₗ[R]
            M ⊗[R] (↑(of R N ⊗ of R P).toModuleCat : Type u) ⊗[R] (M ⊗[R] (↑(of R N ⊗ of R P).toModuleCat : Type u))) ∘ₗ
        ModuleCat.Hom.hom
          (Quiver.Hom.unop MonObj.mul ⊗ₘ
            CategoryStruct.comp (Y :=
              tensorObj (𝒞 := ModuleCat.moduleCategory R)
                (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R N) (ModuleCat.of R N))
                (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R P) (ModuleCat.of R P)))
              (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul)
              (ModuleCat.ofHom
                (↑(tensorTensorTensorComm R N N P P) : N ⊗[R] N ⊗[R] (P ⊗[R] P) →ₗ[R] N ⊗[R] P ⊗[R] (N ⊗[R] P)))) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))) :
          Type u))
    ((↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) :
          M ⊗[R] M ⊗[R] (N ⊗[R] P ⊗[R] (N ⊗[R] P)) →ₗ[R] M ⊗[R] (N ⊗[R] P) ⊗[R] (M ⊗[R] (N ⊗[R] P))) ∘ₗ
        AlgebraTensorModule.map CoalgebraStruct.comul
          ((↑(tensorTensorTensorComm R N N P P) : N ⊗[R] N ⊗[R] (P ⊗[R] P) →ₗ[R] N ⊗[R] P ⊗[R] (N ⊗[R] P)) ∘ₗ
            AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul) :
      M ⊗[R] (N ⊗[R] P) →ₗ[R] M ⊗[R] (N ⊗[R] P) ⊗[R] (M ⊗[R] (N ⊗[R] P)))
⊢ Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
    (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))) :
          Type u))
    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