awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.X) (η ≫ e.hom) η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2)
        (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C }))
        (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C })) ⟶
      G.X)
    (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba : f ≫ @antipode _ _ inst_1 inst_2 _ _ * f = 1
hac : f * @antipode _ _ inst_1 inst_2 _ _ ≫ f = 1
⊢ f ≫ @antipode _ _ inst_1 inst_2 _ _ = @antipode _ _ inst_1 inst_2 _ _ ≫ f

Tactic:
apply left_inv_eq_right_inv
    (M := Conv A B)
    (a := f)

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((f ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ f ≫ @antipode _ _ inst_1 inst_2 _ _ * f = 1

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

Premises used: CategoryTheory.Conv.one_eq, CategoryTheory.Conv.mul_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((f ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
simp only [comp_whiskerRight, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B
| @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ (B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

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

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : f ⊗ₘ f
| f ▷ A ≫ B ◁ f

Tactic:
rw [← tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((f ⊗ₘ f) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ (B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

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

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : f ≫ Δ
| Δ ≫ (f ⊗ₘ f)

Tactic:
rw [← IsComonHom.hom_comul f]

Premises used: CategoryTheory.IsComonHom.hom_comul
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) ((f ≫ Δ) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((f ⊗ₘ f) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
slice_lhs 1 2 =>
      rw [← IsComonHom.hom_comul f]

Premises used: CategoryTheory.IsComonHom.hom_comul
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ B ≫ μ)

Tactic:
rw [antipode_left]

Premises used: CategoryTheory.HopfObj.antipode_left
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba :
  Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) ((f ≫ Δ) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
slice_lhs 2 4 =>
      rw [antipode_left]

Premises used: CategoryTheory.HopfObj.antipode_left
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : ε
| f ≫ ε

Tactic:
rw [IsComonHom.hom_counit]

Premises used: CategoryTheory.IsComonHom.hom_counit
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
slice_lhs :
  Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
hba :
  Eq.{v₁ + 1} (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)

Tactic:
slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]

Premises used: CategoryTheory.IsComonHom.hom_counit
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ (@antipode _ _ inst_1 inst_2 _ _ ≫ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ f * @antipode _ _ inst_1 inst_2 _ _ ≫ f = 1

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

Premises used: CategoryTheory.Conv.one_eq, CategoryTheory.Conv.mul_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ (@antipode _ _ inst_1 inst_2 _ _ ≫ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
simp only [whiskerLeft_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ A
| f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ A) ≫ B ◁ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

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

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ (f ⊗ₘ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ A) ≫ B ◁ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

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

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : μ ≫ f
| (f ⊗ₘ f) ≫ μ

Tactic:
rw [← IsMonHom.mul_hom]

Premises used: CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ ≫ f) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ (f ⊗ₘ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

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

Premises used: CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ)

Tactic:
rw [antipode_right]

Premises used: CategoryTheory.HopfObj.antipode_right
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hac :
  Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ ≫ f) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
slice_lhs 1 3 =>
      rw [antipode_right]

Premises used: CategoryTheory.HopfObj.antipode_right
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
a : η
| η ≫ f

Tactic:
rw [IsMonHom.one_hom]

Premises used: CategoryTheory.IsMonHom.one_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
slice_lhs :
  Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
hac :
  Eq.{v₁ + 1} (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)

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

Premises used: CategoryTheory.IsMonHom.one_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))

Tactic:
have := (rfl : η[A] ≫ Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] = _)
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
rhs : η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ)
| Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))

Tactic:
rhs
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
rw : CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
| η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ)

Tactic:
rw [antipode_left]

Premises used: CategoryTheory.HopfObj.antipode_left
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
rw : CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
| Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))

Tactic:
rhs
    rw [antipode_left]

Premises used: CategoryTheory.HopfObj.antipode_left
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))

Tactic:
conv at this =>
    rhs
    rw [antipode_left]

Premises used: CategoryTheory.HopfObj.antipode_left
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ Iso.inv (ρ_ A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η ≫ μ)
    (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))

Tactic:
rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal,
    ← rightUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc] at this

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.unitors_inv_equal, CategoryTheory.Bimon.one_comul_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ Iso.inv (ρ_ A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η ≫ μ)
    (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A) (η ≫ @antipode _ _ inst_1 inst_2 _ _) η

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))

Tactic:
have := (rfl : Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] ≫ ε[A] = _)
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
rhs : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε)
| Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))

Tactic:
rhs
-- Module: Mathlib.CategoryTheory.Monoidal.Hopf_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
rw : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε)
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε)

Tactic:
rw [antipode_left_assoc]

Premises used: CategoryTheory.HopfObj.antipode_left_assoc