Friday afternoon fun: guess the goals

Stream: general

[Kevin Buzzard]

import tactic

example (a b : ℕ) : false :=
begin
  have hab : {a} ∪ {b} = {a, b},
  { library_search },
  all_goals {sorry}
end

Compiles fine. As Mario once said -- be the elaborator. What do you the the goals closed by sorry are? Again this was something that came up at Xena last night (whilst trying to do an integral!)

[Johan Commelin]

false and decidable_eq nat?

[Kevin Buzzard]

You forgot has_singleton ℕ unit (and several others)

[Floris van Doorn]

I'm not even sure if Lean can figure out the have is talking about set nat. So I'm guessing something like ?m and has_singleton nat ?m

[Floris van Doorn]

or maybe has_singleton nat (set ?m)

[Kevin Buzzard]

Here I'll give you an easier one:

import tactic
import data.complex.basic

example (a b : ℕ) : false :=
begin
  have hab : {a} ∪ {b} = {a, b},
    apply complex.ext,
  all_goals {sorry}
end