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