no goals
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq J
f : J → C
inst✝ : HasBiproduct f
j j' : J
⊢ ι f j ≫ π f j' = if h : j = j' then eqToHom (_ : f j = f j') else 0
convert (biproduct.bicone f).ι_π j j'