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
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) η ε)
| 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
    rw [antipode_left_assoc]

Premises used: CategoryTheory.HopfObj.antipode_left_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.{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 ≫ μ ≫ ε))
⊢ 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 := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε))

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

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

Tactic:
rw [Bimon.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.Bimon.mul_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 : C
inst_3 : HopfObj A
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (A ◁ ε ≫
        @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          ε ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε)
⊢ Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@antipode _ _ inst_1 inst_2 _ _ ≫ ε) ε

Tactic:
simpa [unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal
-- 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.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
| Δ ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ A ◁ Δ

Tactic:
rw [← associator_naturality_right, ← Category.assoc, ← tensorHom_def]

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

Tactic:
slice_lhs 3 5 =>
    rw [← associator_naturality_right, ← Category.assoc, ← tensorHom_def]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.associator_naturality_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 : μ ≫ Δ
| (Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          A ◁ Iso.hom (α_ A A A) ≫ Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ (μ ⊗ₘ μ)

Tactic:
rw [Bimon.compatibility]

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

Tactic:
slice_lhs 3 9 =>
    rw [Bimon.compatibility]

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

Tactic:
slice_lhs 1 3 =>
    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
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ Δ)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
simp [MonObj.tensorObj.one_def]

Premises used: CategoryTheory.MonObj.tensorObj.one_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 : C
inst_3 : HopfObj A
a : A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A
| A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)

Tactic:
simp only [tensorHom_def', whiskerLeft_comp]

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

Tactic:
slice_lhs 6 6 =>
    simp only [tensorHom_def', whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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 : C
inst_3 : HopfObj A
a : A ◁ Iso.inv (α_ A A A) ≫ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A
| A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.inv (α_ A A A)

Tactic:
rw [← whiskerLeft_comp, associator_inv_naturality_middle, whiskerLeft_comp]

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

Tactic:
slice_lhs 7 8 =>
    rw [← whiskerLeft_comp, associator_inv_naturality_middle, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.associator_inv_naturality_middle
-- 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 (β_ A A) ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A
| A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ A ◁ Iso.hom (β_ A A) ▷ A

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight, BraidedCategory.braiding_naturality_right,
      comp_whiskerRight, whiskerLeft_comp]

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

Tactic:
slice_lhs 8 9 =>
    rw [← whiskerLeft_comp, ← comp_whiskerRight, BraidedCategory.braiding_naturality_right,
      comp_whiskerRight, whiskerLeft_comp]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right, CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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 ◁ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A
| A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A ≫ A ◁ Iso.hom (α_ A A A)

Tactic:
rw [← whiskerLeft_comp, associator_naturality_left, whiskerLeft_comp]

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

Tactic:
slice_lhs 9 10 =>
    rw [← whiskerLeft_comp, associator_naturality_left, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.associator_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 ◁ Iso.hom (β_ A A)
| A ◁ A ◁ Iso.hom (β_ A A) ≫ A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _

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

Tactic:
slice_lhs 5 6 =>
    rw [← whiskerLeft_comp, ← whiskerLeft_comp, ← BraidedCategory.braiding_naturality_left,
      whiskerLeft_comp, 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 ◁ μ ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A
| Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ (μ ⊗ₘ μ)

Tactic:
rw [tensorHom_def', ← Category.assoc, ← associator_inv_naturality_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.associator_inv_naturality_right, 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 : 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 ◁ @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))) ≫ (η ⊗ₘ η))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) 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) ≫
                Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
              (μ ⊗ₘ μ))))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
slice_lhs 11 12 =>
    rw [tensorHom_def', ← Category.assoc, ← associator_inv_naturality_right]

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

Tactic:
rw [← whiskerLeft_comp, ← whisker_exchange, whiskerLeft_comp]

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