no goals
J : Type
inst✝⁴ : Fintype J
K : Type
inst✝³ : Fintype K
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
k : K
⊢ components (matrix m) j k = m j k
simp [biproduct.components]