no goals
ι : Type ?u.409694
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
⊢ (∏ i in s, if i ∈ t then f i else 1) = ∏ i in s ∩ t, f i
rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]