Handling Conditional Cases & Prime Representations

Stream: new members

[Kajani Kaunda]

Hello,
I already have a lemma that proves that all primes > 3 can be expressed in the form

(6 * y + 1) or
(6 * y - 1).

Let's call this lemma form_6 for simplicity.

1. In theorem infinitely_many_y_exist_for_primes below,  I want a statement that says:

   if p is in the form (6 * x + 6 * y - 1)
   then do abc
   else if p is in the form (6 * x + 6 * y + 1)
   then do xyz

where y and x are the same y and x defined in the lines:
∃ᶠ (y : ℕ) in Filter.atTop, and
(∃ (x : ℤ),
   respectively.
How do I code that?
I don't want to muddy the waters by posting what I have tried!

Remark: Since p is essentially fixed and we are setting p = 6x + 6y ± 1 and y > 0 by virtue of using the  code ∃ᶠ (y : ℕ) in Filter.atTop,, then x + y has a fixed value  and x must necessarily decrease as y gets larger. But x can start off with a positive value that is why I have defined it as type ℤ.

import Mathlib

theorem infinitely_many_y_exist_for_primes
  (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) :
  ∃ᶠ (y : ℕ) in Filter.atTop,
     (∃ (x : ℤ),
        ((p = (6 * x + 6 * y + 1) ∧
          Nat.Prime (6 * y + 1) ∧
          Nat.Prime ((6 * x + 6 * y + 1).toNat + (6 * y + 1) - 3))
          ∨
         (p = (6 * x + 6 * y - 1) ∧
          Nat.Prime (6 * y - 1) ∧
          Nat.Prime ((6 * x + 6 * y - 1).toNat + (6 * y - 1) - 3)))) :=
  by
-- code goes here ...
  sorry

[Kevin Buzzard]

if p % 6 = 5 then ... else ... maybe?

[Kajani Kaunda]

Kevin Buzzard said:

if p % 6 = 5 then ... else ... maybe?

Oh, Thank you very much. Will try that out.

[Kajani Kaunda]

I suppose I can then work with the equations 6x + 6y - 1 and 6x + 6y + 1 in their respective if blocks and Lean will be happy ...!