LeanPool.RlTheoryInLean.Order.Filter.Basic

theorem Filter.EventuallyEq.finset_sum {α : Type u_1} {ι : Type u_2} {β : Type u_3} [AddCommGroup β] {l : Filter α} {s : Finset ι} {f g : ι → α → β} (hfg : ∀ i ∈ s, f i =ᶠ[l] g i) : ∑ i ∈ s, f i =ᶠ[l] ∑ i ∈ s, g i