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
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫ Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ (μ ⊗ₘ μ)))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ Iso.hom (β_ A A) ≫
            (((((A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                      A ◁ Iso.inv (α_ A A A)) ≫
                    A ◁ Iso.hom (β_ A A) ▷ A) ≫
                  A ◁ Iso.hom (α_ A A A)) ≫
                Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
              (μ ⊗ₘ μ)))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 6 6 =>
    simp only [tensorHom_def', 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 ≫ A ◁ Iso.inv (α_ A A A)
have a : A ◁ Iso.inv (α_ A A A) ≫ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A
Tactic: rw [← whiskerLeft_comp, associator_inv_naturality_middle, 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              (((((A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                        A ◁ Iso.inv (α_ A A A)) ≫
                      A ◁ Iso.hom (β_ A A) ▷ A) ≫
                    A ◁ Iso.hom (α_ A A A)) ≫
                  Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                (μ ⊗ₘ μ)))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ Iso.hom (β_ A A) ≫
            A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
              ((((A ◁ Iso.inv (α_ A A A) ≫ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A) ≫ A ◁ Iso.hom (β_ A A) ▷ A) ≫
                    A ◁ Iso.hom (α_ A A A)) ≫
                  Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                (μ ⊗ₘ μ)))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 7 8 =>
    rw [← whiskerLeft_comp, associator_inv_naturality_middle, 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 ≫ A ◁ Iso.hom (β_ A A) ▷ A
have a : A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A
Tactic: rw [← whiskerLeft_comp, ← comp_whiskerRight, BraidedCategory.braiding_naturality_right,
      comp_whiskerRight, 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
                ((((A ◁ Iso.inv (α_ A A A) ≫ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _) ▷ A) ≫
                        A ◁ Iso.hom (β_ A A) ▷ A) ≫
                      A ◁ Iso.hom (α_ A A A)) ≫
                    Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                  (μ ⊗ₘ μ)))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ Iso.hom (β_ A A) ≫
            A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
              A ◁ Iso.inv (α_ A A A) ≫
                (((A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                    Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                  (μ ⊗ₘ μ)))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 8 9 =>
    rw [← whiskerLeft_comp, ← comp_whiskerRight, BraidedCategory.braiding_naturality_right,
      comp_whiskerRight, 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 ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A ≫ A ◁ Iso.hom (α_ A A A)
have a : A ◁ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A
Tactic: rw [← whiskerLeft_comp, associator_naturality_left, 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  (((A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ▷ A) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                      Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                    (μ ⊗ₘ μ)))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ Iso.hom (β_ A A) ≫
            A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
              A ◁ Iso.inv (α_ A A A) ≫
                A ◁ Iso.hom (β_ A A) ▷ A ≫
                  ((A ◁ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                    (μ ⊗ₘ μ)))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 9 10 =>
    rw [← whiskerLeft_comp, associator_naturality_left, 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) ≫ A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ A ◁ Iso.hom (β_ A A)
Tactic: rw [← whiskerLeft_comp, ← whiskerLeft_comp, ← BraidedCategory.braiding_naturality_left,
      whiskerLeft_comp, 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    ((A ◁ Iso.hom (α_ A A A) ≫
                          A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                        Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                      (μ ⊗ₘ μ)))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)))
          (A ◁ A ◁ Δ)
          (((((((A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ A ◁ Iso.hom (β_ A A)) ≫ A ◁ Iso.inv (α_ A A A)) ≫
                    A ◁ Iso.hom (β_ A A) ▷ A) ≫
                  A ◁ Iso.hom (α_ A A A)) ≫
                A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
              Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
            (μ ⊗ₘ μ))))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 5 6 =>
    rw [← whiskerLeft_comp, ← whiskerLeft_comp, ← BraidedCategory.braiding_naturality_left,
      whiskerLeft_comp, 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
| Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ (μ ⊗ₘ μ)
have a : (A ◁ A ◁ μ ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A
Tactic: rw [tensorHom_def', ← Category.assoc, ← associator_inv_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
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)))
            (A ◁ A ◁ Δ)
            (((((((A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ A ◁ Iso.hom (β_ A A)) ≫ A ◁ Iso.inv (α_ A A A)) ≫
                      A ◁ Iso.hom (β_ A A) ▷ A) ≫
                    A ◁ Iso.hom (α_ A A A)) ≫
                  A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
              (μ ⊗ₘ μ))))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ Iso.inv (α_ A A A) ≫
                A ◁ Iso.hom (β_ A A) ▷ A ≫
                  A ◁ Iso.hom (α_ A A A) ≫
                    A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫
                      (A ◁ A ◁ μ ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 11 12 =>
    rw [tensorHom_def', ← Category.assoc, ← associator_inv_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 ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ A ◁ μ
have a : A ◁ A ◁ μ ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A
Tactic: rw [← whiskerLeft_comp, ← whisker_exchange, 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              A ◁ A ◁ Iso.hom (β_ A A) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫
                      A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫
                        (A ◁ A ◁ μ ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
            A ◁ A ◁ Iso.hom (β_ A A) ≫
              A ◁ Iso.inv (α_ A A A) ≫
                A ◁ Iso.hom (β_ A A) ▷ A ≫
                  A ◁ Iso.hom (α_ A A A) ≫
                    ((A ◁ A ◁ μ ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ Iso.inv (α_ A A A)) ≫ μ ▷ A))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 10 11 =>
    rw [← whiskerLeft_comp, ← whisker_exchange, 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) ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ μ
have a : A ◁ (A ◁ Iso.hom (β_ A A) ≫ Iso.inv (α_ A A A) ≫ Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ A 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 ◁ Iso.hom (β_ A A) ≫ Iso.inv (α_ A A A) ≫ Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ μ)
have a : A ◁ (Iso.inv (α_ A A A) ≫ μ ▷ A ≫ Iso.hom (β_ A A))
Tactic: rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← 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.inv (α_ A A A) ≫ μ ▷ A ≫ Iso.hom (β_ A A))
have a : A ◁ Iso.inv (α_ A A A) ≫ 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) ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ μ
have a : A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ Iso.hom (β_ A A)
Tactic: simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← 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)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (Δ ▷ A ≫
        Iso.hom (α_ A A A) ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
              A ◁ A ◁ Iso.hom (β_ A A) ≫
                A ◁ Iso.inv (α_ A A A) ≫
                  A ◁ Iso.hom (β_ A A) ▷ A ≫
                    A ◁ Iso.hom (α_ A A A) ≫
                      ((A ◁ 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.hom (α_ A A 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))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 6 10 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← 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.hom (α_ A A 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 rw : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (Δ ≫
    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))) ≫ (η ⊗ₘ η))
Tactic: rw [ComonObj.comul_assoc_flip_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
| 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 ◁ (Δ ≫ Δ ▷ A ≫ Iso.hom (α_ A A A))
Tactic: rw [ComonObj.comul_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
| A ◁ (Δ ≫ Δ ▷ A ≫ Iso.hom (α_ A A A))
have a : A ◁ Δ ≫ A ◁ Δ ▷ 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 ◁ Δ ≫ A ◁ A ◁ Δ
have a : A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ Iso.hom (α_ A A A)
Tactic: simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    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 ◁ 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 ◁ Δ ≫ 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))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 2 3 =>
    simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    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 A) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A
have a : A ◁ (Δ ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.inv (α_ A 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 ≫ Iso.hom (α_ A A A) ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ Iso.inv (α_ A A A) ≫ μ ▷ A)
have 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)
Tactic: rw [← associator_naturality_middle_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
| 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 : 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
| A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ) ▷ A
have a : 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
| A ◁ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ▷ A
have a : 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
| A ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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]