∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {F : Type u_7}
  [inst_2 : EquivLike F M N] [AddEquivClass F M N] (g : F) (f : α → M), g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)