case h
α : Type u_1
β : Type ?u.196353
ι : Type ?u.196356
G : Type ?u.196359
M : Type u_2
N : Type ?u.196365
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : Set.Finite (mulSupport f)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔
    x ∈ ↑(Finset.filter (fun x => x ∈ s) (Finite.toFinset hf)) ∩ mulSupport fun i => f i
α : Type u_1
β : Type ?u.196353
ι : Type ?u.196356
G : Type ?u.196359
M : Type u_2
N : Type ?u.196365
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : Set.Finite (mulSupport f)
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finset.filter (fun x => x ∈ s) (Finite.toFinset hf)) ∩ mulSupport fun i => f i
ext x
no goals
case h
α : Type u_1
β : Type ?u.196353
ι : Type ?u.196356
G : Type ?u.196359
M : Type u_2
N : Type ?u.196365
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : Set.Finite (mulSupport f)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔
    x ∈ ↑(Finset.filter (fun x => x ∈ s) (Finite.toFinset hf)) ∩ mulSupport fun i => f i
simp [and_comm]