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

Tactic:
slice_lhs 3 9 =>
  erw [Bimon_.compatibility]

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

Tactic:
slice_lhs 3 5 =>
  rw [← associator_naturality_right, ← Category.assoc, ← 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.antipode ▷ A.X.X.X ≫
        ((((((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.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.comul.hom = A.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ 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.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.comul.hom =
    A.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)

Tactic:
slice_lhs 1 3 =>
  erw [A.antipode_left]

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