case w
C : Type u
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
J : Type
inst✝³ : Fintype J
f✝ : J → C
inst✝² : HasBiproduct f✝
K : Type
inst✝¹ : Fintype K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
j✝ : J
⊢ ι (fun j => f j) j✝ ≫ matrix m ≫ desc x = ι (fun j => f j) j✝ ≫ desc fun j => ∑ k : K, m j k ≫ x k
C : Type u
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
J : Type
inst✝³ : Fintype J
f✝ : J → C
inst✝² : HasBiproduct f✝
K : Type
inst✝¹ : Fintype K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
⊢ matrix m ≫ desc x = desc fun j => ∑ k : K, m j k ≫ x k
ext
no goals
case w
C : Type u
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
J : Type
inst✝³ : Fintype J
f✝ : J → C
inst✝² : HasBiproduct f✝
K : Type
inst✝¹ : Fintype K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
j✝ : J
⊢ ι (fun j => f j) j✝ ≫ matrix m ≫ desc x = ι (fun j => f j) j✝ ≫ desc fun j => ∑ k : K, m j k ≫ x k
simp