# Zulip Chat Archive

## Stream: new members

### Topic: Euclid's proof from LftCM 2023 tutorial

#### Moti Ben-Ari (Nov 30 2023 at 12:20):

In the first tutorial the following proof of Euclid's theorem that there is an infinite number of primes is given:

```
theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
let p := minFac (Nat.factorial n + 1)
have f1 : factorial n + 1 ≠ 1 := Nat.ne_of_gt <| Nat.succ_lt_succ <| factorial_pos _
have pp : Nat.Prime p := minFac_prime f1
have np : n ≤ p :=
le_of_not_ge fun h =>
have h₁ : p ∣ factorial n := dvd_factorial (minFac_pos _) h
have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
pp.not_dvd_one h₂
exact ⟨p, np, pp⟩
```

I don't understand the line `le_of_not_ge fun h =>`

. It seems to be decomposing `¬ n≥p`

into `n≥p → False`

. How does `fun h =>`

do that? I don't think I've seen this syntax in MiL.

#### Eric Wieser (Nov 30 2023 at 12:28):

Moti Ben-Ari said:

It seems to be decomposing

`¬ n≥p`

into`n≥p → False`

.

That's because this is the definition of `¬`

(docs#Not)!

#### Moti Ben-Ari (Nov 30 2023 at 13:18):

Sorry for not being clear. I know the definition of negation, but the previous occurrences of `n≥p → False`

that I have seen have used `intro`

to make `n≥p`

into a hypothesis and `False`

into a goal. How does `fun h => do`

work in this situation? Would it be possible to use `intro`

instead?

#### Eric Wieser (Nov 30 2023 at 13:24):

A rough analogy is that in term-mode, `fun x => by foo`

is the same as `by intro x; foo`

#### Eric Wieser (Nov 30 2023 at 13:25):

Or alternatively, in tactic-mode `exact fun x => y`

is the same as `intro x; exact y`

#### Damiano Testa (Nov 30 2023 at 13:25):

In this case, this is essentially equivalent to what you see:

```
theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
let p := minFac (Nat.factorial n + 1)
have f1 : factorial n + 1 ≠ 1 := Nat.ne_of_gt <| Nat.succ_lt_succ <| factorial_pos _
have pp : Nat.Prime p := minFac_prime f1
have np : n ≤ p := by
apply le_of_not_ge
intro h
have h₁ : p ∣ factorial n := dvd_factorial (minFac_pos _) h
have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
exact pp.not_dvd_one h₂
exact ⟨p, np, pp⟩
```

#### Eric Wieser (Nov 30 2023 at 13:26):

What's relevant here is that everything after the `have np : n ≤ p :=`

is in term-mode not tactic mode, but I think MiL tries very hard to pretend that term-mode proofs don't exist (as they're harder to learn to write, and often less readable)

#### Moti Ben-Ari (Nov 30 2023 at 13:50):

Thanks! I am looking into Lean for teaching math and tactics really are easier than terms.

#### Damiano Testa (Nov 30 2023 at 13:56):

All the `have ... := ...`

s in the proof above can be converted to `have ... := by exact ...`

(I think, I did not test it).

#### Moti Ben-Ari (Dec 05 2023 at 14:59):

For the benefit of other newbees, I am trying to modify this program to use a minimal number of Lean constructs: tactics only, no anonymous, explicit applications of tactics and rewrites. This is as far as I can get:

```
import Mathlib.Data.Nat.Prime
open Nat
theorem Euclid_Thm (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
let p := minFac (factorial n + 1)
have f1 : factorial n + 1 ≠ 1 := by
apply Nat.ne_of_gt <| succ_lt_succ <| factorial_pos _
have pp : Nat.Prime p := by
apply minFac_prime f1
have np : n ≤ p := by
apply le_of_not_ge
intro h
have h₁ : p ∣ factorial n := by
apply dvd_factorial (minFac_pos _) h
have h₂ : p ∣ 1 := by
apply (Nat.dvd_add_iff_right h₁).mpr (minFac_dvd _)
apply pp.not_dvd_one
exact h₂
exact ⟨p, np, pp⟩
```

- Is
`pp.not_dvd_one`

an anonymous projection? If so I should be able to do something like`apply not_dvd_one pp`

but I get unknown identifier. How can I get rid of the projection or whatever it is? - I also want to get rid of the anonymous constructor in the last line.
`use p`

works, but I want to do this step-by-step. I tried`constructor`

to prove the two subformulas of the conjunction in the main goal separately using`np,pp`

but couldn't get it to work. Help would be appreciated.

#### Kevin Buzzard (Dec 05 2023 at 16:07):

`pp`

has type`Nat.Prime p`

so`pp.not_dvd_one`

means`Nat.Prime.not_dvd_one pp`

.- Replace
`exact ⟨p, np, pp⟩`

with`show_term exact ⟨p, np, pp⟩`

to see what the actual constructor used was. It's`Exists.intro`

.

#### Moti Ben-Ari (Dec 05 2023 at 17:42):

Thanks, Kevin. I searched the entire collection of Lean documentation and couldn't find any mention of the syntax`{ left = ... , right = ... }`

. But I found another way of doing it that should be easier to understand for newbees:

```
apply Exists.intro p
constructor
· exact np
· exact pp
```

#### Kevin Buzzard (Dec 05 2023 at 18:09):

`{ left = ... , right = ... }`

is just the default constructor for `And`

(it's a structure and those are the names of the fields). You could use `And.intro`

.

Last updated: Dec 20 2023 at 11:08 UTC