∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, m.WF → (k ∈ Std.HashSet.Raw.filter f m) = ∃ (h' : k ∈ m), f (m.get k h') = true