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_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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      (((((((A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  A ◁ Iso.inv (α_ A A A)) ≫
                A ◁ μ ▷ A) ≫
              A ◁ Iso.hom (β_ A A)) ≫
            A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (Δ ≫
    A ◁ Δ ≫
      (((CategoryStruct.comp (Y :=
                tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
                (A ◁ ε ▷ A) (A ◁ η ▷ A) ≫
              A ◁ Iso.hom (β_ A A)) ≫
            A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 3 7 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]
-- 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.inv (λ_ A)
Tactic: rw [ComonObj.counit_comul]
-- 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.inv (λ_ A)
Tactic: simp only [← whiskerLeft_comp]
    rw [ComonObj.counit_comul]
    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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Δ ≫
        (((CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
                  (A ◁ ε ▷ A) (A ◁ η ▷ A) ≫
                A ◁ Iso.hom (β_ A A)) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (Δ ≫
    ((((A ◁ Iso.inv (λ_ A) ≫ A ◁ η ▷ A) ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
        Iso.inv (α_ A A A)) ≫
      μ ▷ A)
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 2 3 =>
    simp only [← whiskerLeft_comp]
    rw [ComonObj.counit_comul]
    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 ◁ Iso.hom (β_ A A)
have a : 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 ◁ (η ▷ A ≫ Iso.hom (β_ A A))
have a : A ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 ◁ (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ η)
have a : A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 ≫ A ◁ Iso.hom (β_ A A)
have a : A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ 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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      ((((A ◁ Iso.inv (λ_ A) ≫ A ◁ η ▷ A) ≫ A ◁ Iso.hom (β_ A A)) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Δ ≫
    A ◁ Iso.inv (λ_ A) ≫
      (((A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η) ≫
            A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
          Iso.inv (α_ A A A)) ≫
        μ ▷ A =
  ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
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 ◁ A ◁ η ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A
have a : A ◁ (A ◁ η ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ 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 ◁ η ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A)
have a : A ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ 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 ◁ (@antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
have a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ 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 ◁ η ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A
have a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η
Tactic: simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    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.inv (λ_ A) ≫
        (((A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫ A ◁ A ◁ η) ≫
              A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
            Iso.inv (α_ A A A)) ≫
          μ ▷ A =
    ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
have slice_lhs : Δ ≫
    A ◁ Iso.inv (λ_ A) ≫
      A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫
        ((A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η) ≫ Iso.inv (α_ A A A)) ≫
          μ ▷ A =
  ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
Tactic: slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    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 ◁ η ≫ Iso.inv (α_ A A A) ≫ μ ▷ A
have a : Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η
Tactic: rw [associator_inv_naturality_right_assoc, 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 ◁ Iso.inv (λ_ A) ≫
        A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫
          ((A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ A ◁ η) ≫ Iso.inv (α_ A A A)) ≫
            μ ▷ A =
    ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (Δ ≫
    A ◁ Iso.inv (λ_ A) ≫
      A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫
        A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 5 7 =>
    rw [associator_inv_naturality_right_assoc, 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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (Δ ≫
      A ◁ Iso.inv (λ_ A) ≫
        A ◁ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A) ≫
          A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
            Iso.inv (α_ A A (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have simp : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (η ≫ Iso.inv (ρ_ A) ≫ A ◁ η))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: simp only [braiding_tensorUnit_left,
    whiskerLeft_comp, whiskerLeft_rightUnitor_inv,
    whiskerRight_id, whiskerLeft_rightUnitor, Category.assoc, Iso.hom_inv_id_assoc,
    Iso.inv_hom_id_assoc, whiskerLeft_inv_hom_assoc, antipode_right_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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (η ≫ Iso.inv (ρ_ A) ≫ A ◁ η))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have rw : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (ε ≫ Iso.inv (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η)
Tactic: rw [rightUnitor_inv_naturality_assoc, 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.{v₁ + 1} (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ Δ)
    (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _))
have hba : HMul.hMul (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (@antipode _ _ inst_1 inst_2 _ _ ≫ Δ) Δ = 1
Tactic: apply left_inv_eq_right_inv
    (M := Conv A (A ⊗ A))
    (a := Δ[A])
-- 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
hba : HMul.hMul (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (@antipode _ _ inst_1 inst_2 _ _ ≫ Δ) Δ = 1
⊢ Eq.{v₁ + 1} (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ Δ)
    (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _))
have hac : HMul.hMul (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
    (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) =
  1
Tactic: apply left_inv_eq_right_inv
    (M := Conv A (A ⊗ A))
    (a := Δ[A])
-- 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
⊢ HMul.hMul (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (@antipode _ _ inst_1 inst_2 _ _ ≫ Δ) Δ = 1
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    ((@antipode _ _ inst_1 inst_2 _ _ ≫ Δ) ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Δ ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- 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) Δ
      ((@antipode _ _ inst_1 inst_2 _ _ ≫ Δ) ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Δ ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : Eq (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
  (Δ ≫
    @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
      Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫ Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: simp only [comp_whiskerRight, tensor_whiskerLeft, MonObj.tensorObj.mul_def, Category.assoc,
      MonObj.tensorObj.one_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 (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
    (Δ ≫
      @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        Δ ▷ A ≫
          Iso.hom (α_ A A A) ≫
            A ◁ A ◁ Δ ≫ Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have hba : Eq (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
      Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            Iso.inv (α_ 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: simp only [tensorμ]
-- 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 (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        Δ ▷ A ≫
          Iso.hom (α_ A A A) ≫
            A ◁ A ◁ Δ ≫
              Iso.inv (α_ 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have hba : Eq (α := Conv 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: simp only [Category.assoc, Iso.inv_hom_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
⊢ HMul.hMul (α := Conv A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
      (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) =
    1
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
          (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
        μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- 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 ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
            (Δ ≫ Iso.hom (β_ A A) ≫ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
          μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : Eq (α := Conv A (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 _ _) ≫
              Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: simp only [whiskerLeft_comp, tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc,
      MonObj.tensorObj.mul_def, MonObj.tensorObj.one_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 (α := Conv A (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 _ _) ≫
                Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have hac : Eq (α := Conv 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 _ _) ≫
              Iso.inv (α_ 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: simp only [tensorμ]
-- 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 (α := Conv 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 _ _) ≫
                Iso.inv (α_ 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.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have hac : Eq (α := Conv 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: simp only [Category.assoc, Iso.inv_hom_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
| @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A ≫ Iso.hom (α_ A A A)
have a : Iso.hom (α_ A A A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A
Tactic: rw [associator_naturality_left]