-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem comul_tensorObj_tensorObj_left :
    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
            (ModuleCat.Hom.hom
              ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
                ModuleCat.ofHom ↑(tensorTensorTensorComm R M M N N))) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom
          ↑(tensorTensorTensorComm R (↑(of R M ⊗ of R N).toModuleCat) (↑(of R M ⊗ of R N).toModuleCat) P P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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 ⊗ of R N) ⊗ (comonEquivalence R).symm.inverse.obj (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
            (ModuleCat.Hom.hom
              ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N)).comul) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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 (ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N).toComonObj).comul) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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 (ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N).toComonObj).comul) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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
            (ModuleCat.Hom.hom
              ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
                ModuleCat.ofHom ↑(tensorTensorTensorComm R M M N N))) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom
          ↑(tensorTensorTensorComm R (↑(of R M ⊗ of R N).toModuleCat) (↑(of R M ⊗ of R N).toModuleCat) P P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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μ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul 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
            (ModuleCat.Hom.hom
              ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N)).comul) ⊗
          ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul) CoalgebraStruct.comul