-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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 : Fintype J
f : J → C
X : C
w :
  ∀ (j : 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)
      (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)
          (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ≫ 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} (α :=
    (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)
    (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)
    (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ≫ biproduct.ι 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) (biproduct.{0, v_1, u_1} f) X)
have w₁ : ∀ (j : 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)
        (biproduct.desc fun (j : J) ↦ 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)
    (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)
        (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ≫ 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
  ext
  dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
  simp only [biproduct.ι_desc, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]