Referencing "exists" hypothesis

Stream: new members

[Gareth Ma]

Hello. Currently I have the following definition:

def ordinary_line (s : finset P) {p1 p2 : P} (h1 : p1 ∈ s) (h2 : p2 ∈ s) :=
∀ p ∈ s, p = p1 ∨ p = p2 ∨ p ∉ line[k, p1, p2]

And I would like to state the Sylvester-Gallai theorem, which says that for a non-collinear set of points, there exists an ordinary line. So I tried the following:

theorem sylvester_gallai {s : finset Pt} (h : ¬(collinear ℝ (s : set Pt))):
∃ p1 p2 ∈ s, ordinary_line s _ _ :=

However, Lean of course is unable to fill it in. Surprisingly, I got the following stupid-looking method working:

theorem sylvester_gallai {s : finset Pt} (h : ¬(collinear ℝ (s : set Pt))):
∃ p1 p2 ∈ s, ordinary_line s (show p1 ∈ s, by simp [*] at *) (show p2 ∈ s, by simp [*] at *) :=

Another alternative would be

∃ p1 p2 ∈ s, ordinary_line s (show p1 ∈ s, by { clear H, exact H }) H:=

So my question is, what is the correct way to write this? That is, how do I name the local hypothesis from p1 \in s?

[Yaël Dillies]

You can give it a name by doing \exists p1 (hp1 : p1 \in s) p2 (hp2 : p2 \in s), .... But in that case I wouldn't even take the membership hypotheses in ordinary_line, but the points directly.

[Gareth Ma]

Wll the change be "correct" with mathlib style? It seems that a lot of lemmas and stuff takes just the requirements and deduces the remaining variables

[Yaël Dillies]

What change? Taking the points directly would certainly be more mathlib style.

[Gareth Ma]

Yea I mean the taking the points change. I was thinking about stuff like nat.prime_pos, where it only takes a hypothesis hp : nat.prime p instead of say nat.prime_pos p hp.

[Eric Wieser]

That's not the same situation; ordinary_line is a def, prime_pos is a lemma