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

1. 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?
2. 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):

1. pp has type Nat.Prime p so pp.not_dvd_one means Nat.Prime.not_dvd_one pp.
2. 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