-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem antipode_comul (A : Hopf_ C) :
    A.antipode ≫ A.X.comul.hom = A.X.comul.hom ≫ (β_ _ _).hom ≫ (A.antipode ⊗ A.antipode)

Proof state:
case hac
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).hom ≫ (A.antipode ⊗ A.antipode) = 1

Tactic:
erw [Conv.mul_eq, Conv.one_eq]

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ ((Bimon_.toComon_ C).obj A.X).comul ≫
      A.X.comul.hom ▷ ((Bimon_.toComon_ C).obj A.X).X ≫
        (A.X.X ⊗ A.X.X).X ◁ (A.X.comul.hom ≫ (β_ A.X.X.X A.X.X.X).hom ≫ (A.antipode ⊗ A.antipode)) ≫
          (A.X.X ⊗ A.X.X).mul =
    ((Bimon_.toComon_ C).obj A.X).counit ≫ (A.X.X ⊗ A.X.X).one

Proof state:
case hba
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:
exact antipode_comul₁ A

Result:
no goals

Proof state:
case hba
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 ⊗ 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:
simp only [Category.assoc, Iso.inv_hom_id_assoc]

Result:
case hba
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)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.antipode ≫ A.X.comul.hom = A.X.comul.hom ≫ (β_ A.X.X.X A.X.X.X).hom ≫ (A.antipode ⊗ A.antipode)

Tactic:
apply left_inv_eq_right_inv
  (M := Conv ((Bimon_.toComon_ C).obj A.X) (A.X.X ⊗ A.X.X))
  (a := A.X.comul.hom)

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.antipode ≫ A.X.comul.hom * A.X.comul.hom = 1

case hac
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).hom ≫ (A.antipode ⊗ A.antipode) = 1

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.antipode ≫ A.X.comul.hom * A.X.comul.hom = 1

Tactic:
erw [Conv.mul_eq, Conv.one_eq]

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ ((Bimon_.toComon_ C).obj A.X).comul ≫
      (A.antipode ≫ A.X.comul.hom) ▷ ((Bimon_.toComon_ C).obj A.X).X ≫
        (A.X.X ⊗ A.X.X).X ◁ A.X.comul.hom ≫ (A.X.X ⊗ A.X.X).mul =
    ((Bimon_.toComon_ C).obj A.X).counit ≫ (A.X.X ⊗ A.X.X).one

Proof state:
case hac
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.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)

Tactic:
exact antipode_comul₂ A

Result:
no goals

Proof state:
case hac
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.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 ⊗ 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:
simp only [Category.assoc, Iso.inv_hom_id_assoc]

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

Tactic:
simp only [Bimon_.toComon__obj_X, Mon_.monMonoidalStruct_tensorObj_X, Bimon_.toComon__obj_comul,
  comp_whiskerRight, tensor_whiskerLeft, Mon_.tensorObj_mul, Category.assoc,
  Bimon_.toComon__obj_counit, Mon_.tensorObj_one]

Result:
case hba
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 ≫
                tensorμ A.X.X.X A.X.X.X A.X.X.X A.X.X.X ≫ (A.X.X.mul ⊗ A.X.X.mul) =
    A.X.counit.hom ≫ (λ_ (𝟙_ C)).inv ≫ (A.X.X.one ⊗ A.X.X.one)