no goals
ι : Type u_2
α : Type ?u.93086
β : Type ?u.93089
M : Type ?u.93092
N : Type ?u.93095
G✝ : Type ?u.93098
k : Type ?u.93101
R : Type ?u.93104
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ abs (∑ i in s, f i) = ∑ i in s, f i
rw [abs_of_nonneg (Finset.sum_nonneg hf)]