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
X : C
f : J → C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (X ◁ biproduct.ι f j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (Iso.hom (leftDistributor X f) :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.hom (leftDistributor X f) :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

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
X : C
f : J → C
j : J
val : Fintype J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.hom (leftDistributor X f) :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

Tactic:
simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc,
    biproduct.ι_π, whiskerLeft_dite, dite_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_dite, CategoryTheory.leftDistributor_hom, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Limits.biproduct.ι_π
-- 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
X : C
f : J → C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (X ◁ biproduct.ι f j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (Iso.hom (leftDistributor X f) :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.hom (leftDistributor X f) :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

Tactic:
classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc,
    biproduct.ι_π, whiskerLeft_dite, dite_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_dite, CategoryTheory.leftDistributor_hom, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, nonempty_fintype, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Limits.biproduct.ι_π
-- 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
X : C
f : J → 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) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (Iso.inv (leftDistributor X f) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (X ◁ biproduct.π f j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
⊢ Eq.{v_1 + 1} (α :=
    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.π f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

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
X : C
f : J → 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) X (f j)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.π f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

Tactic:
simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp,
    biproduct.ι_π, whiskerLeft_dite, comp_dite]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_dite, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.leftDistributor_inv, 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
X : C
f : J → 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) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (Iso.inv (leftDistributor X f) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
          (X ◁ biproduct.π f j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
⊢ Eq.{v_1 + 1} (α :=
    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.π f j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))

Tactic:
classical
  cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp,
    biproduct.ι_π, whiskerLeft_dite, comp_dite]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_dite, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Preadditive.sum_comp, nonempty_fintype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.leftDistributor_inv, 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
X : C
f : J → C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
      (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
          (Iso.inv (leftDistributor X f) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
      (X ◁ biproduct.ι f j :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (X ◁ biproduct.ι f j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))

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
X : C
f : J → C
j : J
val : Fintype J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (X ◁ biproduct.ι f j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))

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

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.leftDistributor_inv
-- 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
X : C
f : J → C
j : J
intro :
  ∀ (val : Fintype J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
      (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
          (Iso.inv (leftDistributor X f) :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
      (X ◁ biproduct.ι f j :
        tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (Iso.inv (leftDistributor X f) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (X ◁ biproduct.ι f j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))

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

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, nonempty_fintype, CategoryTheory.leftDistributor_inv
-- 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
X Y : C
f : J → C
val : Fintype J
j : J
intro :
  Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
    (if Membership.mem (γ := Finset J) Finset.univ j then
      ∑ x : J,
        (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ biproduct.π f x) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v_1, u_1} (𝒞 := inst) X
              (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
            (𝟙 X ⊗ₘ biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) x)
            (𝟙 X ⊗ₘ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j)
    else 0)
    (if Membership.mem (γ := Finset J) Finset.univ j then
      Iso.inv (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫
        (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) ⊗ₘ biproduct.π f j) ≫ Iso.hom (α_ X Y (f j))
    else 0)
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
    (if Membership.mem (γ := Finset J) Finset.univ j then
      ∑ x : J,
        (𝟙 X ⊗ₘ Y ◁ biproduct.π f x) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v_1, u_1} (𝒞 := inst) X
              (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
            (𝟙 X ⊗ₘ biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) x)
            (X ◁ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j)
    else 0)
    (if Membership.mem (γ := Finset J) Finset.univ j then
      Iso.inv (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫
        tensorObj.{v_1, u_1} (𝒞 := inst) X Y ◁ biproduct.π f j ≫ Iso.hom (α_ X Y (f j))
    else 0)

Tactic:
simp_rw [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- 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
X Y : C
f : J → C
val : Fintype J
j : J
intro :
  Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
    (if Membership.mem (γ := Finset J) Finset.univ j then
      ∑ x : J, 𝟙 X ⊗ₘ (𝟙 Y ⊗ₘ biproduct.π f x) ≫ if h : x = j then eqToHom ⋯ else 0
    else 0)
    (if Membership.mem (γ := Finset J) Finset.univ j then
      Iso.inv (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫
        (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) ⊗ₘ biproduct.π f j) ≫ Iso.hom (α_ X Y (f j))
    else 0)
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
    (if Membership.mem (γ := Finset J) Finset.univ j then
      ∑ x : J,
        (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ biproduct.π f x) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v_1, u_1} (𝒞 := inst) X
              (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)))
            (𝟙 X ⊗ₘ biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) x)
            (𝟙 X ⊗ₘ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j)
    else 0)
    (if Membership.mem (γ := Finset J) Finset.univ j then
      Iso.inv (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫
        (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) ⊗ₘ biproduct.π f j) ≫ Iso.hom (α_ X Y (f j))
    else 0)

Tactic:
simp only [← id_tensor_comp, biproduct.ι_π]

Premises used: CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.MonoidalCategory.id_tensor_comp