finset.sum eq sum over support

Stream: Is there code for X?

[Daniel Packer]

Are there lemmas that look like this in mathlib?

lemma finset.sum_eq_sum_support {σ G : Type*} [fintype σ] [add_comm_monoid G] (f : σ →₀ G) :
  finset.univ.sum f = f.support.sum f :=
begin
  have : ∑ i : σ in (f.supportᶜ), f i = 0,
  {
    apply finset.sum_eq_zero,
    intros i h,
    rw [← finsupp.not_mem_support_iff, ← finset.mem_compl],
    exact h,
  },
  rw [← finset.sum_compl_add_sum f.support, this, zero_add],
end

or the slightly different:

lemma finset.prod_supp_pow_eq_prod_pow {σ G : Type*} [fintype σ] [comm_monoid G] (f : σ → G) (g : σ →₀ ℕ) :
  ∏ (i : σ) in g.support, f i ^ g i = ∏ (i : σ), f i ^ g i :=
begin
  have : ∏ (i : σ) in g.supportᶜ, f i ^ g i = 1,
  {
    apply finset.prod_eq_one,
    intros i h,
    rw [finset.mem_compl, finsupp.not_mem_support_iff] at h,
    rw [h, pow_zero],
  },
  rw [← finset.prod_compl_mul_prod g.support, this, one_mul],
end

I'm getting these sorts of things when proving facts about multivariable polynomials.

[Yaël Dillies]

f.support.sum f is f.sum (λ _, id).

[Kyle Miller]

Maybe Yael is indirectly suggesting this:

lemma finset.sum_eq_sum_support {σ G : Type*} [fintype σ] [add_comm_monoid G] (f : σ →₀ G) :
  finset.univ.sum f = f.sum (λ _, id) :=
(finsupp.sum_fintype f (λ _, id) (λ _, rfl)).symm

That λ _, id can also be λ i x, x, which is perhaps more readable.

Or if you do want it in the f.support.sum f form, since it's definitionally equal,

lemma finset.sum_eq_sum_support {σ G : Type*} [fintype σ] [add_comm_monoid G] (f : σ →₀ G) :
  finset.univ.sum f = f.support.sum f :=
(finsupp.sum_fintype f (λ _, id) (λ _, rfl)).symm