## Stream: new members

### Topic: Referencing "exists" hypothesis

#### Gareth Ma (Feb 10 2023 at 11:44):

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 (Feb 10 2023 at 11:46):

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 (Feb 10 2023 at 11:48):

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 (Feb 10 2023 at 11:50):

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

#### Gareth Ma (Feb 10 2023 at 11:52):

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 (Feb 11 2023 at 00:30):

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

Last updated: Dec 20 2023 at 11:08 UTC