awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A
have a : CategoryStruct.comp (Y :=
  tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A)) (A ◁ ε ▷ A)
  (A ◁ η ▷ A)
Tactic: simp only [← whiskerLeft_comp]
    rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ≫
          ((((((A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      A ◁ Iso.hom (β_ A A) ≫
        A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
          (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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 5 9 =>
    simp only [← whiskerLeft_comp]
    rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ μ
have a : A ◁ (η ▷ A ≫ μ)
Tactic: simp only [← whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ≫ μ)
have a : A ◁ Iso.hom (λ_ A)
Tactic: rw [MonObj.one_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ μ
have a : A ◁ Iso.hom (λ_ A)
Tactic: simp only [← whiskerLeft_comp]
    rw [MonObj.one_mul]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ≫
          A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
            (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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      A ◁ Iso.hom (β_ A A) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ ε ▷ A ≫ A ◁ Iso.hom (λ_ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [MonObj.one_mul]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ (Iso.hom (β_ A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _)
Tactic: simp only [← whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ @antipode _ _ inst_1 inst_2 _ _)
have a : A ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.hom (β_ A A))
Tactic: rw [← BraidedCategory.braiding_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.hom (β_ A A))
have a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.hom (β_ A A)
Tactic: simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.hom (β_ A A)
Tactic: simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ ε ▷ A ≫ A ◁ Iso.hom (λ_ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ ε ▷ A) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
have a : A ◁ (Iso.hom (β_ A A) ≫ ε ▷ A)
Tactic: simp only [← whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
have a : A ◁ (A ◁ ε ≫ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [← BraidedCategory.braiding_naturality_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have a : A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
have a : A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ ε ▷ A) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        ((A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
          ((A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
      Iso.hom (α_ A A A) ≫
        ((A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: rw [← associator_naturality_middle_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
        Iso.hom (α_ A A A) ≫
          ((A ◁ A ◁ ε ≫ A ◁ Iso.hom (β_ A (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫ A ◁ Iso.hom (λ_ A)) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
      Iso.hom (α_ A A A) ≫
        CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
            (A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ A ◁ Iso.inv (λ_ A)) (A ◁ Iso.hom (λ_ A)) ≫
          μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: simp only [braiding_tensorUnit_right, whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
    (A ◁ Iso.inv (λ_ A)) (A ◁ Iso.hom (λ_ A))
have a : A ◁
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (Iso.inv (λ_ A))
    (Iso.hom (λ_ A))
Tactic: simp only [← whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (Iso.inv (λ_ A))
      (Iso.hom (λ_ A))
have a : A ◁ 𝟙 A
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
    (A ◁ Iso.inv (λ_ A)) (A ◁ Iso.hom (λ_ A))
have a : A ◁ 𝟙 A
Tactic: simp only [← whiskerLeft_comp]
    rw [Iso.inv_hom_id]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
        Iso.hom (α_ A A A) ≫
          CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
              (A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ A ◁ Iso.inv (λ_ A)) (A ◁ Iso.hom (λ_ A)) ≫
            μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ A ◁ 𝟙 A ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [Iso.inv_hom_id]
    simp only [whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫
      (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ A ◁ 𝟙 A ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: simp only [whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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) ≫ μ
have a : Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A)
Tactic: rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (Δ ▷ A ≫ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ A ◁ ε ≫ A ◁ Iso.hom (ρ_ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Δ ▷ A ≫
    (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ ε ≫
          Iso.inv (α_ 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 5 6 =>
    rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 _ _) ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ ε ≫
            Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A) =
    (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
have rw : Δ ▷ A ≫
    (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ ε ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A) =
  (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
Tactic: rw [associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ ε ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
have a : μ ▷ A ≫ A ◁ ε
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 _ _) ▷ A ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ ε ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A) =
    (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) 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 ◁ ε) ≫ Iso.hom (ρ_ A)))
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 3 4 =>
    rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (Δ ▷ A)
    ((A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ μ ▷ A)
have a : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ) ▷ A
Tactic: simp only [← comp_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ) ▷ A
have a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ▷ A
Tactic: rw [antipode_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ▷ A
have a : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A)
Tactic: simp only [comp_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (Δ ▷ A)
    ((A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ μ ▷ A)
have a : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A)
Tactic: simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (Δ ▷ A)
      ((A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ (μ ▷ A ≫ A ◁ ε) ≫ Iso.hom (ρ_ A)))
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A) ≫
      A ◁ ε) ≫
    Iso.hom (ρ_ A))
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 1 3 =>
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ◁ ε
have a : tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ ε ≫ η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    ((CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) (ε ▷ A) (η ▷ A) ≫
        A ◁ ε) ≫
      Iso.hom (ρ_ A))
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : 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 2 3 =>
    rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ ε
have a : ε ⊗ₘ ε
Tactic: rw [← tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ ε
have a : ε ⊗ₘ ε
Tactic: dsimp
    rw [← tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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)
    (ε ▷ A ≫ (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ ε ≫ η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ Iso.hom (ρ_ A))
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have 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))) ≫ η)
Tactic: slice_lhs 1 2 =>
    dsimp
    rw [← tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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
| η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ A)
have a : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
Tactic: rw [rightUnitor_naturality]