case w.w
J : Type
inst✝⁴ : Fintype J
K : Type
inst✝³ : Fintype K
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : J
j✝ : K
⊢ (ι (fun j => f j) j✝¹ ≫ matrix fun j k => components m j k) ≫ π (fun k => g k) j✝ =
    (ι (fun j => f j) j✝¹ ≫ m) ≫ π (fun k => g k) j✝
J : Type
inst✝⁴ : Fintype J
K : Type
inst✝³ : Fintype K
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
⊢ (matrix fun j k => components m j k) = m
ext
no goals
case w.w
J : Type
inst✝⁴ : Fintype J
K : Type
inst✝³ : Fintype K
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : J
j✝ : K
⊢ (ι (fun j => f j) j✝¹ ≫ matrix fun j k => components m j k) ≫ π (fun k => g k) j✝ =
    (ι (fun j => f j) j✝¹ ≫ m) ≫ π (fun k => g k) j✝
simp [biproduct.components]