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

Tactic:
classical
  cases nonempty_fintype J
  ext
  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,
    comp_tensor_id, tensorIso_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]
  simp_rw [← tensorHom_id]
  simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
  simp

Premises used: Finset.mem_univ, CategoryTheory.Category.assoc, CategoryTheory.sum_tensor, Finset.sum_dite_irrel, if_true, 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.Preadditive.comp_sum, nonempty_fintype, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.dite_tensor, CategoryTheory.MonoidalCategory.comp_tensor_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.asIso_hom, CategoryTheory.rightDistributor_hom, CategoryTheory.comp_dite, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Limits.biproduct.ι_map