-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem mul_antipode₁ (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:
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:
slice_lhs 8 9 =>
  rw [associator_naturality_left]

Result:
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.antipode ▷ (A.X.X.X ⊗ A.X.X.X)) ≫ 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.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).hom ≫
              (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).inv ≫
                (A.X.X.mul ⊗ A.X.X.mul) ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
slice_lhs 1 7 =>
  erw [Bimon_.compatibility]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ ((A.X.X.mul ≫ A.X.comul.hom) ≫ A.antipode ▷ A.X.X.X) ≫ 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.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.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).hom ≫ A.X.X.mul ▷ (A.X.X.X ⊗ A.X.X.X)) ≫
                      A.X.X.X ◁ A.X.X.mul) ≫
                    A.antipode ▷ A.X.X.X) ≫
                  A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
slice_lhs 8 9 =>
  rw [← tensorHom_def]

Result:
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.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).hom ≫
                  ((A.X.X.mul ⊗ A.X.X.mul) ≫ A.antipode ▷ A.X.X.X) ≫ 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.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.X ⊗ A.X.X.X) A.X.X.X A.X.X.X).hom ≫
                  ((A.X.X.mul ⊗ A.X.X.mul) ≫ A.antipode ▷ A.X.X.X) ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
simp only [Mon_.monMonoidalStruct_tensorObj_X, Category.assoc, pentagon_inv_inv_hom_hom_inv_assoc,
  Mon_.tensorUnit_X]

Result:
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).hom ≫
              (α_ A.X.X.X A.X.X.X (A.X.X.X ⊗ A.X.X.X)).inv ≫
                (A.X.X.mul ⊗ A.X.X.mul) ≫ A.antipode ▷ A.X.X.X ≫ 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.X.comul.hom) ≫ A.antipode ▷ A.X.X.X) ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
slice_lhs 2 4 =>
  rw [antipode_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.mul ≫ A.X.counit.hom ≫ A.X.X.one = (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.X.counit.hom ≫ A.X.X.one = (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
simp

Result:
no goals

Proof state:
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.antipode ▷ (A.X.X.X ⊗ A.X.X.X)) ≫ 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:
slice_lhs 9 10 =>
  rw [← whisker_exchange]

Result:
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.mul ≫ A.antipode ▷ A.X.X.X) ≫ A.X.X.mul =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one