-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem antipode_comul₂ (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.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.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.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.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ 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.comul.hom ≫
        ((((A.X.X.X ◁ A.X.counit.hom ▷ A.X.X.X ≫ A.X.X.X ◁ A.X.X.one ▷ A.X.X.X) ≫ A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom) ≫
              A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)

Tactic:
slice_lhs 2 3 =>
  simp only [← MonoidalCategory.whiskerLeft_comp]
  rw [Bimon_.counit_comul_hom]
  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).inv ≫ A.X.X.X ◁ A.X.X.one ▷ A.X.X.X) ≫ A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom) ≫
            A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ 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.comul.hom ≫
            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.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.antipode ▷ (A.X.X.X ⊗ A.X.X.X) ≫
                        (A.X.X.X ◁ A.X.X.X ◁ A.X.X.mul ≫ (α_ A.X.X.X A.X.X.X A.X.X.X).inv) ≫ A.X.X.mul ▷ A.X.X.X =
    A.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)

Tactic:
slice_lhs 10 11 =>
  rw [← MonoidalCategory.whiskerLeft_comp, ← whisker_exchange,
    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.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.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.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.mul ≫ A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ 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).inv ≫
        A.X.X.X ◁ (β_ (𝟙_ (Mon_ C)).X A.X.X.X).hom ≫
          A.X.X.X ◁ A.antipode ▷ (𝟙_ (Mon_ C)).X ≫
            (α_ A.X.X.X A.X.X.X (𝟙_ (Mon_ C)).X).inv ≫ A.X.X.mul ▷ (𝟙_ (Mon_ C)).X ≫ A.X.X.X ◁ A.X.X.one =
    A.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)

Tactic:
simp only [Mon_.monMonoidalStruct_tensorObj_X, Mon_.tensorUnit_X, braiding_tensorUnit_left,
  MonoidalCategory.whiskerLeft_comp, whiskerLeft_rightUnitor_inv,
  MonoidalCategory.whiskerRight_id, whiskerLeft_rightUnitor, Category.assoc, Iso.hom_inv_id_assoc,
  Iso.inv_hom_id_assoc, whiskerLeft_inv_hom_assoc, antipode_right_assoc]

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

Tactic:
rw [rightUnitor_inv_naturality_assoc, tensorHom_def]

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

Tactic:
slice_lhs 3 7 =>
  simp only [← MonoidalCategory.whiskerLeft_comp]
  rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]
  simp only [← comp_whiskerRight]
  rw [antipode_right]
  simp only [comp_whiskerRight]
  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.comul.hom ≫
        ((((A.X.X.X ◁ A.X.counit.hom ▷ A.X.X.X ≫ A.X.X.X ◁ A.X.X.one ▷ A.X.X.X) ≫ A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom) ≫
              A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ 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.comul.hom ≫
        A.X.X.X ◁ A.X.X.X ◁ A.X.comul.hom ≫
          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).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).hom) ≫
                  A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)

Tactic:
slice_lhs 2 3 =>
  simp only [← MonoidalCategory.whiskerLeft_comp]
  rw [Bimon_.comul_assoc_hom]
  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.comul.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.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.mul ▷ A.X.X.X) ≫
              A.X.X.X ◁ (β_ A.X.X.X A.X.X.X).hom) ≫
            A.X.X.X ◁ A.antipode ▷ 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.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)