no goals
C : Type u_2
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Preadditive D
F G : C ⥤ D
ι : Type u_1
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ (∑ i in s, α i).app X = ∑ i in s, (α i).app X
simp only [← appHom_apply, map_sum]