-- 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.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.comul.hom ▷ A.X.X.X ≫
      (A.X.X ⊗ A.X.X).X ◁ 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 A.X.X.X).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).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.antipode ⊗ A.antipode)) ≫
                      (α_ (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.mul) ▷ A.X.X.X) ≫
                A.X.X.mul ▷ 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, tensor_whiskerLeft,
  MonoidalCategory.whiskerLeft_comp, Category.assoc,
  whiskerLeft_inv_hom, Category.comp_id, whiskerLeft_hom_inv_assoc, Iso.inv_hom_id_assoc,
  pentagon_inv_inv_hom_inv_inv, whisker_assoc, Mon_.mul_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.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.comul.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 A.X.X.X).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).hom ≫
                  A.X.X.X ◁ A.X.X.X ◁ (A.antipode ⊗ A.antipode) ≫
                    A.X.X.X ◁ (α_ 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.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.counit.hom ⊗ A.X.counit.hom) ≫ (ρ_ (𝟙_ (Mon_ C)).X).hom ≫ A.X.X.one =
    (A.X.counit.hom ⊗ A.X.counit.hom) ≫ (λ_ (𝟙_ C)).hom ≫ A.X.X.one

Tactic:
simp only [Mon_.tensorUnit_X]

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

Tactic:
slice_lhs 3 4 =>
  simp only [← MonoidalCategory.whiskerLeft_comp]
  rw [BraidedCategory.braiding_naturality_right]
  simp only [MonoidalCategory.whiskerLeft_comp]

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

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