Iff implies Finset.prod eq

Stream: Is there code for X?

[Edison Xie]

Should we (if not already) have this in mathlib?

open scoped Classical in
@[to_additive]
lemma Finset.prod_filter_eq_of_iff {ι M : Type*} [CommMonoid M] {s : Finset ι}
    {p q : ι → Prop} (h : ∀ x ∈ s, p x ↔ q x) (f : ι → M) :
    ∏ i ∈ s with p i, f i = ∏ i ∈ s with q i, f i :=
  Finset.prod_congr (by ext; simp_all) fun _ _ ↦ rfl

[Miyahara Kō]

This lemma is not yet in mathlib but I think Finset.filter_congr is sufficient.

[Eric Wieser]

This is the downside of having notation which hides composition

[Yaël Dillies]

I agree, but the upside is too great