-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem antipode_antipode (A : Hopf_ C) (comm : (β_ _ _).hom ≫ A.X.X.mul = A.X.X.mul) :
    A.antipode ≫ A.antipode = 𝟙 A.X.X.X

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

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

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

case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
comm : (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul = A.X.X.mul
⊢ A.antipode * 𝟙 A.X.X.X = 1

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

Tactic:
simp

Result:
no goals

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
comm : (β_ A.X.X.X A.X.X.X).hom ≫ A.X.X.mul = A.X.X.mul
⊢ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.X ◁ A.antipode ≫ A.X.X.mul =
    A.X.counit.hom ≫ A.X.X.one

Tactic:
rw [← comm, ← tensorHom_def_assoc, ← mul_antipode]

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

Tactic:
simp only [Bimon_.toComon__obj_X, Bimon_.toComon__obj_comul, comp_whiskerRight, Category.assoc,
  Bimon_.toComon__obj_counit]

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

Tactic:
simp

Result:
no goals