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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
slice_lhs :
  Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have hba : Eq.{v₁ + 1} (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]
-- 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ f * @antipode _ _ inst_1 inst_2 _ _ ≫ f = 1
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (f ▷ A ≫ B ◁ (@antipode _ _ inst_1 inst_2 _ _ ≫ f) ≫ μ) =
  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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ (@antipode _ _ inst_1 inst_2 _ _ ≫ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ B ◁ f ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: simp only [whiskerLeft_comp, Category.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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _
have a : A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ B ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ A) ≫ B ◁ f) ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 2 3 =>
      rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ f ▷ A) ≫ B ◁ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ (f ⊗ₘ f) ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 3 4 =>
      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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| (f ⊗ₘ f) ≫ μ
have a : μ ≫ f
Tactic: rw [← IsMonHom.mul_hom]
-- 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ (f ⊗ₘ f) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ ≫ f) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 3 4 =>
      rw [← IsMonHom.mul_hom]
-- 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ)
have a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ ≫ f) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 1 3 =>
      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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| η ≫ f
have a : η
Tactic: rw [IsMonHom.one_hom]
-- 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have slice_lhs : Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 2 3 =>
      rw [IsMonHom.one_hom]
-- 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 B : C
inst_3 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
slice_lhs :
  Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
⊢ Eq (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ f)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have hac : Eq.{v₁ + 1} (α := Conv A B) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 2 3 =>
      rw [IsMonHom.one_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A) (η ≫ @antipode _ _ inst_1 inst_2 _ _) η
have this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
  (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
  (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
Tactic: have := (rfl : η[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
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
| Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
have rhs : η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ)
Tactic: rhs
-- 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
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
| η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ)
have rw : CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: rw [antipode_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
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
| Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
have rw : CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: rhs
    rw [antipode_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A) (η ≫ @antipode _ _ inst_1 inst_2 _ _) η
have this₁ : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
  (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
  (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))
Tactic: conv at this =>
    rhs
    rw [antipode_left]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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
this :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
    (η ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ))
    (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A) (η ≫ @antipode _ _ inst_1 inst_2 _ _) η
have this₁ : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A)
  (η ≫ Iso.inv (ρ_ A) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ A ◁ η ≫ μ)
  (CategoryStruct.comp (Y := A) η (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η))
Tactic: rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal,
    ← rightUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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 ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@antipode _ _ inst_1 inst_2 _ _ ≫ ε) ε
have this : Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
Tactic: have := (rfl : Δ[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
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
| Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
have rhs : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε)
Tactic: rhs
-- 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
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε)
have rw : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε)
Tactic: rw [antipode_left_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
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
| Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
have rw : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε)
Tactic: rhs
    rw [antipode_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
⊢ Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@antipode _ _ inst_1 inst_2 _ _ ≫ ε) ε
have this₁ : Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε))
Tactic: conv at this =>
    rhs
    rw [antipode_left_assoc]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (hypothesis)
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
this :
  Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ ε))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε))
⊢ Eq.{v₁ + 1} (α := A ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@antipode _ _ inst_1 inst_2 _ _ ≫ ε) ε
have this₁ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (A ◁ ε ≫
      @antipode _ _ inst_1 inst_2 _ _ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
        ε ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (CategoryStruct.comp (Y := A) η ε)
Tactic: rw [Bimon.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this
Cleared hypotheses: this
-- 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 ◁ Δ
have a : (Δ ⊗ₘ Δ) ≫ Iso.hom (α_ A A (tensorObj.{v₁, u₁} (𝒞 := inst) A A))
Tactic: rw [← associator_naturality_right, ← Category.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 (α := 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))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (Δ ≫
    @antipode _ _ inst_1 inst_2 _ _ ▷ 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: slice_lhs 3 5 =>
    rw [← associator_naturality_right, ← Category.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
| (Δ ⊗ₘ Δ) ≫
    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)) ≫ (μ ⊗ₘ μ)
have a : μ ≫ Δ
Tactic: rw [Bimon.compatibility]
-- 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)
    (Δ ≫
      @antipode _ _ inst_1 inst_2 _ _ ▷ 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 slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ Δ))
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 3 9 =>
    rw [Bimon.compatibility]
-- 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 ≫ μ)
have a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [antipode_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 (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ Δ))
    (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
have slice_lhs : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) A A) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η ≫ Δ)
  (ε ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
Tactic: slice_lhs 1 3 =>
    rw [antipode_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 ◁ (@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _)
have a : A ◁ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ A ◁ A ◁ @antipode _ _ inst_1 inst_2 _ _ ▷ A
Tactic: simp only [tensorHom_def', whiskerLeft_comp]