case w
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
j : J
⊢ ι (fun b => f b) j ≫ desc g = ι (fun b => f b) j ≫ ∑ j : J, π f j ≫ g j
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
⊢ desc g = ∑ j : J, π f j ≫ g j
ext j
no goals
case w
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
j : J
⊢ ι (fun b => f b) j ≫ desc g = ι (fun b => f b) j ≫ ∑ j : J, π f j ≫ g j
simp [comp_sum, biproduct.ι_π_assoc, dite_comp]