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)
    ((Δ ▷ 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))) ≫ η)
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 ≫
          A ◁ Iso.hom (α_ A A A) ≫
            Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) 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 [pentagon_inv_inv_hom_hom_inv_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.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
have a : 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorObj.{v₁, u₁} (𝒞 := inst) 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
⊢ 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 ≫
            A ◁ Iso.hom (α_ A A A) ≫
              Iso.inv (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η)
have slice_lhs : Δ ▷ 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) ≫
              (((((((𝟙
                                (tensorObj.{v₁, u₁} (𝒞 := inst) A
                                  (tensorObj.{v₁, u₁} (𝒞 := inst) 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: slice_lhs 7 8 =>
    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
⊢ Δ ▷ 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) ≫
                (((((((𝟙
                                  (tensorObj.{v₁, u₁} (𝒞 := inst) A
                                    (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
have rw : Δ ▷ 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) ≫
              ((((((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 [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 A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ Iso.hom (β_ A A)
have a : A ◁ (Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ 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 ◁ (Iso.hom (β_ A A) ▷ A ≫ Iso.hom (α_ A A A) ≫ A ◁ Iso.hom (β_ A A))
have a : A ◁ (Iso.hom (α_ A A A) ≫ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ Iso.hom (α_ A A A))
Tactic: rw [← BraidedCategory.hexagon_forward]
-- 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) ≫ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ Iso.hom (α_ A A A))
have a : A ◁ Iso.hom (α_ A A A) ≫ A ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) 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 ◁ Iso.hom (β_ A A) ▷ A ≫ A ◁ Iso.hom (α_ A A A) ≫ A ◁ A ◁ Iso.hom (β_ A A)
have a : A ◁ Iso.hom (α_ A A A) ≫ A ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ A ◁ Iso.hom (α_ A A A)
Tactic: simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_forward]
    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 ≫
      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) ≫
                ((((((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))) ≫ η
have slice_lhs : Δ ▷ 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 (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ A ◁ Iso.hom (α_ A 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: slice_lhs 5 7 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_forward]
    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 ≫
      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 (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫ A ◁ Iso.hom (α_ A 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))) ≫ η
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      A ◁ A ◁ Δ ≫
        A ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
          A ◁ Iso.hom (α_ A A A) ≫
            A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
              A ◁ Iso.inv (α_ A A A) ≫ A ◁ μ ▷ A ≫ A ◁ μ ≫ μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: simp only [tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc, pentagon_inv_inv_hom_inv_inv,
    whisker_assoc, MonObj.mul_assoc, whiskerLeft_inv_hom_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 ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
have a : A ◁ (A ◁ Δ ≫ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := 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 ◁ Δ ≫ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)))
have a : A ◁ (Iso.hom (β_ A A) ≫ Δ ▷ A)
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 ◁ (Iso.hom (β_ A A) ≫ Δ ▷ A)
have 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 ◁ Δ ≫ A ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
have a : A ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A
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 ◁ A ◁ Δ ≫
          A ◁ Iso.hom (β_ A (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) ≫
            A ◁ Iso.hom (α_ A A A) ≫
              A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫
                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) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
              A ◁ Iso.inv (α_ A A A)) ≫
            A ◁ μ ▷ A) ≫
          A ◁ μ) ≫
        μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 3 4 =>
    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 ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                  A ◁ A ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)) ≫
                A ◁ Iso.inv (α_ A A A)) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      ((((((A ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                A ◁ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A)) ≫
              A ◁ Iso.inv (α_ 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 ≫
      Iso.hom (α_ A A A) ≫
        ((((((A ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A) ≫ A ◁ Iso.hom (α_ A A A)) ≫
                  A ◁ A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A)) ≫
                A ◁ Iso.inv (α_ A A A)) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
  (Δ ▷ A ≫
    Iso.hom (α_ A A A) ≫
      ((((((A ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A) ≫ A ◁ Iso.hom (α_ A 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 ◁ μ ▷ A) ≫
          A ◁ μ) ≫
        μ)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (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 ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ (Iso.hom (α_ A A 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) ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _)
have a : A ◁ (tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ Iso.hom (α_ A A A))
Tactic: rw [← associator_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 ◁ (tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ Iso.hom (α_ A A A))
have a : A ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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) ≫ A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ Iso.hom (α_ A A A)
Tactic: simp only [← whiskerLeft_comp]
    rw [← associator_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 ◁ Iso.hom (β_ A A) ≫ A ◁ Δ ▷ A) ≫ A ◁ Iso.hom (α_ A 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 ◁ μ ▷ 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 ≫
          (((((A ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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))) ≫ η)
Tactic: slice_lhs 5 6 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_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
| A ◁ Δ ▷ A ≫ A ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ (Δ ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) 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 ◁ (Δ ▷ A ≫ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _)
have a : 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
| A ◁ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ Δ ▷ A)
have a : A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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 ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A)
    (Δ ▷ A ≫
      Iso.hom (α_ A A A) ≫
        A ◁ Iso.hom (β_ A A) ≫
          A ◁ Δ ▷ A ≫
            (((((A ◁ tensorObj.{v₁, u₁} (𝒞 := inst) A A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ 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 _ _ ≫ 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))) ≫ η)
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.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_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]