Exists witness in a def

Stream: new members

[Cayden Codel]

I'm trying to code up and prove things about a more general function (think on a general type u rather than on nats), but my first pass seems to require that I use the witness of an exists hypothesis in the def, which Lean doesn't seem to like. Here's a MWE that produces the error.

lemma exists_not_mem (l : list nat) : ∃ (n : nat), n ∉ l := begin ... end

def cons_not_mem : list nat → list nat
| [] := [1]
| l := have exi : ∃ (n : nat), n ∉ l, from exists_not_mem l,
    exi.w :: l

In cons_not_mem, Lean complains that Exists.w is an unknown. Is there a way to use exi in the def? Or must I try a different route?

[Kevin Buzzard]

You need to use classical.some exi because constructively Exists only eliminates into Prop

[Kevin Buzzard]

And then classical.some_spec exi is the proof that n is not in l

[Cayden Codel]

Great, that's exactly what I needed. Thanks!