How to define equality between sets?

Stream: new members

[An Qi Zhang]

Hello, I was wondering how does one define equality between sets? When I abbreviate a Set of a type, Lean doesn't synthesize decidable equality for this Set of a type. Is there something in particular that I need to do to define equality between sets?

Here's a MWE using Set of Nat:

import Mathlib

abbrev SetNat := Set Nat

def ex1 : SetNat := {0}
def ex2 : SetNat := {1}

instance SetNat.instDecidableEq (s₁ s₂ : SetNat) : Decidable (s₁ = s₂) := by
  unfold SetNat
  infer_instance -- dead end

#check ex1 = ex2
#eval ex1 = ex2 -- failed to synthesize Decidable (ex1 = ex2)
-----------------------------
abbrev ListNat := List Nat
def ex3 : ListNat := [0]
def ex4 : ListNat := [1]
#eval ex3 = ex4 -- works

[Bjørn Kjos-Hanssen]

Infinite sets of natural numbers don't have decidable equality I guess. There are infinitely many things to check. You can look into docs#Finset

[Kenny Lau]

@An Qi Zhang you're mixing up "defining equality" with "deciding equality". Equality has already been defined, which is why you could even write = in the first place.