-- 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
Y : C
val : Fintype J
j : J
intro :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J,
      (X ◁ biproduct.π f 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) X (f j)) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ▷ Y))
    (∑ x : J,
      Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
        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) (f j) Y))
          (𝟙 X ⊗ₘ
            biproduct.π f x ▷ Y ≫
              biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) x)
          (X ◁ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j ≫ Iso.inv (α_ X (f j) Y)))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v_1, u_1} fun (j : J) ↦
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
        (Iso.hom
            (Iso.trans (Y :=
              tensorObj.{v_1, u_1} (𝒞 := inst)
                (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
              (leftDistributor X f ⊗ᵢ asIso (𝟙 Y) :
                tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
                  tensorObj.{v_1, u_1} (𝒞 := inst)
                    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
              (rightDistributor (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y :
                tensorObj.{v_1, u_1} (𝒞 := inst)
                    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y ≅
                  biproduct.{0, v_1, u_1} fun (j : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)) :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦
              tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦
              tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v_1, u_1} fun (j : J) ↦
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
        (Iso.hom
          (α_ X (biproduct.{0, v_1, u_1} f) Y ≪≫
            Iso.trans (Y :=
              tensorObj.{v_1, u_1} (𝒞 := inst) X
                (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
              (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y :
                tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) ≅
                  tensorObj.{v_1, u_1} (𝒞 := inst) X
                    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
              (Iso.trans (Y :=
                  biproduct.{0, v_1, u_1} fun (j : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                  (leftDistributor X fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y :
                    tensorObj.{v_1, u_1} (𝒞 := inst) X
                        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
                      biproduct.{0, v_1, u_1} fun (j : J) ↦
                        tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                  (biproduct.mapIso fun (x : J) ↦ Iso.symm (α_ X (f x) Y) :
                    Iso.{v_1, u_1} (C := C)
                      (biproduct.{0, v_1, u_1} fun (j : J) ↦
                        tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                      (biproduct.{0, v_1, u_1} fun (x : J) ↦
                        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)) :
                tensorObj.{v_1, u_1} (𝒞 := inst) X
                    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
                  biproduct.{0, v_1, u_1} fun (x : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)))
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) j) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)

Tactic:
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
    tensor_sum, comp_tensor_id, tensorIso_hom, leftDistributor_hom, rightDistributor_hom,
    biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel,
    Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]

Premises used: Finset.mem_univ, CategoryTheory.Category.assoc, CategoryTheory.sum_tensor, Finset.sum_dite_irrel, if_true, CategoryTheory.leftDistributor_hom, CategoryTheory.Limits.biproduct.mapIso_hom, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.symm_hom, CategoryTheory.Preadditive.sum_comp, CategoryTheory.eqToHom_refl, Finset.sum_dite_eq', CategoryTheory.Category.comp_id, Finset.sum_const_zero, CategoryTheory.tensor_sum, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.comp_tensor_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.asIso_hom, CategoryTheory.rightDistributor_hom, CategoryTheory.comp_dite, CategoryTheory.Limits.biproduct.ι_map