no goals
α : Type u_1
β : Type ?u.195249
ι : Type ?u.195252
G : Type ?u.195255
M : Type u_2
N : Type ?u.195261
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hf : Set.Finite (s ∩ mulSupport f)
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finite.toFinset hf) ∩ mulSupport fun i => f i
simp [inter_assoc]