I need help formalizing the following well-known result

Stream: new members

[Kajani Kaunda]

Hello,

I need help formalizing the following well-known result:

All prime numbers > 3 can be expressed in the forms 6n ± 1.

theorem lemma_4_2 (p : ℕ) (hp : Nat.Prime p) (h : p > 3) :
∃ (n : ℕ), p = 6 * n + 1 ∨ p = 6 * n - 1 := sorry

Thank you and I am grateful for your help.

[Martin Dvořák]

What goes wrong when you simply follow your proof from paper?

[Kajani Kaunda]

Martin Dvořák said:

What goes wrong when you simply follow your proof from paper?

Nice question! I am not (yet) good at Lean. Very bad. So I do not know how to code what I want to say. Result? errors, errors, errors!

[Kevin Buzzard]

First prove by a case analysis that p % 6 must be 1 or 5.

[Kajani Kaunda]

Kevin Buzzard said:

First prove by a case analysis that p % 6 must be 1 or 5.

Ok. Will try that approach. Thank you...

[Luigi Massacci]

Also, if you haven't already, you should start reading #mil

[Kajani Kaunda]

Luigi Massacci said:

Also, if you haven't already, you should start reading #mil

Thanks for that too! - was reading "How to prove it with Lan"

[A.]

Example 3.4.4 of MoP introduces the mod_cases tactic.

[Dan Velleman]

Note that How To Prove It with Lean uses some tactics that are not standard--they are defined in a package that accompanies the book. But it is not too hard to switch from those tactics to standard tactics--see the section "Transitioning to Standard Lean" in the appendix to How To Prove It with Lean.

[Kajani Kaunda]

Dan Velleman said:

Note that How To Prove It with Lean uses some tactics that are not standard--they are defined in a package that accompanies the book. But it is not too hard to switch from those tactics to standard tactics--see the section "Transitioning to Standard Lean" in the appendix to How To Prove It with Lean.

Ah!, noted with thanks.