no goals
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ ∀ (j : J),
    ι f j ≫ toSubtype f p =
      ι f j ≫ desc fun j => if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0
simp