awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
X : CoalgCat R
simp_rw :
  Eq (α :=
    (↑X.toModuleCat : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)) :
        Type u))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul) (X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫
          Iso.hom (α_ X.toModuleCat X.toModuleCat X.toModuleCat))))
⊢ Eq (α :=
    (↑(ModuleCat.of R (↑X.toModuleCat : Type u)) : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑X.toModuleCat : Type u)))) :
        Type u))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑X.toModuleCat : Type u)))
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.of R (↑X.toModuleCat : Type u) ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑X.toModuleCat : Type u)))
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.ofHom CoalgebraStruct.comul ▷ ModuleCat.of R (↑X.toModuleCat : Type u) ≫
          Iso.hom
            (α_ (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑X.toModuleCat : Type u))))))

Tactic:
simp_rw [ModuleCat.of_coe]

Premises used: ModuleCat.of_coe
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
X : CoalgCat R
⊢ Eq (α :=
    (↑X.toModuleCat : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)) :
        Type u))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul) (X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫
          Iso.hom (α_ X.toModuleCat X.toModuleCat X.toModuleCat))))

Tactic:
Coalgebra.coassoc.symm

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.coassoc, Quotient, TensorProduct, AddCon.Quotient, Eq.symm
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
X : CoalgCat R
⊢ Eq (α :=
    (↑X.toModuleCat : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)) :
        Type u))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul) (X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫
          Iso.hom (α_ X.toModuleCat X.toModuleCat X.toModuleCat))))

Tactic:
exact Coalgebra.coassoc.symm

Premises used: Coalgebra.coassoc, Eq.symm
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat R
x : X ⟶ Y
⊢ Eq (α := Functor.obj (𝟭 (CoalgCat R)) X ⟶ Functor.obj (toComon R ⋙ ofComon R) Y)
    (CategoryTheory.Functor.map (𝟭 (CoalgCat R)) x ≫
      Iso.hom
        ((fun (x : CoalgCat R) ↦
            (Iso.refl (Functor.obj (𝟭 (CoalgCat R)) x) :
              Functor.obj (𝟭 (CoalgCat R)) x ≅ Functor.obj (𝟭 (CoalgCat R)) x))
          Y))
    (Iso.hom
        ((fun (x : CoalgCat R) ↦
            (Iso.refl (Functor.obj (𝟭 (CoalgCat R)) x) :
              Functor.obj (𝟭 (CoalgCat R)) x ≅ Functor.obj (𝟭 (CoalgCat R)) x))
          X) ≫
      CategoryTheory.Functor.map (toComon R ⋙ ofComon R) x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
X Y : Comon (ModuleCat R)
x : X ⟶ Y
⊢ Eq (α := Functor.obj (ofComon R ⋙ toComon R) X ⟶ Functor.obj (𝟭 (Comon (ModuleCat R))) Y)
    (CategoryTheory.Functor.map (ofComon R ⋙ toComon R) x ≫
      Iso.hom
        ((fun (x : Comon (ModuleCat R)) ↦
            (Iso.refl (Functor.obj (ofComon R ⋙ toComon R) x) :
              Functor.obj (ofComon R ⋙ toComon R) x ≅ Functor.obj (ofComon R ⋙ toComon R) x))
          Y))
    (Iso.hom
        ((fun (x : Comon (ModuleCat R)) ↦
            (Iso.refl (Functor.obj (ofComon R ⋙ toComon R) x) :
              Functor.obj (ofComon R ⋙ toComon R) x ≅ Functor.obj (ofComon R ⋙ toComon R) x))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (Comon (ModuleCat R))) x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
K L : CoalgCat R
simp :
  Eq.{u + 1} (α :=
    (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) K.toModuleCat K.toModuleCat)
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) L.toModuleCat L.toModuleCat)) :
        Type u))
    (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
    (TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul)
⊢ Eq.{u + 1} (α :=
    (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
      TensorProduct R (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u)
        (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (tensorObj (𝒞 := category) K L).toModuleCat
              (tensorObj (𝒞 := category) K L).toModuleCat) :
          Type u))
    ((↑(TensorProduct.tensorTensorTensorComm R (↑K.toModuleCat : Type u) (↑K.toModuleCat : Type u)
            (↑L.toModuleCat : Type u) (↑L.toModuleCat : Type u)) :
        TensorProduct R (TensorProduct R (↑K.toModuleCat : Type u) (↑K.toModuleCat : Type u))
            (TensorProduct R (↑L.toModuleCat : Type u) (↑L.toModuleCat : Type u)) →ₗ[R]
          TensorProduct R (TensorProduct R (↑K.toModuleCat : Type u) (↑L.toModuleCat : Type u))
            (TensorProduct R (↑K.toModuleCat : Type u) (↑L.toModuleCat : Type u))) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
simp only [Comon.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse,
    comonEquivalence_functor, toComon_obj, toComonObj_X, ModuleCat.of_coe,
    MonObj.tensorObj.mul_def, unop_comp, unop_tensorObj, unop_tensorHom,
    BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp,
    ModuleCat.hom_ofHom, LinearEquiv.comp_toLinearMap_eq_iff]

Premises used: ModuleCat.of_coe, CategoryTheory.unop_tensorHom, LinearEquiv.comp_toLinearMap_eq_iff, CategoryTheory.BraidedCategory.unop_tensorμ, CoalgCat.toComonObj_X, CategoryTheory.MonObj.tensorObj.mul_def, CategoryTheory.unop_comp, CoalgCat.comonEquivalence_functor, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_ofHom, ModuleCat.hom_comp, CategoryTheory.unop_tensorObj, CoalgCat.toComon_obj, CategoryTheory.Equivalence.symm_inverse, CategoryTheory.Comon.monoidal_tensorObj_comon_comul
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
K L : CoalgCat R
⊢ Eq.{u + 1} (α :=
    (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) K.toModuleCat K.toModuleCat)
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) L.toModuleCat L.toModuleCat)) :
        Type u))
    (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
    (TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P Q : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : AddCommGroup Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Coalgebra R M
inst_10 : Coalgebra R N
inst_11 : Coalgebra R P
inst_12 : Coalgebra R Q
f : M →ₗc[R] N
g : P →ₗc[R] Q
⊢ CoalgHom.toLinearMap (Hom.toCoalgHom' (ofHom f ⊗ₘ ofHom g)) = TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Coalgebra R M
inst_6 : Coalgebra R N
simp :
  Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
      (↑(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))) :
        Type u))
    (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
    (AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)
⊢ Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N)))
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N)))) :
          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
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Coalgebra R M
inst_6 : Coalgebra R N
⊢ Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
      (↑(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))) :
        Type u))
    (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
    (AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
rfl
-- 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.{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
⊢ 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 Δ :
      (↑(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 only [Comon.monoidal_tensorObj_comon_comul]

Premises used: CategoryTheory.Comon.monoidal_tensorObj_comon_comul
-- 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
⊢ 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:
rfl
-- 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
dsimp :
  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
⊢ Eq.{u + 1} (α :=
    (↑(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 Δ :
      (↑(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))
    CoalgebraStruct.comul

Tactic:
dsimp +instances
-- 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) (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
⊢ 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

Tactic:
simp +instances only [toComonObj]

Premises used: CoalgCat.toComonObj
-- 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
⊢ 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:
rfl