-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- Auxiliary calculation for `antipode_comul`.
This calculation calls for some ASCII art out of This Week's Finds.

```
   |   |
   n   n
  | \ / |
  |  /  |
  | / \ |
  | | S S
  | | \ /
  | |  /
  | | / \
  \ / \ /
   v   v
    \ /
     v
     |
```

We move the left antipode up through the crossing,
the right antipode down through the crossing,
the right multiplication down across the strand,
reassociate the comultiplications,
then use `antipode_right` then `antipode_left` to simplify.
 -/
CategoryTheory.HopfObj.antipode_comul₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul A)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.ComonObj.comul))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A A).hom))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode
                      CategoryTheory.HopfObj.antipode)))
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                    (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A))
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                        (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom)
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.associator A A
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).inv
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                          CategoryTheory.MonObj.mul)))))))))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))