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)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε ⊗ₘ ε)
        (η ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      Iso.hom (ρ_ A))
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
have slice_lhs : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) ((ε ⊗ₘ ε) ≫ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
  ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ η)
Tactic: slice_lhs 2 3 =>
    rw [rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _)
    ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ)
have hba : HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _) μ = 1
Tactic: apply left_inv_eq_right_inv
    (M := Conv (A ⊗ A) A)
    (a := μ[A])
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
hba : HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _) μ = 1
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _)
    ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ)
have hac : HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) μ
    ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ) =
  1
Tactic: apply left_inv_eq_right_inv
    (M := Conv (A ⊗ A) A)
    (a := μ[A])
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) (μ ≫ @antipode _ _ inst_1 inst_2 _ _) μ = 1
have hba : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
    ((μ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
      ((μ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫ A ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : (Δ ⊗ₘ Δ) ≫
    tensorμ A A A A ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
Tactic: simp only [Comon.tensorObj_comul, whiskerRight_tensor, comp_whiskerRight, Category.assoc,
      Comon.tensorObj_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 : C
inst_3 : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      tensorμ A A A A ≫
        Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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 hba : (Δ ⊗ₘ Δ) ≫
    (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
Tactic: simp only [tensorμ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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 hba : Eq (α := Conv (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))) ≫ η)
Tactic: simp only [Category.assoc, pentagon_hom_inv_inv_inv_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
⊢ HMul.hMul (α := Conv (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) μ
      ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ) =
    1
have hac : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
    (μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫
      A ◁ ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ) ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) Δ
      (μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) A A ≫
        A ◁ ((@antipode _ _ inst_1 inst_2 _ _ ⊗ₘ @antipode _ _ inst_1 inst_2 _ _) ≫ Iso.hom (β_ A A) ≫ μ) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hac : (Δ ⊗ₘ Δ) ≫
    tensorμ A A A A ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
Tactic: simp only [Comon.tensorObj_comul, whiskerRight_tensor,
      BraidedCategory.braiding_naturality_assoc, whiskerLeft_comp, Category.assoc,
      Comon.tensorObj_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 : C
inst_3 : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      tensorμ A A A A ≫
        Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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 hac : (Δ ⊗ₘ Δ) ≫
    (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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))) ≫ η
Tactic: simp only [tensorμ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) 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 hac : Eq (α := Conv (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))) ≫ η)
Tactic: simp only [Category.assoc, pentagon_hom_inv_inv_inv_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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) (𝟙 A)
have hba : HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _)
    (@antipode _ _ inst_1 inst_2 _ _) =
  1
Tactic: apply left_inv_eq_right_inv
    (M := Conv 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
hba :
  HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _)
      (@antipode _ _ inst_1 inst_2 _ _) =
    1
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) (𝟙 A)
have hac : HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _) (𝟙 A) = 1
Tactic: apply left_inv_eq_right_inv
    (M := Conv 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _)
      (@antipode _ _ inst_1 inst_2 _ _) =
    1
have hba : Eq.{v₁ + 1} (α := Conv A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    ((@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((@antipode _ _ inst_1 inst_2 _ _ ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫
        A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have hba : Eq.{v₁ + 1} (α := Conv A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
      @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: simp only [comp_whiskerRight, 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 : C
inst_3 : HopfObj A
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ Eq.{v₁ + 1} (α := Conv A A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫
        @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ @antipode _ _ inst_1 inst_2 _ _ ≫ μ))
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have hba : Eq.{v₁ + 1} (α := Conv A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ μ ≫ @antipode _ _ inst_1 inst_2 _ _))
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: rw [← comm, ← tensorHom_def_assoc, ← mul_antipode]
-- 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
comm : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) A A ⟶ A) (Iso.hom (β_ A A) ≫ μ) μ
⊢ HMul.hMul (α := Conv A A) (@antipode _ _ inst_1 inst_2 _ _) (𝟙 A) = 1
have hac : Eq.{v₁ + 1} (α := Conv A A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ A ◁ 𝟙 A ≫ μ))
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ Mon.X (functorObjObj A Y)) (η ≫ A.map f) η
have dsimp : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
  (NatTrans.app η X ≫ A.map f : tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
  (NatTrans.app η Y :
    Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η X ≫ A.map f : tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (NatTrans.app η Y :
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)
have rw : Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
  (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)
Tactic: rw [← η[A].naturality, tensorUnit_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ≫ NatTrans.app η Y) (NatTrans.app η Y)
have rw : Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_1) ⟶ A.obj Y)
  (NatTrans.app η Y :
    Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y ⟶ A.obj Y)
  (NatTrans.app η Y)
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (Mon.X (functorObjObj A X)) (Mon.X (functorObjObj A X)) ⟶
      Mon.X (functorObjObj A Y))
    (μ ≫ A.map f) ((A.map f ⊗ₘ A.map f) ≫ μ)
have dsimp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
  (NatTrans.app μ X ≫ A.map f : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
  ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    (NatTrans.app μ X ≫ A.map f : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
  ((tensorObj (𝒞 := Functor.category) A A).map f ≫ NatTrans.app μ Y) ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
Tactic: rw [← μ[A].naturality, tensorObj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((tensorObj (𝒞 := Functor.category) A A).map f ≫ NatTrans.app μ Y) ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    (NatTrans.app μ X ≫ A.map f : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
have rw₁ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y) ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
  ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
Tactic: rw [← μ[A].naturality, tensorObj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
⊢ Eq (α := Quiver.Hom (V := Mon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A X))
    { hom := A.map (𝟙 X), isMonHom_hom := ⋯ } (𝟙 (functorObjObj A X))
have w : Eq (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A X)) (Mon.Hom.hom { hom := A.map (𝟙 X), isMonHom_hom := sorry })
  (Mon.Hom.hom (𝟙 (functorObjObj A X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
⊢ Eq (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A X))
    (Mon.Hom.hom { hom := A.map (𝟙 X), isMonHom_hom := ⋯ }) (Mon.Hom.hom (𝟙 (functorObjObj A X)))
have w : A.map (𝟙 X) = 𝟙 (A.obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)
have w : Eq.{v₂ + 1} (α := A.obj X ⟶ A.obj X) (𝟙 (A.obj X)) (𝟙 (A.obj X))
Tactic: rw [CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := Quiver.Hom (V := Mon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A Z))
    { hom := A.map (f ≫ g), isMonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := ⋯ }
      { hom := A.map g, isMonHom_hom := ⋯ })
have w : Eq.{v₂ + 1} (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A Z))
  (Mon.Hom.hom { hom := A.map (f ≫ g), isMonHom_hom := sorry })
  (Mon.Hom.hom
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := sorry }
      { hom := A.map g, isMonHom_hom := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A Z))
    (Mon.Hom.hom { hom := A.map (f ≫ g), isMonHom_hom := ⋯ })
    (Mon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := ⋯ }
        { hom := A.map g, isMonHom_hom := ⋯ }))
have w : A.map (f ≫ g) = A.map f ≫ A.map g
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ A.map (f ≫ g) = A.map f ≫ A.map g
have w : A.map f ≫ A.map g = A.map f ≫ A.map g
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := Comon.X (functorObjObj A X) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) (A.map f ≫ ε) ε
have dsimp : Eq (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
  (A.map f ≫ NatTrans.app ε Y : A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
  (NatTrans.app ε X :
    A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
Tactic: dsimp