R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ (sum (single f r) fun f' s_1 => sum (single g s) fun g' t => single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ single f r ≫ single g s = single (f ≫ g) (r * s)
dsimp [CategoryTheory.categoryFree]
no goals
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ (sum (single f r) fun f' s_1 => sum (single g s) fun g' t => single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)
simp