# Zulip Chat Archive

## 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