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)
j : Subtype p
⊢ (fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j =
    𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j
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)
⊢ fromSubtype f p ≫ toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)
refine' biproduct.hom_ext _ _ fun j => _
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)
j : Subtype p
⊢ (fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j =
    𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j
rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]