no goals
C : Type u₁
inst✝⁶ : Category C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((mapBiproduct F f).hom ≫ desc fun j => F.map (g j)) = F.map (desc g)
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]