reasoning about empty set in lean

Stream: new members

[Marcus Klaas]

Hi y'all. Sorry to bother again. I'm having trouble working with the empty set. Specifically, I'd like to prove that a set is not empty whenever I can produce a concrete element of it:

example : { x | x = nat.succ nat.zero } ≠ ∅ := sorry

but so far, I haven't been successful. What can I do here?

[Rob Lewis]

set.ne_empty_of_mem will probably be helpful!

[Rob Lewis]

You'll have to import data.set.basic from mathlib.

[Marcus Klaas]

Thanks! I will try it.

[Kenny Lau]

no import needed :)

example : { x | x = nat.succ nat.zero } ≠ ∅ :=
λ H, (congr_fun H 1).mp rfl

[Kevin Buzzard]

...says the person with over 1 year's Lean experience ;-)

[Kevin Buzzard]

import data.set.basic

example : { x | x = nat.succ nat.zero } ≠ ∅ :=
begin
  rw set.ne_empty_iff_exists_mem,
  use 1,
  exact rfl, -- refl doesn't work!
end

[Kevin Buzzard]

refl is really bad at set membership.

[Kevin Buzzard]

example (a : ℕ) : a ∈ {x : ℕ | x = a} := by refl -- fails

[Reid Barton]

I wonder whether we could fool it into working somehow

[Marcus Klaas]

Hmmm I don't seem to have the mathlib tho.. can I install it using elan? I have found a way to do it ^^

[Reid Barton]

basically by adding what Kevin just wrote as a relfexivity lemma

[Kevin Buzzard]

@Marcus Klaas mathlib is great. It's not just for mathematicians. It has a bunch of useful tactics in, and a whole host of useful data structures. If you work with Lean projects (as I do -- all my files, even scratch files, are within a Lean project) then you can just make mathlib a dependency for that project and then leanpkg upgrade will download mathlib.