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

Tactic:
classical
  cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum,
    id_tensor_comp, tensorIso_hom, leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
    biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero]
  simp_rw [← id_tensorHom]
  simp only [← id_tensor_comp, biproduct.ι_π]
  simp only [id_tensor_comp, tensor_dite, comp_dite]
  simp

Premises used: CategoryTheory.Category.assoc, Finset.sum_dite_irrel, CategoryTheory.MonoidalCategory.id_tensorHom, 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, nonempty_fintype, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.asIso_hom, CategoryTheory.comp_dite, CategoryTheory.MonoidalCategory.tensor_dite, CategoryTheory.Limits.biproduct.ι_map, CategoryTheory.MonoidalCategory.id_tensor_comp