no goals
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j : J, g j ≫ h j
simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
  dite_comp]