awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
slice_lhs :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              A ◁ A ◁ Iso.hom (β_ A A) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫
                      ((A ◁ A ◁ μ ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              A ◁ A ◁ Iso.hom (β_ A A) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫
                      A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫
                        (A ◁ A ◁ μ ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 10 11 =>
    rw [← whiskerLeft_comp, ← whisker_exchange, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, 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 : C
inst_3 : HopfObj A
a : A ◁ (A ◁ Iso.hom (β_ A A) ≫ Iso.inv (α_ A A A) ≫ Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ μ)
| A ◁ A ◁ Iso.hom (β_ A A) ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ μ

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ (Iso.inv (α_ A A A) ≫ μ ▷ A ≫ Iso.hom (β_ A A))
| A ◁ (A ◁ Iso.hom (β_ A A) ≫ Iso.inv (α_ A A A) ≫ Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ μ)

Tactic:
rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← BraidedCategory.braiding_naturality_left]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse_assoc, CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.Iso.inv_hom_id_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
a : A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)
| A ◁ (Iso.inv (α_ A A A) ≫ μ ▷ A ≫ Iso.hom (β_ A A))

Tactic:
simp only [whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)
| A ◁ A ◁ Iso.hom (β_ A A) ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ μ

Tactic:
simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.Iso.inv_hom_id_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
slice_lhs :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              (((A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  Iso.inv (α_ A A A)) ≫
                μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              A ◁ A ◁ Iso.hom (β_ A A) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫
                      ((A ◁ A ◁ μ ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 6 10 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.Iso.inv_hom_id_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
rw :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
            (((A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                Iso.inv (α_ A A A)) ≫
              μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              (((A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  Iso.inv (α_ A A A)) ≫
                μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
rw [ComonObj.comul_assoc_flip_assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ComonObj.comul_assoc_flip_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
a : A ◁ (Δ ≫ A ◁ Δ)
| A ◁ Δ ≫ A ◁ A ◁ Δ

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ (Δ ≫ Δ ▷ A ≫ Iso.hom (α_ A A A))
| A ◁ (Δ ≫ A ◁ Δ)

Tactic:
rw [ComonObj.comul_assoc]

Premises used: CategoryTheory.ComonObj.comul_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
a : A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)
| A ◁ (Δ ≫ Δ ▷ A ≫ Iso.hom (α_ A A A))

Tactic:
simp only [whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)
| A ◁ Δ ≫ A ◁ A ◁ Δ

Tactic:
simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.ComonObj.comul_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
slice_lhs :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      (((((((A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  A ◁ Iso.inv (α_ A A A)) ≫
                A ◁ μ ▷ A) ≫
              A ◁ Iso.hom (β_ A A)) ≫
            A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
            (((A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                Iso.inv (α_ A A A)) ≫
              μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 2 3 =>
    simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.ComonObj.comul_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
a : A ◁ (Δ ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.inv (α_ A A A) ≫ μ ▷ A)
| A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a :
  A ◁
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (Δ ▷ A)
      ((A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ μ ▷ A)
| A ◁ (Δ ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.inv (α_ A A A) ≫ μ ▷ A)

Tactic:
rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.Iso.hom_inv_id_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
a : A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ) ▷ A
| A ◁
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (Δ ▷ A)
      ((A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ μ ▷ A)

Tactic:
simp only [← comp_whiskerRight]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ▷ A
| A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ) ▷ A

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 : C
inst_3 : HopfObj A
a : A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A)
| A ◁ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ▷ A

Tactic:
simp only [comp_whiskerRight]

Premises used: 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 : C
inst_3 : HopfObj A
a :
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A)) (A ◁ ε ▷ A)
    (A ◁ η ▷ A)
| A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A)

Tactic:
simp only [whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a :
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A)) (A ◁ ε ▷ A)
    (A ◁ η ▷ A)
| A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A

Tactic:
simp only [← whiskerLeft_comp]
    rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.hom_inv_id_assoc, 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 : C
inst_3 : HopfObj A
slice_lhs :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Δ ≫
        (((CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
                  (A ◁ ε ▷ A) (A ◁ η ▷ A) ≫
                A ◁ Iso.hom (β_ A A)) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      (((((((A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  A ◁ Iso.inv (α_ A A A)) ≫
                A ◁ μ ▷ A) ≫
              A ◁ Iso.hom (β_ A A)) ≫
            A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 3 7 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.hom_inv_id_assoc, 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 : C
inst_3 : HopfObj A
a : A ◁ (Δ ≫ ε ▷ A)
| A ◁ Δ ≫ A ◁ ε ▷ A

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ Iso.inv (λ_ A)
| A ◁ (Δ ≫ ε ▷ A)

Tactic:
rw [ComonObj.counit_comul]

Premises used: CategoryTheory.ComonObj.counit_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 : C
inst_3 : HopfObj A
a : A ◁ Iso.inv (λ_ A)
| A ◁ Δ ≫ A ◁ ε ▷ A

Tactic:
simp only [← whiskerLeft_comp]
    rw [ComonObj.counit_comul]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.ComonObj.counit_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 : C
inst_3 : HopfObj A
slice_lhs :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      ((((A ◁ Iso.inv (λ_ A) ≫ A ◁ η ▷ A) ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Δ ≫
        (((CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
                  (A ◁ ε ▷ A) (A ◁ η ▷ A) ≫
                A ◁ Iso.hom (β_ A A)) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 2 3 =>
    simp only [← whiskerLeft_comp]
    rw [ComonObj.counit_comul]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.ComonObj.counit_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 : C
inst_3 : HopfObj A
a : A ◁ (η ▷ A ≫ Iso.hom (β_ A A))
| A ◁ η ▷ A ≫ A ◁ Iso.hom (β_ A A)

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ η)
| A ◁ (η ▷ A ≫ Iso.hom (β_ A A))

Tactic:
rw [BraidedCategory.braiding_naturality_left]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_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
a : A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η
| A ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ η)

Tactic:
simp only [whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η
| A ◁ η ▷ A ≫ A ◁ Iso.hom (β_ A A)

Tactic:
simp only [← whiskerLeft_comp]
    rw [BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality_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
slice_lhs :
  Δ ≫
      A ◁ Iso.inv (λ_ A) ≫
        (((A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A =
    ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      ((((A ◁ Iso.inv (λ_ A) ≫ A ◁ η ▷ A) ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.BraidedCategory.braiding_naturality_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
a : A ◁ (A ◁ η ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A)
| A ◁ A ◁ η ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A

Tactic:
simp only [← whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
| A ◁ (A ◁ η ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A)

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 : C
inst_3 : HopfObj A
a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η
| A ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)

Tactic:
simp only [whiskerLeft_comp]

Premises used: 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 : C
inst_3 : HopfObj A
a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η
| A ◁ A ◁ η ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A

Tactic:
simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, 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 : C
inst_3 : HopfObj A
slice_lhs :
  Δ ≫
      A ◁ Iso.inv (λ_ A) ≫
        A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫
          ((A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η) ≫ Iso.inv (α_ A A A)) ≫
            μ ▷ A =
    ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
⊢ Δ ≫
      A ◁ Iso.inv (λ_ A) ≫
        (((A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A =
    ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    simp only [whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, 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 : C
inst_3 : HopfObj A
a : Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η
| A ◁ A ◁ η ≫ Iso.inv (α_ A A A) ≫ μ ▷ A

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc