Defining a finset with two elements {x,y}

Stream: new members

[Sebastian Monnet]

Given terms x y : X, I would like to define the set {x, y} as a finset. Here is a mwe for a way that doesn't work and a way that works:

import field_theory.galois


example (X : Type*) (x y : X) : X :=
begin
  let S := ({x, y} : finset X),
end

example (X : Type*) (x y : X) (hxy : x ≠ y): X :=
begin
  let S := finset.cons x ({y} : finset X) (finset.not_mem_singleton.mpr hxy),
end

I'm pretty sure the first method worked in a previous version of mathlib, and it had the advantage of not requiring x and y to be distinct (I assume it just made the set a singleton if they were equal). Is there a way to do something equivalent to the first method in current mathlib?

[Yaël Dillies]

You're missing a [decidable_eq X] assumption in the first case.

[Sebastian Monnet]

Yaël Dillies said:

You're missing a [decidable_eq X] assumption in the first case.

Thank you!