Starting with Lean: exists.elim complication

Stream: new members

[Lucas Polymeris]

Hello everyone, I recently started working with Lean and I wanted to formalize some notions I've been working on
for the past Month. But I'm stuck with a step, which should be solved with exists.elim I think, but doesn't seem to work:
a MWE I can come up with would be something like this:

lemma xd {C : Type} {h: ∃ x : C, x = x}: ∃ (X : set C), X ≠ ∅ :=
begin
exists.elim h,
end

where the intention would be to prove it by constructing the a singleton set.
Shouldn't that tactic give x : C, and h: x = x ? Or what am I missing? Instead, when
I hover, I ger "don't know how yo synthesize placeholder".

Thanks and sorry for the noobie question.

[Johan Commelin]

@Lucas Polymeris Welcome. One way to deal with existentials is using the cases tactic. So you can write cases h with x hx, and this will decompose h into a witness x : C with property hx : x = x.

[Scott Morrison]

If you're using mathlib, you can also write obtain ⟨x, hx⟩ := h which is sometimes more readable than cases.

[Lucas Polymeris]

@Johan Commelin Oh, thanks. I think I didn't see that when reading about existential quantifier. Any hint on why doesn't
exists.elim work?

[Kyle Miller]

One thing is that exists.elim is not a tactic. Each statement in a begin ... end block needs to be a tactic -- Lean will be looking for tactic.interactive.exists.elim, which isn't what you want.

[Kyle Miller]

If you want to use exists.elim, this is one way to proceed:

lemma xd {C : Type} {h: ∃ x : C, x = x}: ∃ (X : set C), X ≠ ∅ :=
begin
  apply exists.elim h,
  intros x hx,

end

[Lucas Polymeris]

@Kyle Miller Oh I see, thanks. I wasn't aware of that.

[Mario Carneiro]

You can also write terms directly if you don't use a begin ... end block, i.e.:

lemma xd {C : Type} {h: ∃ x : C, x = x}: ∃ (X : set C), X ≠ ∅ :=
exists.elim h $ λ x hx, _

[Mario Carneiro]

which is what the tactics mentioned so far are doing under the hood