-- Mathlib/CategoryTheory/Monoidal/Comon_.lean
theorem tensorObj_comul (A B : Comon_ C) :
    (A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ tensorμ A.X A.X B.X B.X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (A.comul ⊗ B.comul) ≫ (tensorμ (op A.X) (op B.X) (op A.X) (op B.X)).unop =
    (A.comul ⊗ B.comul) ≫ tensorμ A.X A.X B.X B.X

Tactic:
congr

Result:
case e_a.e_f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ tensorμ (op A.X) (op B.X) (op A.X) (op B.X) =
    op
      ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
        A.X ◁ (α_ A.X B.X B.X).inv ≫
          A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv)

Proof state:
case e_a.e_f.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ ((((α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv) ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X) ≫
        A.X ◁ (α_ B.X A.X B.X).hom) ≫
      (α_ A.X B.X (A.X ⊗ B.X)).inv =
    (α_ A.X A.X (B.X ⊗ B.X)).hom ≫
      A.X ◁ (α_ A.X B.X B.X).inv ≫
        A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv

Tactic:
rw [Category.assoc, Category.assoc, Category.assoc]

Result:
no goals

Proof state:
case e_a.e_f.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ ((α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫
        op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫
          op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫
            op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv).unop =
    Quiver.Hom.unop
      (op
        ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
          A.X ◁ (α_ A.X B.X B.X).inv ≫
            A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv))

Tactic:
dsimp [op_tensorObj, op_associator]

Result:
case e_a.e_f.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ ((((α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv) ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X) ≫
        A.X ◁ (α_ B.X A.X B.X).hom) ≫
      (α_ A.X B.X (A.X ⊗ B.X)).inv =
    (α_ A.X A.X (B.X ⊗ B.X)).hom ≫
      A.X ◁ (α_ A.X B.X B.X).inv ≫
        A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ tensorμ A.X A.X B.X B.X

Tactic:
rw [tensorObj_comul']

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (A.comul ⊗ B.comul) ≫ (tensorμ (op A.X) (op B.X) (op A.X) (op B.X)).unop =
    (A.comul ⊗ B.comul) ≫ tensorμ A.X A.X B.X B.X

Proof state:
case e_a.e_f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫
      op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫
        op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫
          op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv =
    op
      ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
        A.X ◁ (α_ A.X B.X B.X).inv ≫
          A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv)

Tactic:
apply Quiver.Hom.unop_inj

Result:
case e_a.e_f.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ ((α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫
        op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫
          op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫
            op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv).unop =
    Quiver.Hom.unop
      (op
        ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
          A.X ◁ (α_ A.X B.X B.X).inv ≫
            A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv))

Proof state:
case e_a.e_f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ tensorμ (op A.X) (op B.X) (op A.X) (op B.X) =
    op
      ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
        A.X ◁ (α_ A.X B.X B.X).inv ≫
          A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv)

Tactic:
simp only [tensorμ, unop_tensorObj, unop_op]

Result:
case e_a.e_f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫
      op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫
        op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫
          op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv =
    op
      ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫
        A.X ◁ (α_ A.X B.X B.X).inv ≫
          A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv)