Need help with Multiset.filter

Stream: new members

[Kevin Cheung]

I have the following

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Powerset

structure foo (α : Type*) where
  V : Finset α
  E : Multiset { x // x ⊆ V }
  double_cover : ∀ x ∈ V, (E.filter (fun e ↦ x ∈ e.val)).sizeOf ≥ 2

and I am getting the error:

failed to synthesize instance
  DecidablePred fun e ↦ x ∈ ↑e

Replacing x ∈ e.val with something trivial like 1 = 1 does not lead to the error. So I guess the former is not decidable? But it seems easy enough that there must be a way to do this and this is where I am stuck. Any help greatly appreciated.

[Ruben Van de Velde]

Probably easiest is

structure foo (α : Type*) [DecidableEq α] where

because if you can check if elements are equal, you can check if an element is in a finite set

[Kevin Cheung]

Thank you. That worked!