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) → T ⟶ f j
⊢ ∀ (j : J), lift g ≫ π (fun b => f b) j = (∑ j : J, g j ≫ ι f j) ≫ π (fun b => f b) 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) → T ⟶ f j
⊢ lift g = ∑ j : J, g j ≫ ι f j
apply biproduct.hom_ext
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) → T ⟶ f j
j : J
⊢ lift g ≫ π (fun b => f b) j = (∑ j : J, g j ≫ ι f j) ≫ π (fun b => f b) j
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) → T ⟶ f j
⊢ ∀ (j : J), lift g ≫ π (fun b => f b) j = (∑ j : J, g j ≫ ι f j) ≫ π (fun b => f b) j
intro 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) → T ⟶ f j
j : J
⊢ lift g ≫ π (fun b => f b) j = (∑ j : J, g j ≫ ι f j) ≫ π (fun b => f b) j
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]