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

Tactic:
slice_lhs 1 2 =>
    dsimp
    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
a : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
| η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A)

Tactic:
rw [rightUnitor_naturality]

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

Tactic:
slice_lhs 2 3 =>
    rw [rightUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- 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 (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((ε ⊗ₘ ε) ≫ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)

Tactic:
monoidal
-- 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
hba : HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _) μ = 1
hac :
  HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) μ
      ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ) =
    1
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _)
    ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ)

Tactic:
apply left_inv_eq_right_inv
    (M := Conv (A ⊗ A) A)
    (a := μ[A])

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 : C
inst_3 : HopfObj A
hba :
  CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
      ((μ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
⊢ HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _) μ = 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 : C
inst_3 : HopfObj A
hba :
  (Δ ⊗ₘ Δ) ≫
      tensorμ A A A A ≫
        Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
          μ ▷ A ▷ A ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
      ((μ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η

Tactic:
simp only [Comon.tensorObj_comul, whiskerRight_tensor, comp_whiskerRight, Category.assoc,
      Comon.tensorObj_counit]

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

Tactic:
simp only [tensorμ]

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

Tactic:
simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]

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

Tactic:
mul_antipode₁ A

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

Tactic:
exact mul_antipode₁ A

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

Tactic:
simp only [Comon.tensorObj_comul, whiskerRight_tensor,
      BraidedCategory.braiding_naturality_assoc, whiskerLeft_comp, Category.assoc,
      Comon.tensorObj_counit]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comon.tensorObj_comul, CategoryTheory.MonoidalCategory.whiskerRight_tensor, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Comon.tensorObj_counit, CategoryTheory.BraidedCategory.braiding_naturality_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
hac :
  (Δ ⊗ₘ Δ) ≫
      (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
⊢ (Δ ⊗ₘ Δ) ≫
      tensorμ A A A A ≫
        Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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:
simp only [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- 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
hac :
  Eq (α := Conv (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))) ≫ η)
⊢ (Δ ⊗ₘ Δ) ≫
      (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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:
simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_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
⊢ Eq (α := Conv (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:
mul_antipode₂ A

Premises used: CategoryTheory.HopfObj.mul_antipode₂, CategoryTheory.Conv
-- 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 (α := Conv (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:
exact mul_antipode₂ A

Premises used: CategoryTheory.HopfObj.mul_antipode₂
-- 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hba :
  HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _)
      (@antipode _ _ inst_1 inst_2 _ _) =
    1
hac : HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _) (𝟙 A) = 1
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) (𝟙 A)

Tactic:
apply left_inv_eq_right_inv
    (M := Conv A A)
    (a := 𝒮[A])

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 : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hba :
  Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
        A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _)
      (@antipode _ _ inst_1 inst_2 _ _) =
    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 : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hba :
  Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
        A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (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 : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hba :
  Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ @antipode _ _ inst_1 inst_2 _ _))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)

Tactic:
rw [← comm, ← tensorHom_def_assoc, ← mul_antipode]

Premises used: CategoryTheory.HopfObj.mul_antipode, 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ @antipode _ _ inst_1 inst_2 _ _))
    (CategoryStruct.comp (Y := 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hac :
  Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ 𝟙 A ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _) (𝟙 A) = 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 : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ 𝟙 A ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η X ≫ A.map f : tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η Y :
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ Mon.X (functorObjObj A Y)) (η ≫ A.map f) η

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η X ≫ A.map f : tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η Y :
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)

Tactic:
rw [← η[A].naturality, tensorUnit_map]

Premises used: CategoryTheory.Monoidal.tensorUnit_map, CategoryTheory.MonObj.one, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)
⊢ Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
rw rw₁ :
  Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η Y :
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)
    (NatTrans.app η Y)
⊢ Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp