J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map p = p j ≫ ι g j
rw [biproduct.map_eq_map']
no goals
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j
apply
  Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone
  (Discrete.natTrans fun j => p j.as) (Discrete.mk j)