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 (α := 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))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              μ ▷ A ▷ A ≫
                ((Iso.hom (α_ A A A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫ A ◁ μ) ≫
                  μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 8 9 =>
    rw [associator_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
| @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ
have a : A ◁ μ ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ 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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                μ ▷ A ▷ A ≫
                  ((Iso.hom (α_ A A A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      A ◁ μ) ≫
                    μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫ μ ▷ A ▷ A ≫ Iso.hom (α_ A A A) ≫ (A ◁ μ ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 9 10 =>
    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 ≫ Iso.hom (α_ A A A)
have a : Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A
Tactic: rw [associator_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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                μ ▷ A ▷ A ≫ Iso.hom (α_ A A A) ≫ (A ◁ μ ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              (((Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                    A ◁ μ) ≫
                  @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 7 8 =>
    rw [associator_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
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                (((Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      A ◁ μ) ≫
                    @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫
                  μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : (Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                ((μ ⊗ₘ μ) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A) ≫ μ =
  (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
Tactic: slice_lhs 8 9 =>
    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)
    ((Δ ⊗ₘ Δ) ≫
      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))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              ((((Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      A ◁ Iso.hom (β_ A A)) ≫
                    A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
                  A ◁ μ) ≫
                μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 7 8 =>
    rw [associator_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
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ Iso.hom (β_ A A)
have a : tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) 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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                ((((Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                        A ◁ Iso.hom (β_ A A)) ≫
                      A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
                    A ◁ μ) ≫
                  μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : (Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                (((tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
                    A ◁ μ) ≫
                  μ =
  (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
Tactic: slice_lhs 8 9 =>
    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
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)
have a : tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
  μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) 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
⊢ (Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  (((tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫ μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                        A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
                      A ◁ μ) ≫
                    μ =
    (ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                  ((tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                          (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                        μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                      A ◁ μ) ≫
                    μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 9 10 =>
    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 ◁ μ ≫ μ
have a : Iso.inv (α_ A A A) ≫ μ ▷ A ≫ μ
Tactic: rw [MonObj.mul_assoc_flip]
-- 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)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                    ((tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                            (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                          μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A) ≫
                        A ◁ μ) ≫
                      μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                      (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                    μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ Iso.inv (α_ A A A) ≫ μ ▷ A ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 11 12 =>
    rw [MonObj.mul_assoc_flip]
-- 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 ≫ Iso.inv (α_ A A A)
have a : Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ A ▷ A
Tactic: rw [associator_inv_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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                        (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                      μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ Iso.inv (α_ A A A) ≫ μ ▷ A ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                      (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                    ((Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ A ▷ A) ≫ μ ▷ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 10 11 =>
    rw [associator_inv_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 ▷ A ≫ μ ▷ A
have 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 ≫ μ) ▷ A
have a : (Iso.hom (α_ A A A) ≫ A ◁ μ ≫ μ) ▷ A
Tactic: rw [MonObj.mul_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
| (Iso.hom (α_ A A A) ≫ A ◁ μ ≫ μ) ▷ A
have a : Iso.hom (α_ A A A) ▷ A ≫ (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 ▷ A ≫ μ ▷ A
have a : Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A
Tactic: simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    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)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                        (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                      ((Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫ μ ▷ A ▷ A) ≫ μ ▷ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ⊗ₘ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                      (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                      (Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 11 12 =>
    simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    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)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                        (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                        (Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                      (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                      (Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    ((Δ ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Δ) ≫
      Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
        A ◁ Iso.inv (α_ A A A) ≫
          A ◁ Iso.hom (β_ A A) ▷ A ≫
            Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
              Iso.inv (α_ A A A) ▷ A ≫
                Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Iso.hom (β_ A A) ≫
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                        (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                        (Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  ((Δ ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ Δ) ≫
    Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
      A ◁ Iso.inv (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ▷ A ≫
          Iso.inv (α_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
            Iso.inv (α_ A A A) ▷ A ≫
              Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                (Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
                    A ◁ A ◁ Iso.hom (β_ A A) ≫ Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))) ≫
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁
                      (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A A) ≫
                      (Iso.hom (α_ A A A) ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: rw [tensor_whiskerLeft _ _ (β_ A A).hom]