awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (biproduct.ι f j ▷ X :
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (Iso.hom (rightDistributor f X) :
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.ι f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.hom (rightDistributor f X) :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
val : Fintype J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.ι f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.hom (rightDistributor f X) :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π,
    dite_whiskerRight, dite_comp]

Premises used: CategoryTheory.MonoidalCategory.dite_whiskerRight, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.rightDistributor_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (biproduct.ι f j ▷ X :
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (Iso.hom (rightDistributor f X) :
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.ι f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.hom (rightDistributor f X) :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
classical
  cases nonempty_fintype J
  simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π,
    dite_whiskerRight, dite_comp]

Premises used: CategoryTheory.MonoidalCategory.dite_whiskerRight, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, nonempty_fintype, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.rightDistributor_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (Iso.inv (rightDistributor f X) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (biproduct.π f j ▷ X :
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
⊢ Eq.{v_1 + 1} (α :=
    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.π f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
val : Fintype J
⊢ Eq.{v_1 + 1} (α :=
    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.π f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_whiskerRight,
    biproduct.ι_π, dite_whiskerRight, comp_dite]

Premises used: CategoryTheory.MonoidalCategory.dite_whiskerRight, CategoryTheory.Preadditive.sum_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.rightDistributor_inv, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (Iso.inv (rightDistributor f X) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
          (biproduct.π f j ▷ X :
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
⊢ Eq.{v_1 + 1} (α :=
    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
        (biproduct.π f j ▷ X :
          tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)

Tactic:
classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_whiskerRight,
    biproduct.ι_π, dite_whiskerRight, comp_dite]

Premises used: CategoryTheory.MonoidalCategory.dite_whiskerRight, CategoryTheory.Preadditive.sum_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.rightDistributor_inv, nonempty_fintype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
      (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
          (Iso.inv (rightDistributor f X) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
      (biproduct.ι f j ▷ X :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
val : Fintype J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)

Tactic:
simp [rightDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc,
    dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.rightDistributor_inv, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X : C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
      (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
          (Iso.inv (rightDistributor f X) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
      (biproduct.ι f j ▷ X :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)

Tactic:
classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc,
    dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.rightDistributor_inv, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, nonempty_fintype
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
val : Fintype J
j : J
intro :
  ∑ x : J,
      ((biproduct.π f x ⊗ₘ 𝟙 X) ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ⊗ₘ 𝟙 Y) =
    Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) Y)
    (∑ x : J,
      (biproduct.π f x ▷ X ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ▷ Y))
    (Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (f j) X Y))

Tactic:
simp_rw [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
val : Fintype J
j : J
intro :
  (∑ x : J, if h : x = j then (biproduct.π f x ⊗ₘ 𝟙 X) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (biproduct.π f x ⊗ₘ 𝟙 X) ≫ 0 ⊗ₘ 𝟙 Y) =
    Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ₘ 𝟙 X) ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ⊗ₘ 𝟙 Y) =
    Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)

Tactic:
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]

Premises used: CategoryTheory.MonoidalCategory.dite_tensor, CategoryTheory.MonoidalCategory.comp_tensor_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
val : Fintype J
j : J
⊢ (∑ x : J, if h : x = j then (biproduct.π f x ⊗ₘ 𝟙 X) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (biproduct.π f x ⊗ₘ 𝟙 X) ≫ 0 ⊗ₘ 𝟙 Y) =
    Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)

Tactic:
simp