Finset.prod s id

Stream: Is there code for X?

[Arend Mellendijk]

Are there lemmas to this effect? I find rw sometimes has trouble dealing with these expressions because it doesn't unify fun n => n and id

import Mathlib.Data.Finset

theorem prod_id [CommMonoid R] (s : Finset R) : ∏ n in s, n = s.prod id := rfl
theorem sum_id [AddCommMonoid R] (s : Finset R) : ∑ n in s, n = s.sum id := rfl

[Eric Wieser]

Does unfold id work in the place that you want this?

[Arend Mellendijk]

No, because ∏ n in s, n appears in the goal and I'm rewriting using docs#Finset.prod_val

[Arend Mellendijk]

That said perhaps this is a code smell and I should just refactor this proof

[Arend Mellendijk]

Actually it appears erw deals with it in this case