-- 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 (α :=
    (↑(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
have 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))
Tactic: simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]