-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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
⊢ 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
have 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)))
Tactic: simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]