no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : Preadditive C
J : Type
inst✝² : Fintype J
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = fst ≫ f ≫ inl + snd ≫ g ≫ inr
apply biprod.hom_ext <;> apply biprod.hom_ext' <;> simp