Extracting variables from an existential quantifier (∃)

Stream: new members

[Kajani Kaunda]

Hello,

Learning Lean is as fun as a Pirates of the Caribbean or Lord of the Rings Quest!

How do extract the variables pa, x, y and k defined in the Theorem infinitely_many_y_exist_for_primes so that I can then use them later in the code? I guess I could use obtain, but I don't know how.

Probably, something like:
obtain ⟨x, y, k, hkpos, hk, hx_lt, hcases⟩ := sorry

But what do I replace the sorry with?

import Mathlib
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Topology.Algebra.FilterBasis
import Mathlib.Order.Filter.Basic
import Mathlib.Tactic
-- ------------------------------------------------------
theorem prime_form_6n_plus_1_or_6n_minus_1 (p : ℕ) (hprime : Nat.Prime p) (hp : 3 < p) :
    ∃ n, (p = 6 * n + 1 ∨ p = 6 * n - 1) := by
  suffices p % 6 = 1 ∨ p % 6 = 5 by
    obtain hp | hp := this
    · use p / 6
      left
      omega
    · use (p / 6 + 1)
      right
      omega
  have : p % 6 < 6 := Nat.mod_lt _ (by norm_num)
  have : p ≠ 2 := by linarith
  have : p ≠ 3 := by linarith
  have : p ≠ 6 := by rintro rfl; norm_num at hprime
  interval_cases hr : p % 6 <;> first | omega | (exfalso; revert hr)
  · rw [← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 2) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 3) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 2) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop

 -- -----------------------------------------------------

theorem infinitely_many_y_exist_for_primes'
  (pa : ℕ) (hp : pa > 3) (hprime : Nat.Prime pa) :
  ∃ᶠ (y : ℕ) in atTop,
    (∃ (x k : ℤ),
      (k > 0) ∧
      (k = x + y) ∧
      (x < x + y) ∧
      (
        (pa = (6 * x + 6 * y + 1) ∧
         Nat.Prime (6 * y + 1) ∧
         Nat.Prime ((6 * x + 6 * y + 1).toNat + (6 * y + 1) - 3)
        )
        ∨
        (pa = (6 * x + 6 * y - 1) ∧
         Nat.Prime (6 * y - 1) ∧
         Nat.Prime ((6 * x + 6 * y - 1).toNat + (6 * y - 1) - 3)
        )
      )
    ) := by

  obtain ⟨n, h⟩ := prime_form_6n_plus_1_or_6n_minus_1 pa hprime hp
  rcases h with rfl | rfl
  · -- Case 1: pa = 6n + 1
    sorry
  · -- Case 2: pa = 6n - 1
    sorry

[Eric Paul]

It seems like the x, y, and k are in the goal of your theorem. In other words, it is your job to show that they exist and so you can’t just access them as they don’t exist yet.

[Kajani Kaunda]

Eric Paul said:

It seems like the x, y, and k are in the goal of your theorem. In other words, it is your job to show that they exist and so you can’t just access them as they don’t exist yet.

Okay, noted.

[Kajani Kaunda]

So essentially, I should just get on with constructing them, yes?

[Igor Khavkine]

I'm not sure how much it would apply to your use case, but have a look at this earlier thread where I brought up a similar question. Have a look at my "working solution" based on docs#Exists.imp.