-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem hom_antipode {A B : Hopf_ C} (f : A ⟶ B) :
    f.hom.hom ≫ B.antipode = A.antipode ≫ f.hom.hom

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

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ A.X.comul.hom ≫ f.hom.hom ▷ A.X.X.X ≫ B.X.X.X ◁ A.antipode ≫ B.X.X.X ◁ f.hom.hom ≫ B.X.X.mul =
    A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 2 3 =>
  rw [← whisker_exchange]

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

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ (A.X.counit.hom ≫ A.X.X.one) ≫ f.hom.hom = A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 2 3 =>
  rw [f.hom.one_hom]

Result:
no goals

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ A.X.comul.hom ≫ A.X.X.X ◁ A.antipode ≫ (f.hom.hom ⊗ f.hom.hom) ≫ B.X.X.mul = A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 3 4 =>
  rw [← f.hom.mul_hom]

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ A.X.comul.hom ≫ A.X.X.X ◁ A.antipode ≫ A.X.X.mul ≫ f.hom.hom = A.X.counit.hom ≫ B.X.X.one

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

Tactic:
slice_lhs 3 4 =>
  rw [← tensorHom_def]

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

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

Tactic:
slice_lhs 3 4 =>
  rw [← whisker_exchange]

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

Proof state:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ A.X.comul.hom ≫ A.X.X.X ◁ A.antipode ≫ A.X.X.mul ≫ f.hom.hom = A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 1 3 =>
  rw [A.antipode_right]

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ (A.X.counit.hom ≫ A.X.X.one) ≫ f.hom.hom = A.X.counit.hom ≫ B.X.X.one

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

Tactic:
slice_lhs 1 2 =>
  rw [← Bimon_.hom_comul_hom f]

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

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ f.hom.hom ≫ B.antipode = A.antipode ≫ f.hom.hom

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

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

case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ f.hom.hom * A.antipode ≫ f.hom.hom = 1

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ f.hom.hom ≫ B.X.counit.hom ≫ B.X.X.one = A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 1 2 =>
  rw [Bimon_.hom_counit_hom f]

Result:
no goals

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

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

Tactic:
slice_lhs 2 3 =>
  rw [← tensorHom_def]

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

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

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

Result:
case hac
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ A.X.comul.hom ≫ f.hom.hom ▷ A.X.X.X ≫ B.X.X.X ◁ A.antipode ≫ B.X.X.X ◁ f.hom.hom ≫ B.X.X.mul =
    A.X.counit.hom ≫ B.X.X.one

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