-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem mul_antipode (A : Hopf_ C) :
    A.X.X.mul ≫ A.antipode = (A.antipode ⊗ A.antipode) ≫ (β_ _ _).hom ≫ A.X.X.mul

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
        A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
          A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
            (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
              (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
                A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
                  (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫
                    A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ≫
                      A.X.X.X ◁ (A.antipode ⊗ A.antipode) ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
exact mul_antipode₂ A

Result:
no goals

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
        A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
          A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
            (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
              (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
                A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
                  A.antipode ▷ A.X.X.X ▷ A.X.X.X ≫ (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
exact mul_antipode₁ A

Result:
no goals

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul ≫ A.antipode * A.X.X.mul = 1

Tactic:
erw [Conv.mul_eq, Conv.one_eq]

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).comul ≫
      (A.X.X.mul ≫ A.antipode) ▷ ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).X ≫
        A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).counit ≫ A.X.X.one

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (tensorμ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).unop ≫
        (α_ (A.X.X.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).inv ≫
          A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
            (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫
              A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ≫
                A.X.X.X ◁ (A.antipode ⊗ A.antipode) ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
simp only [tensorμ]

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      ((α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X ⊗ Opposite.op A.X.X.X)).hom ≫
            Opposite.op A.X.X.X ◁ (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).inv ≫
              Opposite.op A.X.X.X ◁ (β_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).hom ▷ Opposite.op A.X.X.X ≫
                Opposite.op A.X.X.X ◁ (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).hom ≫
                  (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)
                      (Opposite.op A.X.X.X ⊗ Opposite.op A.X.X.X)).inv).unop ≫
        (α_ (A.X.X.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).inv ≫
          A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
            (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫
              A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ≫
                A.X.X.X ◁ (A.antipode ⊗ A.antipode) ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul ≫ A.antipode = (A.antipode ⊗ A.antipode) ≫ (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul

Tactic:
apply left_inv_eq_right_inv
  (M := Conv (((Bimon_.toComon_ C).obj A.X) ⊗ ((Bimon_.toComon_ C).obj A.X)) A.X.X)
  (a := A.X.X.mul)

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul ≫ A.antipode * A.X.X.mul = 1

case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul * (A.antipode ⊗ A.antipode) ≫ (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul = 1

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      ((α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X ⊗ Opposite.op A.X.X.X)).hom ≫
            Opposite.op A.X.X.X ◁ (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).inv ≫
              Opposite.op A.X.X.X ◁ (β_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).hom ▷ Opposite.op A.X.X.X ≫
                Opposite.op A.X.X.X ◁ (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)).hom ≫
                  (α_ (Opposite.op A.X.X.X) (Opposite.op A.X.X.X)
                      (Opposite.op A.X.X.X ⊗ Opposite.op A.X.X.X)).inv).unop ≫
        (α_ (A.X.X.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).inv ≫
          A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
            A.antipode ▷ A.X.X.X ▷ A.X.X.X ≫ (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
simp only [unop_comp, unop_tensorObj, unop_inv_associator, unop_whiskerLeft,
  unop_hom_associator, unop_whiskerRight, unop_hom_braiding, Category.assoc,
  pentagon_hom_inv_inv_inv_inv_assoc]

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ (A.X.comul.hom ⊗ A.X.comul.hom) ≫
      (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).hom ≫
        A.X.X.X ◁ (α_ A.X.X.X A.X.X.X A.X.X.X).inv ≫
          A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom ▷ A.X.X.X ≫
            (α_ A.X.X.X (A.X.X.X ⊗ A.X.X.X) A.X.X.X).inv ≫
              (α_ A.X.X.X A.X.X.X A.X.X.X).inv ▷ A.X.X.X ≫
                A.X.X.mul ▷ A.X.X.X ▷ A.X.X.X ≫
                  A.antipode ▷ A.X.X.X ▷ A.X.X.X ≫ (α_ A.X.X.X A.X.X.X A.X.X.X).hom ≫ A.X.X.X ◁ A.X.X.mul ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul * (A.antipode ⊗ A.antipode) ≫ (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul = 1

Tactic:
erw [Conv.mul_eq, Conv.one_eq]

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).comul ≫
      A.X.X.mul ▷ ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).X ≫
        A.X.X.X ◁ ((A.antipode ⊗ A.antipode) ≫ (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul) ≫ A.X.X.mul =
    ((Bimon_.toComon_ C).obj A.X ⊗ (Bimon_.toComon_ C).obj A.X).counit ≫ A.X.X.one