-- 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 : Finite J
X Y : C
f : J → C
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)))
have 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)
Tactic: 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]