In a set

Stream: new members

[Martin Dvořák]

I have a problem. When I was transforming it to MWE, a weird has_mem instance appeared, but here we are.

example (S : set ℕ) (n : ℕ) [has_mem ℕ (ℕ → Prop)]
  (h : n ∈ (λ (x : ℕ), x ∈ S)) :
    n ∈ S :=
begin
  sorry,
end

[Kevin Buzzard]

[has_mem ℕ (ℕ → Prop)] means "let's decree that n \in (\lam x, x \in S) makes sense whilst attaching no meaning at all to it" so h is useless to you.

[Martin Dvořák]

Lemme make a less minimal example instead. Thanks for this observation!