no goals
ι : Type u_2
α : Type ?u.95199
β : Type ?u.95202
M : Type ?u.95205
N : Type ?u.95208
G✝ : Type ?u.95211
k : Type ?u.95214
R : Type ?u.95217
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ abs (∑ i in s, f i) = ∑ i in s, f i
rw [abs_of_nonneg (Finset.sum_nonneg' hf)]