∀ {M : Type u_1} {N : Type u_2} {γ : Type u_3} [inst : AddCommMonoid N] [inst_1 : DistribSMul M N] {r : M} {f : γ → N}
  {s : Set γ}, s.Finite → r • ∑ᶠ (x : γ) (_ : x ∈ s), f x = ∑ᶠ (x : γ) (_ : x ∈ s), r • f x