∀ {α : Type u_1} {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α), g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)