finset.sum

Stream: Is there code for X?

[Scott Morrison]

lemma foo {α : Type*} [comm_monoid α] {β : Type*} [fintype β] (s : set β) (f : β → α) (g : s → α)
  (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ (x : β), x ∉ s → f x = 1) :
  finset.univ.prod f = finset.univ.prod g := sorry

[Yaël Dillies]

docs#finset.sum_congr along with docs#finset.sum_subtype?

[Scott Morrison]

I don't see how that would use the essential w' hypothesis.

[Yaël Dillies]

Oh sorry you also need docs#finset.prod_subset

[Scott Morrison]

Ah, okay. This is gross, but suffices:

@[to_additive]
lemma finset.prod_congr_set
  {α : Type*} [comm_monoid α] {β : Type*} [fintype β] (s : set β) (f : β → α) (g : s → α)
  (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ (x : β), x ∉ s → f x = 1) :
  finset.univ.prod f = finset.univ.prod g :=
begin
  rw ←@finset.prod_subset _ _ s.to_finset finset.univ f _ (by simp),
  { rw finset.prod_subtype,
    { apply finset.prod_congr rfl,
      exact λ ⟨x, h⟩ _, w x h, },
    { simp, }, },
  { rintro x _ h, exact w' x (by simpa using h), },
end

If anyone wants to golf, rename, or give an opinion on whether this belongs with other finset.sum lemmas, please go ahead. :-)