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

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

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

Tactic:
slice_lhs 7 8 =>
    rw [associator_naturality_left]

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

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

Tactic:
slice_lhs 9 10 =>
    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 : Iso.inv (α_ A A A) ≫ μ ▷ A ≫ μ
| A ◁ μ ≫ μ

Tactic:
rw [MonObj.mul_assoc_flip]

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

Tactic:
slice_lhs 11 12 =>
    rw [MonObj.mul_assoc_flip]

Premises used: CategoryTheory.MonObj.mul_assoc_flip
-- 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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ A ▷ A
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ Iso.inv (α_ A A A)

Tactic:
rw [associator_inv_naturality_left]

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

Tactic:
slice_lhs 10 11 =>
    rw [associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_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
| μ ▷ A ▷ 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 : (Iso.hom (α_ A A A) ≫ A ◁ μ ≫ μ) ▷ A
| (μ ▷ A ≫ μ) ▷ A

Tactic:
rw [MonObj.mul_assoc]

Premises used: CategoryTheory.MonObj.mul_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 : Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A
| (Iso.hom (α_ A A A) ≫ 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 : Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A
| μ ▷ A ▷ A ≫ μ ▷ A

Tactic:
simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    simp only [comp_whiskerRight]

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

Tactic:
slice_lhs 11 12 =>
    simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    simp only [comp_whiskerRight]

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

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

Tactic:
rw [tensor_whiskerLeft _ _ (β_ A A).hom]

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

Tactic:
rw [pentagon_inv_inv_hom_hom_inv_assoc]

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

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id