Help prove a Lemma in Lean 4

Stream: lean4

[Kajani Kaunda]

Hello,

I need help proving the following Lemma. The lemma tries to prove that every prime > 3 is not divisible by 2. An elementally task for a seasoned Leaner!

lemma theo1 (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) : ¬ (2 ∣ p) := by

[Ruben Van de Velde]

First step:

import Mathlib
lemma theo1 (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) : ¬ (2 ∣ p) := by
  -- rw? finds:
  rw [propext (Nat.dvd_prime hprime)]

(Not sure why it puts propext in there)

[Kajani Kaunda]

Ruben Van de Velde said:

First step:

import Mathlib
lemma theo1 (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) : ¬ (2 ∣ p) := by
  -- rw? finds:
  rw [propext (Nat.dvd_prime hprime)]

(Not sure why it puts propext in there)

Looks like some kind of transformation ...

[Ruben Van de Velde]

No, I know what it does, but I don't know why rw? suggests it

[Kajani Kaunda]

Ruben Van de Velde said:

First step:

import Mathlib
lemma theo1 (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) : ¬ (2 ∣ p) := by
  -- rw? finds:
  rw [propext (Nat.dvd_prime hprime)]

(Not sure why it puts propext in there)

Thank you very much for the code. I am working on a certain known result about primes. Proof that all primes > 3 can be expressed in the form 6n - 1 or 6n + 1.

[Kajani Kaunda]

So this result was the first step. I am new to lean so I have kind of dived into the deep end ...

[Kajani Kaunda]

:smile:

[Kim Morrison]

Ruben Van de Velde said:

No, I know what it does, but I don't know why rw? suggests it

Good question. @Ruben Van de Velde, do you want to open an issue for that? We should try to fix it at some point (it shouldn't be hard, PR welcome :-).

[Ruben Van de Velde]

https://github.com/leanprover/lean4/issues/5082