-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem comul_tensorObj_tensorObj_right :
    Coalgebra.comul (R := R) (A := (CoalgebraCat.of R M ⊗
      (CoalgebraCat.of R N ⊗ CoalgebraCat.of R P) : CoalgebraCat R))
      = Coalgebra.comul (A := M ⊗[R] N ⊗[R] P)

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom
            (ModuleCat.Hom.hom
              ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
                ModuleCat.ofHom ↑(tensorTensorTensorComm R N N P P)))) ≫
        ModuleCat.ofHom ↑(tensorTensorTensorComm R M M ↑(of R N ⊗ of R P).toModuleCat ↑(of R N ⊗ of R P).toModuleCat)) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
rw [ofComonObjCoalgebraStruct_comul]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N ⊗ of R P)).comul =
    CoalgebraStruct.comul

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom (ModuleCat.Hom.hom ((of R N).toComonObj ⊗ (of R P).toComonObj).comul)) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
simp only [instMonoidalCategoryStruct_tensorObj, ModuleCat.MonoidalCategory.tensorObj,
  ModuleCat.coe_of, Comon_.monoidal_tensorObj_comul, toComonObj_X, toComonObj_comul,
  tensorμ_eq_tensorTensorTensorComm]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom
            (ModuleCat.Hom.hom
              ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
                ModuleCat.ofHom ↑(tensorTensorTensorComm R N N P P)))) ≫
        ModuleCat.ofHom ↑(tensorTensorTensorComm R M M ↑(of R N ⊗ of R P).toModuleCat ↑(of R N ⊗ of R P).toModuleCat)) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom
            (ModuleCat.Hom.hom
              ((comonEquivalence R).symm.inverse.obj (of R N) ⊗
                  (comonEquivalence R).symm.inverse.obj (of R P)).comul)) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom (ModuleCat.Hom.hom ((of R N).toComonObj ⊗ (of R P).toComonObj).comul)) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
rw [ofComonObjCoalgebraStruct_comul]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗
          ModuleCat.ofHom
            (ModuleCat.Hom.hom
              ((comonEquivalence R).symm.inverse.obj (of R N) ⊗
                  (comonEquivalence R).symm.inverse.obj (of R P)).comul)) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)