How to fix this?

Stream: new members

[Lewis]

(deleted)

[Lewis]

(deleted)

[Lewis]

How to fix this?

All Messages (3)
f.lean:14:12

Kim Morrison said:

f.lean:27:2
invalid 'end', insufficient scopes
f.lean:27:5
unexpected token ','; expected command

For the lean 4 code:

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Factorial.Basic

open Nat

theorem infinite_primes (n : ℕ) : ∃ p : ℕ, p ≥ n ∧ Prime p :=
let m := factorial n
let p := minFac (m + 1)
⟨p, ⟨
-- Prove p ≥ n
begin
intro hp,
push_neg at hp,
-- Since p < n, p should divide factorial of n
have h1 : p ∣ m := dvd_factorial (minFac_pos (m + 1)) (le_of_lt hp),
-- p also divides (m + 1)
have h2 : p ∣ (m + 1) := minFac_dvd (m + 1),
-- Thus, p divides the difference, which is 1
have h3 : p ∣ 1 := nat_dvd_sub h2 h1,
-- p cannot be greater than 1
have h4 : p ≤ 1 := le_of_dvd (by decide) h3,
-- But prime p must be at least 2
have h5 : 2 ≤ p := Prime.two_le (minFac_prime (m + 1)),
-- Contradiction arises
linarith
end,
-- Prove p is prime
minFac_prime (m + 1)
⟩⟩

Thanks a lot!

[Kim Morrison]

#backticks

[Notification Bot]

2 messages were moved here from #maths > How to fix this? by Kim Morrison.

[Kim Morrison]

(Please don't double post.)

[Notification Bot]

A message was moved here from #mathlib4 > How to fix this? by Kim Morrison.

[Kim Morrison]

Err.. triple post. Really, please do not ever do this again, okay?

[Lewis]

Deleted; How to fix the errors? Thanks.

[Eric Wieser]

Please read #backticks and edit your post above

[Richard Copley]

begin, end and the commas at the ends of lines are all Lean 3 Syntax. You can read the first chapters of one or both of the Lean 4 books #tpil or #mil to get introduced to the Lean 4 syntax.

Here is a version of your proof in Lean 4 syntax with the errors corrected. If you still have questions, please ask.

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Factorial.Basic

open Nat

theorem infinite_primes (n : ℕ) : ∃ p : ℕ, p ≥ n ∧ p.Prime :=
  let m := factorial n
  let p := minFac (m + 1)
  have h00 : 1 ≤ m := Nat.one_le_of_lt (Nat.factorial_pos n)
  have h01 : m + 1 ≠ 1 := by linarith
  ⟨p,
    by
      -- Prove p ≥ n
      rw [ge_iff_le, ← not_lt]
      intro hp
      -- Since p < n, p should divide factorial of n
      have h1 : p ∣ m := dvd_factorial (minFac_pos (m + 1)) (le_of_lt hp)
      -- p also divides (m + 1)
      have h2 : p ∣ (m + 1) := minFac_dvd (m + 1)
      -- Thus, p divides the difference, which is 1
      have h3 : p ∣ 1 := Nat.add_sub_cancel_left m 1 ▸ Nat.dvd_sub (Nat.le_add_right ..) h2 h1
      -- p cannot be greater than 1
      have h4 : p ≤ 1 := le_of_dvd (by decide) h3
      -- But prime p must be at least 2
      have h5 : 2 ≤ p := Prime.two_le (minFac_prime h01)
      -- Contradiction arises
      linarith,
    -- Prove p is prime
    minFac_prime h01⟩