no goals
α : Type u_1
β : Type ?u.1844
γ : Type ?u.1847
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i : ι, if i ∈ s then f i else 1) = ∏ i in s, f i
rw [← prod_filter, filter_mem_eq_inter, univ_inter]