Problems / erdos-402 / erdos-402--h3-v2--h1--h1--h1--h2--h2

Window primes for 229 ≤ n ≤ 200014

erdos-402--h3-v2--h1--h1--h1--h2--h2

proved

Hole hs2 of erdos-402--h3-v2--h1--h1--h1--h2 (split by 20261001T170100Z-t1001-402a-partial.lean).

$\displaystyle \forall n \in \mathbb{N},\ 229 \le n \le 200014:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$

For every n from 229 to 200014 there is a prime p with n < p < 2n and 2(2n − p) ≤ n + 2 such that every α < n with p − n < α either has a prime q with n ≤ 3q dividing α(p − α), or satisfies n·x ≤ α·y for all x < y with x·y dividing α. All variables range over ℕ; the subtractions are in ℕ but p < 2n and α < n < p keep 2n − p and p − α ordinary.

unverified · history

Lean

theorem erdos_402__h3_v2__h1__h1__h1__h2__h2 : ∀ (n : ℕ),
  (229 : ℕ) ≤ n →
    n ≤ (200014 : ℕ) →
      ∃ (p : ℕ),
        Nat.Prime p ∧
          n < p ∧
            p < (2 : ℕ) * n ∧
              (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧
                ∀ α < n,
                  p < α + n →
                    (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                      ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000360, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000360.json, merge commit feeca055f8c6.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

lvl have ∀ (B Q : ℕ), (∀ q < B, (2 : ℕ) ≤ q → q.gcd Q ≠ (1 : ℕ)) → ∀ (p : ℕ), (1 : ℕ) < p → p < B * B → p.gcd Q = (1 : ℕ) → Nat.Prime p
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with lvl : ∀ (B Q : ℕ), (∀ q < B, (2 : ℕ) ≤ q → q.gcd Q ≠ (1 : ℕ)) → ∀ (p : ℕ), (1 : ℕ) < p → p < B * B → p.gcd Q = (1 : ℕ) → Nat.Prime p.
Uses library Nat.gcd, Nat.eq_one_of_dvd_one.
Lean, lines 21–31
```
 have lvl : ∀ B Q : ℕ, (∀ q : ℕ, q < B → 2 ≤ q → Nat.gcd q Q ≠ 1) →
 ∀ p : ℕ, 1 < p → p < B * B → Nat.gcd p Q = 1 → p.Prime := by
 intro B Q small p h1 h2 hg
 by_contra hnp
 have hq : p.minFac.Prime := Nat.minFac_prime (by omega)
 have hsq : p.minFac ^ 2 ≤ p := Nat.minFac_sq_le_self (by omega) hnp
 have hlt : p.minFac < B := by nlinarith
 apply small _ hlt hq.two_le
 have hd := Nat.gcd_dvd_gcd_of_dvd_left Q (Nat.minFac_dvd p)
 rw [hg] at hd
 exact Nat.eq_one_of_dvd_one hd
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 21–31 at feeca055f8c6 ↗
1. lvl.hq have Nat.Prime p.minFac
 Leaves False, with hq : Nat.Prime p.minFac.
 Uses library Nat.minFac_prime.
 Lean, line 25
 have hq : p.minFac.Prime := Nat.minFac_prime (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 25 at feeca055f8c6 ↗
2. lvl.hsq have p.minFac ^ (2 : ℕ) ≤ p
 Leaves False, with hsq : p.minFac ^ (2 : ℕ) ≤ p.
 Uses library Nat.minFac_sq_le_self.
 Lean, line 26
 have hsq : p.minFac ^ 2 ≤ p := Nat.minFac_sq_le_self (by omega) hnp
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 26 at feeca055f8c6 ↗
3. lvl.hlt have p.minFac < B routine: nlinarith
 Leaves False, with hlt : p.minFac < B.
 Lean, line 27
 have hlt : p.minFac < B := by nlinarith
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 27 at feeca055f8c6 ↗
4. lvl.hd have p.minFac.gcd Q ∣ p.gcd Q
 Leaves p.minFac.gcd Q = (1 : ℕ), with hd : p.minFac.gcd Q ∣ p.gcd Q.
 Uses library Nat.gcd_dvd_gcd_of_dvd_left, Nat.minFac_dvd.
 Lean, line 29
 have hd := Nat.gcd_dvd_gcd_of_dvd_left Q (Nat.minFac_dvd p)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 29 at feeca055f8c6 ↗
hP have ∀ (p : ℕ), (decide ((1 : ℕ) < p) && (decide (p < (49 : ℕ)) && decide (p.gcd (30 : ℕ) = (1 : ℕ)) || decide (p < (900 : ℕ)) && decide (p.gcd (6469693230 : ℕ) = (1 : ℕ)) || decide (p < (401956 : ℕ)) && decide (p.gcd (1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 : ℕ) = (1 : ℕ)))) = true → Nat.Prime p
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with hP : ∀ (p : ℕ), (decide ((1 : ℕ) < p) && (decide (p < (49 : ℕ)) && decide (p.gcd (30 : ℕ) = (1 : ℕ)) || decide (p < (900 : ℕ)) && decide (p.gcd (6469693230 : ℕ) = (1 : ℕ)) || decide (p < (401956 : ℕ)) && decide (p.gcd (1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 : ℕ) = (1 : ℕ)))) = true → Nat.Prime p.
Uses library Decidable.decide, Nat.gcd, Bool.true, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq.
Lean, lines 32–38
```
 have hP : ∀ p : ℕ, (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1))) = true → p.Prime := by
 intro p h
 simp only [Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] at h
 obtain ⟨h1, (⟨h2, h3⟩ | ⟨h2, h3⟩) | ⟨h2, h3⟩⟩ := h
 · exact lvl 7 30 (by decide +kernel) p h1 h2 h3
 · exact lvl 30 6469693230 (by decide +kernel) p h1 h2 h3
 · exact lvl 634 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 (by decide +kernel) p h1 h2 h3
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 32–38 at feeca055f8c6 ↗
1. hP.s1 obtain (1 : ℕ) < p ∧ ((p < (49 : ℕ) ∧ p.gcd (30 : ℕ) = (1 : ℕ) ∨ p < (900 : ℕ) ∧ p.gcd (6469693230 : ℕ) = (1 : ℕ)) ∨ p < (401956 : ℕ) ∧ p.gcd (1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 : ℕ) = (1 : ℕ))
 Leaves Nat.Prime p, with h1 : (1 : ℕ) < p, h2 : p < (49 : ℕ), h3 : p.gcd (30 : ℕ) = (1 : ℕ).
 Lean, line 35
 obtain ⟨h1, (⟨h2, h3⟩ | ⟨h2, h3⟩) | ⟨h2, h3⟩⟩ := h
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 35 at feeca055f8c6 ↗
2. hP.s2 case
 Leaves Nat.Prime p.
 Uses library Lean.Parser.Tactic.DecideConfig.kernel.
 Lean, line 36
 · exact lvl 7 30 (by decide +kernel) p h1 h2 h3
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 36 at feeca055f8c6 ↗
3. hP.s3 case
 Leaves Nat.Prime p.
 Uses library Lean.Parser.Tactic.DecideConfig.kernel.
 Lean, line 37
 · exact lvl 30 6469693230 (by decide +kernel) p h1 h2 h3
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 37 at feeca055f8c6 ↗
4. hP.s4 case
 Leaves Nat.Prime p.
 Uses library Lean.Parser.Tactic.DecideConfig.kernel.
 Lean, line 38
 · exact lvl 634 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 (by decide +kernel) p h1 h2 h3
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 38 at feeca055f8c6 ↗
key have ∀ (t : ℕ → Bool), (∀ (p : ℕ), t p = true → Nat.Prime p) → ∀ (b : ℕ) (L : List (ℕ × ℕ)) (a : ℕ), List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) => t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) L a = true → ∀ (n : ℕ), a ≤ n → n ≤ b → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with key : ∀ (t : ℕ → Bool), (∀ (p : ℕ), t p = true → Nat.Prime p) → ∀ (b : ℕ) (L : List (ℕ × ℕ)) (a : ℕ), List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) => t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) L a = true → ∀ (n : ℕ), a ≤ n → n ≤ b → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n.
Uses library Bool, Bool.true, List, List.foldr, Decidable.decide.
Lean, lines 39–60
```
 have key : ∀ t : ℕ → Bool, (∀ p : ℕ, t p = true → p.Prime) →
 ∀ (b : ℕ) (L : List (ℕ × ℕ)) (a : ℕ),
 List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) =>
 (t x.1 && decide (x.2 < x.1) &&
 decide (x.1 < 2 * lo) && decide ((2 * x.2 - x.1) * (2 * x.2 - x.1) ≤ lo)) && f (x.2 + 1))
 (fun lo => decide (b < lo)) L a = true →
 ∀ n : ℕ, a ≤ n → n ≤ b → ∃ p : ℕ, p.Prime ∧ n 
 intro a h n h1 h2
 simp only [List.foldr_nil, decide_eq_true_eq] at h
 omega
 | cons x L ih =>
 intro a h n h1 h2
 simp only [List.foldr_cons, Bool.and_eq_true, decide_eq_true_eq] at h
 obtain ⟨⟨⟨⟨c1, c4⟩, c5⟩, c6⟩, c7⟩ := h
 by_cases hn : n ≤ x.2
 · refine ⟨x.1, ht x.1 c1, by omega, by omega, ?_⟩
 have h3 : 2 * n - x.1 ≤ 2 * x.2 - x.1 := by omega
 exact le_trans (Nat.mul_le_mul h3 h3) (le_trans c6 h1)
 · exact ih (x.2 + 1) c7 n (by omega) h2
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 39–60 at feeca055f8c6 ↗
1. key.s1 case
 Leaves ∀ (a : ℕ), List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) => t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) [] a = true → ∀ (n : ℕ), a ≤ n → n ≤ b → ∃ (p : ℕ), Nat.Prime p ∧ n intro a h n h1 h2 simp only [List.foldr_nil, decide_eq_true_eq] at h omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 48–51 at feeca055f8c6 ↗
2. key.s2 case
 Leaves ∀ (a : ℕ), List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) => t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) (x :: L) a = true → ∀ (n : ℕ), a ≤ n → n ≤ b → ∃ (p : ℕ), Nat.Prime p ∧ n t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) L a = true → ∀ (n : ℕ), a ≤ n → n ≤ b → ∃ (p : ℕ), Nat.Prime p ∧ n intro a h n h1 h2 simp only [List.foldr_cons, Bool.and_eq_true, decide_eq_true_eq] at h obtain ⟨⟨⟨⟨c1, c4⟩, c5⟩, c6⟩, c7⟩ := h by_cases hn : n ≤ x.2 · refine ⟨x.1, ht x.1 c1, by omega, by omega, ?_⟩ have h3 : 2 * n - x.1 ≤ 2 * x.2 - x.1 := by omega exact le_trans (Nat.mul_le_mul h3 h3) (le_trans c6 h1) · exact ih (x.2 + 1) c7 n (by omega) h2
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 52–60 at feeca055f8c6 ↗
 key.s2.s1 obtain (((t x.1 = true ∧ x.2 < x.1) ∧ x.1 < (2 : ℕ) * a) ∧ ((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ a) ∧ List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) => t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) L (x.2 + (1 : ℕ)) = true
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ n t x.1 && decide (x.2 < x.1) && decide (x.1 < (2 : ℕ) * lo) && decide (((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ lo) && f (x.2 + (1 : ℕ))) (fun (lo : ℕ) => decide (b < lo)) L (x.2 + (1 : ℕ)) = true, c6 : ((2 : ℕ) * x.2 - x.1) * ((2 : ℕ) * x.2 - x.1) ≤ a, c5 : x.1 < (2 : ℕ) * a, c1 : t x.1 = true, c4 : x.2 < x.1.
 Lean, line 55
 obtain ⟨⟨⟨⟨c1, c4⟩, c5⟩, c6⟩, c7⟩ := h
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 55 at feeca055f8c6 ↗
 key.s2.s2 case
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n.
 Uses library Exists.intro, le_trans, Nat.mul_le_mul.
 Lean, lines 57–59
 · refine ⟨x.1, ht x.1 c1, by omega, by omega, ?_⟩ have h3 : 2 * n - x.1 ≤ 2 * x.2 - x.1 := by omega exact le_trans (Nat.mul_le_mul h3 h3) (le_trans c6 h1)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 57–59 at feeca055f8c6 ↗
 key.s2.s2.h3 have (2 : ℕ) * n - x.1 ≤ (2 : ℕ) * x.2 - x.1 routine: omega
 Leaves ((2 : ℕ) * n - x.1) * ((2 : ℕ) * n - x.1) ≤ n, with h3 : (2 : ℕ) * n - x.1 ≤ (2 : ℕ) * x.2 - x.1.
 Lean, line 58
 have h3 : 2 * n - x.1 ≤ 2 * x.2 - x.1 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 58 at feeca055f8c6 ↗
 key.s2.s3 case
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n.
 Lean, line 60
 · exact ih (x.2 + 1) c7 n (by omega) h2
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 60 at feeca055f8c6 ↗
r5b_bridge have ∀ (n p : ℕ), n < p → p < (2 : ℕ) * n → ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n → (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_bridge : ∀ (n p : ℕ), n < p → p < (2 : ℕ) * n → ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n → (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 61–91
```
 have r5b_bridge : ∀ n p : ℕ, n < p → p < 2 * n → (2 * n - p) * (2 * n - p) ≤ n →
 2 * (2 * n - p) ≤ n + 2 ∧
 ∀ α : ℕ, α < n → p < α + n →
 (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
 intro n p h1 h2 h3
 generalize hk : 2 * n - p = k at *
 constructor
 · rcases Nat.lt_or_ge k 3 with h | h
 · omega
 · have : 3 * k ≤ k * k := Nat.mul_le_mul_right _ h
 omega
 · intro α hα1 hα2
 right
 intro x y hxy hd
 by_contra hc
 have h : α * y < n * x := by omega
 have α0 : 0 < α := by omega
 have hx : x * y ≤ α := Nat.le_of_dvd α0 hd
 obtain ⟨s, rfl⟩ : ∃ s, n = α + s := ⟨n - α, by omega⟩
 have hs : s < k := by omega
 have a1 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have a2 : α < s * x := by nlinarith
 have a3 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have a4 : x + 1 < s := by
 by_contra hc
 have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega)
 nlinarith
 have a5 : (s + 1) * (s + 1) ≤ k * k := Nat.mul_le_mul hs hs
 have a6 : s * x ≤ s * s := Nat.mul_le_mul_left _ (by omega)
 nlinarith
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 61–91 at feeca055f8c6 ↗
1. r5b_bridge.s1 case
 Leaves (2 : ℕ) * k ≤ n + (2 : ℕ).
 Uses library Nat.lt_or_ge.
 Lean, lines 69–72
 · rcases Nat.lt_or_ge k 3 with h | h · omega · have : 3 * k ≤ k * k := Nat.mul_le_mul_right _ h omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 69–72 at feeca055f8c6 ↗
 r5b_bridge.s1.s1 case routine: omega
 Leaves (2 : ℕ) * k ≤ n + (2 : ℕ).
 Lean, line 70
 · omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 70 at feeca055f8c6 ↗
 r5b_bridge.s1.s2 case
 Leaves (2 : ℕ) * k ≤ n + (2 : ℕ).
 Lean, lines 71–72
 · have : 3 * k ≤ k * k := Nat.mul_le_mul_right _ h omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 71–72 at feeca055f8c6 ↗
 r5b_bridge.s1.s2.this have (3 : ℕ) * k ≤ k * k
 Leaves (2 : ℕ) * k ≤ n + (2 : ℕ), with this : (3 : ℕ) * k ≤ k * k.
 Uses library Nat.mul_le_mul_right.
 Lean, line 71
 · have : 3 * k ≤ k * k := Nat.mul_le_mul_right _ h
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 71 at feeca055f8c6 ↗
2. r5b_bridge.s2 case
 Leaves ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
 Lean, lines 73–91
 · intro α hα1 hα2 right intro x y hxy hd by_contra hc have h : α * y < n * x := by omega have α0 : 0 < α := by omega have hx : x * y ≤ α := Nat.le_of_dvd α0 hd obtain ⟨s, rfl⟩ : ∃ s, n = α + s := ⟨n - α, by omega⟩ have hs : s < k := by omega have a1 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy have a2 : α < s * x := by nlinarith have a3 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy have a4 : x + 1 < s := by by_contra hc have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega) nlinarith have a5 : (s + 1) * (s + 1) ≤ k * k := Nat.mul_le_mul hs hs have a6 : s * x ≤ s * s := Nat.mul_le_mul_left _ (by omega) nlinarith
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 73–91 at feeca055f8c6 ↗
 r5b_bridge.s2.h have α * y < n * x routine: omega
 Leaves False, with h : α * y < n * x.
 Lean, line 77
 have h : α * y < n * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 77 at feeca055f8c6 ↗
 r5b_bridge.s2._x3b10 (α0) have (0 : ℕ) < α routine: omega
 Leaves False, with α0 : (0 : ℕ) < α.
 Lean, line 78
 have α0 : 0 < α := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 78 at feeca055f8c6 ↗
 r5b_bridge.s2.hx have x * y ≤ α
 Leaves False, with hx : x * y ≤ α.
 Uses library Nat.le_of_dvd.
 Lean, line 79
 have hx : x * y ≤ α := Nat.le_of_dvd α0 hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 79 at feeca055f8c6 ↗
 r5b_bridge.s2.s4 obtain ∃ (s : ℕ), n = α + s
 Leaves False, with s : ℕ, h1 : α + s < p, h2 : p < (2 : ℕ) * (α + s), hk : (2 : ℕ) * (α + s) - p = k, h3 : k * k ≤ α + s, hα1 : α < α + s, hα2 : p < α + (α + s), hc : ¬(α + s) * x ≤ α * y, h : α * y < (α + s) * x.
 Uses library Exists.intro.
 Lean, line 80
 obtain ⟨s, rfl⟩ : ∃ s, n = α + s := ⟨n - α, by omega⟩
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 80 at feeca055f8c6 ↗
 r5b_bridge.s2.hs have s < k routine: omega
 Leaves False, with hs : s < k.
 Lean, line 81
 have hs : s < k := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 81 at feeca055f8c6 ↗
 r5b_bridge.s2.a1 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with a1 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 82
 have a1 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 82 at feeca055f8c6 ↗
 r5b_bridge.s2.a2 have α < s * x routine: nlinarith
 Leaves False, with a2 : α < s * x.
 Lean, line 83
 have a2 : α < s * x := by nlinarith
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 83 at feeca055f8c6 ↗
 r5b_bridge.s2.a3 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with a3 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 84
 have a3 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 84 at feeca055f8c6 ↗
 r5b_bridge.s2.a4 have x + (1 : ℕ) < s
 Leaves False, with a4 : x + (1 : ℕ) < s.
 Lean, lines 85–88
 have a4 : x + 1 < s := by by_contra hc have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega) nlinarith
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 85–88 at feeca055f8c6 ↗
 r5b_bridge.s2.a4.this have s * x ≤ (x + (1 : ℕ)) * x
 Leaves False, with this : s * x ≤ (x + (1 : ℕ)) * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 87
 have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 87 at feeca055f8c6 ↗
 r5b_bridge.s2.a5 have (s + (1 : ℕ)) * (s + (1 : ℕ)) ≤ k * k
 Leaves False, with a5 : (s + (1 : ℕ)) * (s + (1 : ℕ)) ≤ k * k.
 Uses library Nat.mul_le_mul.
 Lean, line 89
 have a5 : (s + 1) * (s + 1) ≤ k * k := Nat.mul_le_mul hs hs
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 89 at feeca055f8c6 ↗
 r5b_bridge.s2.a6 have s * x ≤ s * s
 Leaves False, with a6 : s * x ≤ s * s.
 Uses library Nat.mul_le_mul_left.
 Lean, line 90
 have a6 : s * x ≤ s * s := Nat.mul_le_mul_left _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 90 at feeca055f8c6 ↗
fin have ∀ (n : ℕ), (∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with fin : ∀ (n : ℕ), (∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 92–100
```
 have fin : ∀ n : ℕ, (∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ (2 * n - p) * (2 * n - p) ≤ n) →
 ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
 ∀ α : ℕ, α < n → p < α + n →
 (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
 intro n hw
 obtain ⟨p, hp, a, b, c⟩ := hw
 have br := r5b_bridge n p a b c
 exact ⟨p, hp, a, b, br.1, br.2⟩
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 92–100 at feeca055f8c6 ↗
1. fin.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with p : ℕ, hp : Nat.Prime p, a : n < p, b : p < (2 : ℕ) * n, c : ((2 : ℕ) * n - p) * ((2 : ℕ) * n - p) ≤ n.
 Lean, line 98
 obtain ⟨p, hp, a, b, c⟩ := hw
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 98 at feeca055f8c6 ↗
2. fin.br have (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with br : (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
 Lean, line 99
 have br := r5b_bridge n p a b c
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 99 at feeca055f8c6 ↗
r5b_cert_270 have ∃ (p : ℕ), Nat.Prime p ∧ (270 : ℕ) < p ∧ p < (2 : ℕ) * (270 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (270 : ℕ) - p) ≤ (270 : ℕ) + (2 : ℕ) ∧ ∀ α < (270 : ℕ), p < α + (270 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (270 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (270 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_cert_270 : ∃ (p : ℕ), Nat.Prime p ∧ (270 : ℕ) < p ∧ p < (2 : ℕ) * (270 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (270 : ℕ) - p) ≤ (270 : ℕ) + (2 : ℕ) ∧ ∀ α < (270 : ℕ), p < α + (270 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (270 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (270 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 101–125
```
 have r5b_cert_270 : ∃ p : ℕ, p.Prime ∧ 270 < p ∧ p < 2 * 270 ∧ 2 * (2 * 270 - p) ≤ 270 + 2 ∧
 ∀ α : ℕ, α < 270 → p < α + 270 →
 (∃ q : ℕ, q.Prime ∧ 270 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 270 * x ≤ α * y) := by
 refine ⟨523, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
 intro α h1 h2
 right
 intro x y hxy hd
 obtain ⟨m, hm⟩ := hd
 by_contra hc
 have hc' : α * y < 270 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 254 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have b2' : α * (x + 1) = α * x + α := by ring
 have b3 : 254 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have b4' : x * (x + 1) = x * x + x := by ring
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 have x1 : 16 ≤ x := by omega
 have x2 : x ≤ 15 := by
 by_contra h
 have : 16 * 16 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 101–125 at feeca055f8c6 ↗
1. r5b_cert_270.s1 obtain x * y ∣ α
 Leaves (270 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 109
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 109 at feeca055f8c6 ↗
2. r5b_cert_270.hc' have α * y < (270 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (270 : ℕ) * x.
 Lean, line 111
 have hc' : α * y < 270 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 111 at feeca055f8c6 ↗
3. r5b_cert_270.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 112
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 112 at feeca055f8c6 ↗
4. r5b_cert_270.b1 have (254 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (254 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 113
 have b1 : 254 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 113 at feeca055f8c6 ↗
5. r5b_cert_270.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 114
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 114 at feeca055f8c6 ↗
6. r5b_cert_270.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 115
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 115 at feeca055f8c6 ↗
7. r5b_cert_270.b3 have (254 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (254 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 116
 have b3 : 254 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 116 at feeca055f8c6 ↗
8. r5b_cert_270.b4 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with b4 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 117
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 117 at feeca055f8c6 ↗
9. r5b_cert_270.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 118
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 118 at feeca055f8c6 ↗
10. r5b_cert_270.b5 have x * y ≤ x * y * m
 Leaves False, with b5 : x * y ≤ x * y * m.
 Uses library Nat.le_mul_of_pos_right.
 Lean, line 119
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 119 at feeca055f8c6 ↗
11. r5b_cert_270.x1 have (16 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (16 : ℕ) ≤ x.
 Lean, line 120
 have x1 : 16 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 120 at feeca055f8c6 ↗
12. r5b_cert_270.x2 have x ≤ (15 : ℕ)
 Leaves False, with x2 : x ≤ (15 : ℕ).
 Lean, lines 121–124
 have x2 : x ≤ 15 := by by_contra h have : 16 * 16 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 121–124 at feeca055f8c6 ↗
 r5b_cert_270.x2.this have (16 : ℕ) * (16 : ℕ) ≤ x * x
 Leaves False, with this : (16 : ℕ) * (16 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 123
 have : 16 * 16 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 123 at feeca055f8c6 ↗
r5b_cert_677 have ∃ (p : ℕ), Nat.Prime p ∧ (677 : ℕ) < p ∧ p < (2 : ℕ) * (677 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (677 : ℕ) - p) ≤ (677 : ℕ) + (2 : ℕ) ∧ ∀ α < (677 : ℕ), p < α + (677 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (677 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (677 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_cert_677 : ∃ (p : ℕ), Nat.Prime p ∧ (677 : ℕ) < p ∧ p < (2 : ℕ) * (677 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (677 : ℕ) - p) ≤ (677 : ℕ) + (2 : ℕ) ∧ ∀ α < (677 : ℕ), p < α + (677 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (677 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (677 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 126–150
```
 have r5b_cert_677 : ∃ p : ℕ, p.Prime ∧ 677 < p ∧ p < 2 * 677 ∧ 2 * (2 * 677 - p) ≤ 677 + 2 ∧
 ∀ α : ℕ, α < 677 → p < α + 677 →
 (∃ q : ℕ, q.Prime ∧ 677 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 677 * x ≤ α * y) := by
 refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
 intro α h1 h2
 right
 intro x y hxy hd
 obtain ⟨m, hm⟩ := hd
 by_contra hc
 have hc' : α * y < 677 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 651 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have b2' : α * (x + 1) = α * x + α := by ring
 have b3 : 651 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have b4' : x * (x + 1) = x * x + x := by ring
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 have x1 : 26 ≤ x := by omega
 have x2 : x ≤ 25 := by
 by_contra h
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 126–150 at feeca055f8c6 ↗
1. r5b_cert_677.s1 obtain x * y ∣ α
 Leaves (677 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 134
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 134 at feeca055f8c6 ↗
2. r5b_cert_677.hc' have α * y < (677 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (677 : ℕ) * x.
 Lean, line 136
 have hc' : α * y < 677 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 136 at feeca055f8c6 ↗
3. r5b_cert_677.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 137
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 137 at feeca055f8c6 ↗
4. r5b_cert_677.b1 have (651 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (651 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 138
 have b1 : 651 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 138 at feeca055f8c6 ↗
5. r5b_cert_677.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 139
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 139 at feeca055f8c6 ↗
6. r5b_cert_677.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 140
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 140 at feeca055f8c6 ↗
7. r5b_cert_677.b3 have (651 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (651 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 141
 have b3 : 651 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 141 at feeca055f8c6 ↗
8. r5b_cert_677.b4 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with b4 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 142
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 142 at feeca055f8c6 ↗
9. r5b_cert_677.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 143
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 143 at feeca055f8c6 ↗
10. r5b_cert_677.b5 have x * y ≤ x * y * m
 Leaves False, with b5 : x * y ≤ x * y * m.
 Uses library Nat.le_mul_of_pos_right.
 Lean, line 144
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 144 at feeca055f8c6 ↗
11. r5b_cert_677.x1 have (26 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (26 : ℕ) ≤ x.
 Lean, line 145
 have x1 : 26 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 145 at feeca055f8c6 ↗
12. r5b_cert_677.x2 have x ≤ (25 : ℕ)
 Leaves False, with x2 : x ≤ (25 : ℕ).
 Lean, lines 146–149
 have x2 : x ≤ 25 := by by_contra h have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 146–149 at feeca055f8c6 ↗
 r5b_cert_677.x2.this have (26 : ℕ) * (26 : ℕ) ≤ x * x
 Leaves False, with this : (26 : ℕ) * (26 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 148
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 148 at feeca055f8c6 ↗
r5b_cert_678 have ∃ (p : ℕ), Nat.Prime p ∧ (678 : ℕ) < p ∧ p < (2 : ℕ) * (678 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (678 : ℕ) - p) ≤ (678 : ℕ) + (2 : ℕ) ∧ ∀ α < (678 : ℕ), p < α + (678 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (678 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (678 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_cert_678 : ∃ (p : ℕ), Nat.Prime p ∧ (678 : ℕ) < p ∧ p < (2 : ℕ) * (678 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (678 : ℕ) - p) ≤ (678 : ℕ) + (2 : ℕ) ∧ ∀ α < (678 : ℕ), p < α + (678 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (678 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (678 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 151–182
```
 have r5b_cert_678 : ∃ p : ℕ, p.Prime ∧ 678 < p ∧ p < 2 * 678 ∧ 2 * (2 * 678 - p) ≤ 678 + 2 ∧
 ∀ α : ℕ, α < 678 → p < α + 678 →
 (∃ q : ℕ, q.Prime ∧ 678 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 678 * x ≤ α * y) := by
 refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
 intro α h1 h2
 by_cases e650 : α = 650
 · left
 exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 right
 intro x y hxy hd
 obtain ⟨m, hm⟩ := hd
 by_contra hc
 have hc' : α * y < 678 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 650 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have b2' : α * (x + 1) = α * x + α := by ring
 have b3 : 650 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have b4' : x * (x + 1) = x * x + x := by ring
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 have x1 : 24 ≤ x := by omega
 have x2 : x ≤ 25 := by
 by_contra h
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 25 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 26 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 151–182 at feeca055f8c6 ↗
1. r5b_cert_678.s1 case
 Leaves (∃ (q : ℕ), Nat.Prime q ∧ (678 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * ((1327 : ℕ) - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (678 : ℕ) * x ≤ α * y.
 Uses library Exists.intro.
 Lean, lines 158–159
 · left exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 158–159 at feeca055f8c6 ↗
2. r5b_cert_678.s2 obtain x * y ∣ α
 Leaves (678 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 162
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 162 at feeca055f8c6 ↗
3. r5b_cert_678.hc' have α * y < (678 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (678 : ℕ) * x.
 Lean, line 164
 have hc' : α * y < 678 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 164 at feeca055f8c6 ↗
4. r5b_cert_678.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 165
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 165 at feeca055f8c6 ↗
5. r5b_cert_678.b1 have (650 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (650 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 166
 have b1 : 650 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 166 at feeca055f8c6 ↗
6. r5b_cert_678.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 167
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 167 at feeca055f8c6 ↗
7. r5b_cert_678.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 168
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 168 at feeca055f8c6 ↗
8. r5b_cert_678.b3 have (650 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (650 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 169
 have b3 : 650 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 169 at feeca055f8c6 ↗
9. r5b_cert_678.b4 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with b4 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 170
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 170 at feeca055f8c6 ↗
10. r5b_cert_678.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 171
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 171 at feeca055f8c6 ↗
11. r5b_cert_678.b5 have x * y ≤ x * y * m
 Leaves False, with b5 : x * y ≤ x * y * m.
 Uses library Nat.le_mul_of_pos_right.
 Lean, line 172
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 172 at feeca055f8c6 ↗
12. r5b_cert_678.x1 have (24 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (24 : ℕ) ≤ x.
 Lean, line 173
 have x1 : 24 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 173 at feeca055f8c6 ↗
13. r5b_cert_678.x2 have x ≤ (25 : ℕ)
 Leaves False, with x2 : x ≤ (25 : ℕ).
 Lean, lines 174–177
 have x2 : x ≤ 25 := by by_contra h have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 174–177 at feeca055f8c6 ↗
 r5b_cert_678.x2.this have (26 : ℕ) * (26 : ℕ) ≤ x * x
 Leaves False, with this : (26 : ℕ) * (26 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 176
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 176 at feeca055f8c6 ↗
14. r5b_cert_678.s14 case
 Leaves False.
 Lean, lines 179–180
 · have y2 : y ≤ 25 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 179–180 at feeca055f8c6 ↗
 r5b_cert_678.s14.y2 have y ≤ (25 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (25 : ℕ).
 Lean, line 179
 · have y2 : y ≤ 25 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 179 at feeca055f8c6 ↗
15. r5b_cert_678.s15 case
 Leaves False.
 Lean, lines 181–182
 · have y2 : y ≤ 26 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 181–182 at feeca055f8c6 ↗
 r5b_cert_678.s15.y2 have y ≤ (26 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (26 : ℕ).
 Lean, line 181
 · have y2 : y ≤ 26 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 181 at feeca055f8c6 ↗
r5b_cert_679 have ∃ (p : ℕ), Nat.Prime p ∧ (679 : ℕ) < p ∧ p < (2 : ℕ) * (679 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (679 : ℕ) - p) ≤ (679 : ℕ) + (2 : ℕ) ∧ ∀ α < (679 : ℕ), p < α + (679 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (679 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (679 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_cert_679 : ∃ (p : ℕ), Nat.Prime p ∧ (679 : ℕ) < p ∧ p < (2 : ℕ) * (679 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (679 : ℕ) - p) ≤ (679 : ℕ) + (2 : ℕ) ∧ ∀ α < (679 : ℕ), p < α + (679 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (679 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (679 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 183–218
```
 have r5b_cert_679 : ∃ p : ℕ, p.Prime ∧ 679 < p ∧ p < 2 * 679 ∧ 2 * (2 * 679 - p) ≤ 679 + 2 ∧
 ∀ α : ℕ, α < 679 → p < α + 679 →
 (∃ q : ℕ, q.Prime ∧ 679 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 679 * x ≤ α * y) := by
 refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
 intro α h1 h2
 by_cases e650 : α = 650
 · left
 exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 right
 intro x y hxy hd
 obtain ⟨m, hm⟩ := hd
 by_contra hc
 have hc' : α * y < 679 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 649 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have b2' : α * (x + 1) = α * x + α := by ring
 have b3 : 649 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have b4' : x * (x + 1) = x * x + x := by ring
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 have x1 : 22 ≤ x := by omega
 have x2 : x ≤ 25 := by
 by_contra h
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 23 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 24 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 25 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 26 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 183–218 at feeca055f8c6 ↗
1. r5b_cert_679.s1 case
 Leaves (∃ (q : ℕ), Nat.Prime q ∧ (679 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * ((1327 : ℕ) - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (679 : ℕ) * x ≤ α * y.
 Uses library Exists.intro.
 Lean, lines 190–191
 · left exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 190–191 at feeca055f8c6 ↗
2. r5b_cert_679.s2 obtain x * y ∣ α
 Leaves (679 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 194
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 194 at feeca055f8c6 ↗
3. r5b_cert_679.hc' have α * y < (679 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (679 : ℕ) * x.
 Lean, line 196
 have hc' : α * y < 679 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 196 at feeca055f8c6 ↗
4. r5b_cert_679.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 197
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 197 at feeca055f8c6 ↗
5. r5b_cert_679.b1 have (649 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (649 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 198
 have b1 : 649 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 198 at feeca055f8c6 ↗
6. r5b_cert_679.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 199
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 199 at feeca055f8c6 ↗
7. r5b_cert_679.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 200
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 200 at feeca055f8c6 ↗
8. r5b_cert_679.b3 have (649 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (649 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 201
 have b3 : 649 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 201 at feeca055f8c6 ↗
9. r5b_cert_679.b4 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with b4 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 202
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 202 at feeca055f8c6 ↗
10. r5b_cert_679.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 203
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 203 at feeca055f8c6 ↗
11. r5b_cert_679.b5 have x * y ≤ x * y * m
 Leaves False, with b5 : x * y ≤ x * y * m.
 Uses library Nat.le_mul_of_pos_right.
 Lean, line 204
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 204 at feeca055f8c6 ↗
12. r5b_cert_679.x1 have (22 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (22 : ℕ) ≤ x.
 Lean, line 205
 have x1 : 22 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 205 at feeca055f8c6 ↗
13. r5b_cert_679.x2 have x ≤ (25 : ℕ)
 Leaves False, with x2 : x ≤ (25 : ℕ).
 Lean, lines 206–209
 have x2 : x ≤ 25 := by by_contra h have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 206–209 at feeca055f8c6 ↗
 r5b_cert_679.x2.this have (26 : ℕ) * (26 : ℕ) ≤ x * x
 Leaves False, with this : (26 : ℕ) * (26 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 208
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 208 at feeca055f8c6 ↗
14. r5b_cert_679.s14 case
 Leaves False.
 Lean, lines 211–212
 · have y2 : y ≤ 23 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 211–212 at feeca055f8c6 ↗
 r5b_cert_679.s14.y2 have y ≤ (23 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (23 : ℕ).
 Lean, line 211
 · have y2 : y ≤ 23 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 211 at feeca055f8c6 ↗
15. r5b_cert_679.s15 case
 Leaves False.
 Lean, lines 213–214
 · have y2 : y ≤ 24 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 213–214 at feeca055f8c6 ↗
 r5b_cert_679.s15.y2 have y ≤ (24 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (24 : ℕ).
 Lean, line 213
 · have y2 : y ≤ 24 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 213 at feeca055f8c6 ↗
16. r5b_cert_679.s16 case
 Leaves False.
 Lean, lines 215–216
 · have y2 : y ≤ 25 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 215–216 at feeca055f8c6 ↗
 r5b_cert_679.s16.y2 have y ≤ (25 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (25 : ℕ).
 Lean, line 215
 · have y2 : y ≤ 25 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 215 at feeca055f8c6 ↗
17. r5b_cert_679.s17 case
 Leaves False.
 Lean, lines 217–218
 · have y2 : y ≤ 26 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 217–218 at feeca055f8c6 ↗
 r5b_cert_679.s17.y2 have y ≤ (26 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (26 : ℕ).
 Lean, line 217
 · have y2 : y ≤ 26 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 217 at feeca055f8c6 ↗
r5b_cert_680 have ∃ (p : ℕ), Nat.Prime p ∧ (680 : ℕ) < p ∧ p < (2 : ℕ) * (680 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (680 : ℕ) - p) ≤ (680 : ℕ) + (2 : ℕ) ∧ ∀ α < (680 : ℕ), p < α + (680 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (680 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (680 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with r5b_cert_680 : ∃ (p : ℕ), Nat.Prime p ∧ (680 : ℕ) < p ∧ p < (2 : ℕ) * (680 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (680 : ℕ) - p) ≤ (680 : ℕ) + (2 : ℕ) ∧ ∀ α < (680 : ℕ), p < α + (680 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (680 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (680 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 219–256
```
 have r5b_cert_680 : ∃ p : ℕ, p.Prime ∧ 680 < p ∧ p < 2 * 680 ∧ 2 * (2 * 680 - p) ≤ 680 + 2 ∧
 ∀ α : ℕ, α < 680 → p < α + 680 →
 (∃ q : ℕ, q.Prime ∧ 680 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 680 * x ≤ α * y) := by
 refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
 intro α h1 h2
 by_cases e650 : α = 650
 · left
 exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 right
 intro x y hxy hd
 obtain ⟨m, hm⟩ := hd
 by_contra hc
 have hc' : α * y < 680 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 648 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 have b2' : α * (x + 1) = α * x + α := by ring
 have b3 : 648 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 have b4' : x * (x + 1) = x * x + x := by ring
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 have x1 : 21 ≤ x := by omega
 have x2 : x ≤ 25 := by
 by_contra h
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 22 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 23 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 24 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 25 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 26 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 219–256 at feeca055f8c6 ↗
1. r5b_cert_680.s1 case
 Leaves (∃ (q : ℕ), Nat.Prime q ∧ (680 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * ((1327 : ℕ) - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (680 : ℕ) * x ≤ α * y.
 Uses library Exists.intro.
 Lean, lines 226–227
 · left exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 226–227 at feeca055f8c6 ↗
2. r5b_cert_680.s2 obtain x * y ∣ α
 Leaves (680 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 230
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 230 at feeca055f8c6 ↗
3. r5b_cert_680.hc' have α * y < (680 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (680 : ℕ) * x.
 Lean, line 232
 have hc' : α * y < 680 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 232 at feeca055f8c6 ↗
4. r5b_cert_680.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 233
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 233 at feeca055f8c6 ↗
5. r5b_cert_680.b1 have (648 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (648 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 234
 have b1 : 648 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 234 at feeca055f8c6 ↗
6. r5b_cert_680.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 235
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 235 at feeca055f8c6 ↗
7. r5b_cert_680.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 236
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 236 at feeca055f8c6 ↗
8. r5b_cert_680.b3 have (648 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (648 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 237
 have b3 : 648 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 237 at feeca055f8c6 ↗
9. r5b_cert_680.b4 have x * (x + (1 : ℕ)) ≤ x * y
 Leaves False, with b4 : x * (x + (1 : ℕ)) ≤ x * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 238
 have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 238 at feeca055f8c6 ↗
10. r5b_cert_680.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 239
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 239 at feeca055f8c6 ↗
11. r5b_cert_680.b5 have x * y ≤ x * y * m
 Leaves False, with b5 : x * y ≤ x * y * m.
 Uses library Nat.le_mul_of_pos_right.
 Lean, line 240
 have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 240 at feeca055f8c6 ↗
12. r5b_cert_680.x1 have (21 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (21 : ℕ) ≤ x.
 Lean, line 241
 have x1 : 21 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 241 at feeca055f8c6 ↗
13. r5b_cert_680.x2 have x ≤ (25 : ℕ)
 Leaves False, with x2 : x ≤ (25 : ℕ).
 Lean, lines 242–245
 have x2 : x ≤ 25 := by by_contra h have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 242–245 at feeca055f8c6 ↗
 r5b_cert_680.x2.this have (26 : ℕ) * (26 : ℕ) ≤ x * x
 Leaves False, with this : (26 : ℕ) * (26 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 244
 have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 244 at feeca055f8c6 ↗
14. r5b_cert_680.s14 case
 Leaves False.
 Lean, lines 247–248
 · have y2 : y ≤ 22 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 247–248 at feeca055f8c6 ↗
 r5b_cert_680.s14.y2 have y ≤ (22 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (22 : ℕ).
 Lean, line 247
 · have y2 : y ≤ 22 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 247 at feeca055f8c6 ↗
15. r5b_cert_680.s15 case
 Leaves False.
 Lean, lines 249–250
 · have y2 : y ≤ 23 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 249–250 at feeca055f8c6 ↗
 r5b_cert_680.s15.y2 have y ≤ (23 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (23 : ℕ).
 Lean, line 249
 · have y2 : y ≤ 23 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 249 at feeca055f8c6 ↗
16. r5b_cert_680.s16 case
 Leaves False.
 Lean, lines 251–252
 · have y2 : y ≤ 24 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 251–252 at feeca055f8c6 ↗
 r5b_cert_680.s16.y2 have y ≤ (24 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (24 : ℕ).
 Lean, line 251
 · have y2 : y ≤ 24 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 251 at feeca055f8c6 ↗
17. r5b_cert_680.s17 case
 Leaves False.
 Lean, lines 253–254
 · have y2 : y ≤ 25 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 253–254 at feeca055f8c6 ↗
 r5b_cert_680.s17.y2 have y ≤ (25 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (25 : ℕ).
 Lean, line 253
 · have y2 : y ≤ 25 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 253 at feeca055f8c6 ↗
18. r5b_cert_680.s18 case
 Leaves False.
 Lean, lines 255–256
 · have y2 : y ≤ 26 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 255–256 at feeca055f8c6 ↗
 r5b_cert_680.s18.y2 have y ≤ (26 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (26 : ℕ).
 Lean, line 255
 · have y2 : y ≤ 26 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 255 at feeca055f8c6 ↗
s11 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 259–260
```
 · subst e270
 exact r5b_cert_270
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 259–260 at feeca055f8c6 ↗
s12 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 262–263
```
 · subst e677
 exact r5b_cert_677
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 262–263 at feeca055f8c6 ↗
s13 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 265–266
```
 · subst e678
 exact r5b_cert_678
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 265–266 at feeca055f8c6 ↗
s14 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 268–269
```
 · subst e679
 exact r5b_cert_679
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 268–269 at feeca055f8c6 ↗
s15 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Lean, lines 271–272
```
 · subst e680
 exact r5b_cert_680
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, lines 271–272 at feeca055f8c6 ↗
s16 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.
Uses library Decidable.decide, Nat.gcd, Lean.Parser.Tactic.DecideConfig.kernel.
Lean, line 274
```
 · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 269 [(457, 236), (467, 241), (479, 247), (491, 253), (503, 259), (509, 262), (523, 269)] 229 (by decide +kernel) n (by omega) s269)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 274 at feeca055f8c6 ↗

s17 case

Leaves ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.

Uses library Decidable.decide, Nat.gcd, Lean.Parser.Tactic.DecideConfig.kernel.

Lean, line 276

  · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 676 [(541, 278), (557, 286), (571, 293), (587, 302), (601, 309), (619, 318), (631, 324), (647, 332), (661, 339), (677, 347), (691, 354), (709, 363), (727, 373), (743, 381), (761, 390), (773, 396), (787, 403), (797, 408), (811, 415), (829, 424), (839, 429), (859, 439), (877, 448), (887, 454), (907, 464), (929, 475), (947, 484), (967, 494), (983, 502), (997, 509), (1019, 520), (1039, 530), (1061, 542), (1069, 546), (1093, 558), (1117, 570), (1129, 576), (1153, 588), (1171, 597), (1193, 608), (1217, 620), (1237, 630), (1259, 642), (1283, 654), (1307, 666), (1327, 676)] 271 (by decide +kernel) n (by omega) s676)

targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 276 at feeca055f8c6 ↗

s18 case

Uses library Decidable.decide, Nat.gcd, Lean.Parser.Tactic.DecideConfig.kernel.

Lean, line 278

  · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 200014 [(1361, 693), (1381, 703), (1399, 712), (1423, 724), (1447, 736), (1471, 749), (1499, 763), (1523, 775), (1549, 788), (1571, 799), (1597, 812), (1621, 824), (1637, 832), (1663, 845), (1669, 849), (1699, 864), (1723, 876), (1753, 891), (1783, 906), (1811, 920), (1831, 930), (1861, 945), (1889, 959), (1913, 971), (1933, 982), (1951, 991), (1979, 1005), (2011, 1021), (2039, 1035), (2069, 1050), (2099, 1065), (2131, 1081), (2161, 1096), (2179, 1106), (2213, 1123), (2243, 1138), (2273, 1153), (2297, 1165), (2311, 1172), (2341, 1187), (2371, 1202), (2399, 1216), (2423, 1228), (2447, 1241), (2477, 1256), (2503, 1269), (2539, 1287), (2557, 1296), (2593, 1314), (2621, 1328), (2657, 1346), (2693, 1364), (2729, 1382), (2753, 1395), (2791, 1414), (2819, 1428), (2857, 1447), (2887, 1462), (2917, 1477), (2953, 1495), (2971, 1504), (3001, 1519), (3037, 1537), (3067, 1553), (3089, 1564), (3121, 1580), (3137, 1588), (3169, 1604), (3209, 1624), (3229, 1634), (3259, 1649), (3299, 1669), (3331, 1685), (3371, 1706), (3413, 1727), (3449, 1745), (3491, 1766), (3533, 1787), (3571, 1806), (3613, 1827), (3643, 1842), (3677, 1859), (3719, 1881), (3761, 1902), (3803, 1923), (3847, 1945), (3889, 1966), (3931, 1987), (3967, 2005), (4007, 2025), (4051, 2048), (4093, 2069), (4139, 2092), (4177, 2111), (4219, 2132), (4261, 2153), (4297, 2171), (4339, 2192), (4373, 2209), (4409, 2228), (4457, 2252), (4493, 2270), (4523, 2285), (4567, 2307), (4603, 2325), (4651, 2349), (4691, 2369), (4733, 2390), (4759, 2403), (4801, 2425), (4831, 2440), (4877, 2463), (4919, 2484), (4969, 2509), (5011, 2530), (5059, 2554), (5107, 2578), (5153, 2601), (5197, 2624), (5237, 2644), (5281, 2666), (5333, 2692), (5381, 2716), (5431, 2741), (5483, 2767), (5531, 2791), (5581, 2816), (5623, 2838), (5669, 2861), (5717, 2885), (5749, 2901), (5801, 2927), (5851, 2952), (5903, 2978), (5953, 3003), (6007, 3030), (6053, 3054), (6101, 3078), (6151, 3103), (6203, 3129), (6257, 3156), (6311, 3183), (6367, 3211), (6421, 3238), (6473, 3264), (6529, 3293), (6581, 3319), (6637, 3347), (6691, 3374), (6737, 3397), (6793, 3425), (6841, 3449), (6899, 3478), (6949, 3503), (7001, 3530), (7057, 3558), (7109, 3584), (7159, 3609), (7219, 3639), (7253, 3656), (7309, 3684), (7369, 3714), (7417, 3738), (7477, 3769), (7537, 3799), (7591, 3826), (7649, 3855), (7703, 3882), (7759, 3910), (7817, 3939), (7879, 3970), (7937, 4000), (7993, 4028), (8053, 4058), (8117, 4090), (8179, 4121), (8243, 4153), (8297, 4180), (8353, 4208), (8389, 4226), (8447, 4256), (8513, 4289), (8573, 4319), (8629, 4347), (8693, 4379), (8753, 4409), (8819, 4442), (8867, 4466), (8933, 4499), (8999, 4533), (9067, 4567), (9133, 4600), (9199, 4633), (9257, 4662), (9323, 4695), (9391, 4729), (9439, 4753), (9497, 4782), (9551, 4810), (9619, 4844), (9689, 4879), (9749, 4909), (9817, 4943), (9887, 4978), (9949, 5009), (10009, 5039), (10079, 5074), (10141, 5106), (10211, 5141), (10273, 5172), (10343, 5207), (10399, 5235), (10463, 5267), (10531, 5301), (10601, 5336), (10667, 5370), (10739, 5406), (10799, 5436), (10867, 5470), (10939, 5506), (11003, 5538), (11071, 5572), (11131, 5602), (11197, 5635), (11261, 5668), (11329, 5702), (11399, 5737), (11471, 5773), (11527, 5801), (11597, 5836), (11657, 5866), (11731, 5903), (11807, 5941), (11867, 5972), (11941, 6009), (12011, 6044), (12073, 6075), (12149, 6113), (12227, 6152), (12301, 6189), (12379, 6228), (12457, 6267), (12527, 6303), (12601, 6340), (12671, 6375), (12743, 6411), (12823, 6451), (12899, 6489), (12979, 6529), (13049, 6564), (13127, 6604), (13187, 6634), (13267, 6674), (13339, 6710), (13421, 6751), (13499, 6790), (13577, 6829), (13649, 6865), (13729, 6905), (13807, 6945), (13883, 6983), (13967, 7025), (14051, 7067), (14107, 7095), (14177, 7130), (14251, 7167), (14327, 7205), (14411, 7247), (14489, 7287), (14563, 7324), (14639, 7362), (14723, 7404), (14797, 7441), (14879, 7482), (14957, 7521), (15031, 7558), (15107, 7596), (15193, 7640), (15277, 7682), (15361, 7724), (15443, 7765), (15527, 7807), (15607, 7847), (15683, 7885), (15767, 7927), (15823, 7956), (15913, 8001), (16001, 8045), (16091, 8090), (16141, 8115), (16231, 8160), (16319, 8204), (16381, 8235), (16453, 8271), (16529, 8309), (16619, 8355), (16703, 8397), (16787, 8439), (16879, 8485), (16963, 8527), (17053, 8572), (17137, 8614), (17209, 8650), (17299, 8696), (17393, 8743), (17483, 8788), (17573, 8833), (17659, 8876), (17749, 8921), (17839, 8966), (17929, 9011), (18013, 9053), (18097, 9096), (18191, 9143), (18287, 9191), (18379, 9237), (18461, 9278), (18553, 9324), (18637, 9366), (18731, 9413), (18803, 9450), (18899, 9498), (18979, 9538), (19073, 9585), (19163, 9630), (19259, 9678), (19333, 9715), (19429, 9763), (19507, 9802), (19603, 9851), (19699, 9899), (19793, 9946), (19891, 9995), (19991, 10045), (20089, 10094), (20183, 10141), (20269, 10184), (20369, 10234), (20443, 10272), (20543, 10322), (20641, 10371), (20743, 10422), (20809, 10455), (20903, 10502), (21001, 10551), (21101, 10601), (21193, 10647), (21283, 10693), (21383, 10743), (21487, 10795), (21589, 10846), (21683, 10893), (21787, 10945), (21881, 10992), (21977, 11040), (22079, 11092), (22171, 11138), (22277, 11191), (22381, 11243), (22483, 11294), (22573, 11339), (22679, 11392), (22783, 11444), (22877, 11491), (22973, 11540), (23081, 11594), (23189, 11648), (23297, 11702), (23399, 11753), (23497, 11802), (23603, 11855), (23689, 11898), (23789, 11949), (23899, 12004), (24007, 12058), (24113, 12111), (24223, 12166), (24329, 12219), (24439, 12274), (24547, 12328), (24631, 12371), (24733, 12422), (24841, 12476), (24953, 12532), (25057, 12584), (25169, 12640), (25261, 12686), (25373, 12742), (25471, 12791), (25583, 12848), (25693, 12903), (25801, 12957), (25913, 13013), (26021, 13067), (26119, 13116), (26227, 13170), (26339, 13226), (26449, 13282), (26561, 13338), (26669, 13392), (26783, 13449), (26893, 13504), (26993, 13554), (27109, 13612), (27211, 13663), (27299, 13707), (27409, 13763), (27527, 13822), (27631, 13874), (27749, 13933), (27851, 13984), (27967, 14042), (28081, 14099), (28183, 14150), (28297, 14207), (28411, 14265), (28517, 14318), (28631, 14375), (28751, 14435), (28871, 14495), (28979, 14549), (29077, 14598), (29191, 14655), (29311, 14716), (29429, 14775), (29537, 14829), (29641, 14881), (29761, 14941), (29881, 15001), (29989, 15055), (30109, 15115), (30223, 15172), (30341, 15232), (30449, 15286), (30559, 15341), (30677, 15400), (30781, 15452), (30893, 15508), (31013, 15568), (31123, 15623), (31247, 15685), (31357, 15741), (31481, 15803), (31607, 15866), (31729, 15927), (31849, 15987), (31973, 16049), (32099, 16112), (32213, 16169), (32327, 16227), (32443, 16285), (32569, 16348), (32693, 16410), (32803, 16465), (32917, 16522), (33037, 16582), (33161, 16644), (33289, 16709), (33413, 16771), (33533, 16831), (33647, 16888), (33773, 16951), (33893, 17011), (34019, 17074), (34147, 17138), (34273, 17201), (34403, 17267), (34519, 17325), (34651, 17391), (34781, 17456), (34913, 17522), (35027, 17579), (35159, 17645), (35291, 17711), (35423, 17778), (35543, 17838), (35677, 17905), (35809, 17971), (35933, 18033), (36067, 18100), (36191, 18162), (36319, 18226), (36451, 18293), (36587, 18361), (36721, 18428), (36857, 18496), (36979, 18557), (37097, 18616), (37223, 18679), (37357, 18746), (37493, 18814), (37619, 18878), (37747, 18942), (37879, 19008), (38011, 19074), (38149, 19143), (38287, 19212), (38393, 19265), (38501, 19319), (38639, 19388), (38767, 19453), (38903, 19521), (39043, 19591), (39181, 19660), (39317, 19728), (39451, 19795), (39581, 19860), (39719, 19929), (39857, 19999), (39989, 20065), (40129, 20135), (40253, 20197), (40387, 20264), (40529, 20335), (40639, 20390), (40771, 20456), (40903, 20523), (41047, 20595), (41189, 20666), (41333, 20738), (41467, 20805), (41611, 20877), (41737, 20940), (41879, 21011), (42023, 21083), (42157, 21151), (42299, 21222), (42443, 21294), (42589, 21367), (42727, 21436), (42863, 21504), (43003, 21574), (43133, 21639), (43271, 21709), (43411, 21779), (43543, 21845), (43691, 21919), (43801, 21974), (43943, 22045), (44089, 22118), (44221, 22184), (44357, 22252), (44501, 22325), (44651, 22400), (44797, 22473), (44939, 22544), (45083, 22616), (45233, 22691), (45377, 22763), (45523, 22836), (45673, 22912), (45823, 22987), (45971, 23061), (46103, 23127), (46237, 23194), (46381, 23266), (46523, 23337), (46663, 23407), (46811, 23481), (46957, 23555), (47111, 23632), (47251, 23702), (47389, 23771), (47543, 23848), (47681, 23917), (47819, 23986), (47969, 24061), (48121, 24138), (48271, 24213), (48413, 24284), (48563, 24359), (48679, 24417), (48823, 24489), (48973, 24564), (49123, 24639), (49279, 24717), (49433, 24795), (49559, 24858), (49711, 24934), (49853, 25005), (49999, 25078), (50153, 25155), (50311, 25234), (50461, 25309), (50599, 25379), (50753, 25456), (50909, 25534), (51061, 25610), (51217, 25688), (51361, 25760), (51521, 25840), (51679, 25919), (51839, 25999), (51991, 26076), (52153, 26157), (52313, 26237), (52457, 26309), (52609, 26385), (52769, 26465), (52919, 26540), (53077, 26619), (53239, 26701), (53401, 26782), (53551, 26857), (53699, 26931), (53861, 27012), (54013, 27088), (54167, 27165), (54331, 27247), (54493, 27329), (54647, 27406), (54799, 27482), (54959, 27562), (55117, 27641), (55259, 27712), (55411, 27788), (55547, 27856), (55711, 27938), (55871, 28019), (56039, 28103), (56207, 28187), (56369, 28268), (56533, 28350), (56701, 28434), (56857, 28512), (56999, 28583), (57163, 28666), (57331, 28750), (57493, 28831), (57653, 28911), (57809, 28989), (57977, 29073), (58147, 29158), (58313, 29241), (58481, 29326), (58631, 29401), (58789, 29480), (58943, 29557), (59113, 29642), (59281, 29726), (59453, 29812), (59621, 29896), (59791, 29981), (59957, 30065), (60127, 30150), (60293, 30233), (60457, 30315), (60631, 30402), (60793, 30483), (60961, 30567), (61129, 30651), (61297, 30736), (61471, 30823), (61643, 30909), (61819, 30997), (61991, 31083), (62143, 31159), (62311, 31243), (62483, 31329), (62659, 31418), (62827, 31502), (62989, 31583), (63149, 31663), (63317, 31747), (63493, 31835), (63671, 31924), (63841, 32009), (64019, 32098), (64189, 32184), (64333, 32256), (64513, 32346), (64693, 32436), (64871, 32525), (65033, 32606), (65213, 32696), (65393, 32786), (65563, 32872), (65731, 32956), (65899, 33040), (66071, 33126), (66239, 33210), (66413, 33297), (66593, 33387), (66763, 33472), (66943, 33562), (67121, 33652), (67289, 33736), (67453, 33818), (67631, 33907), (67807, 33995), (67987, 34085), (68171, 34177), (68351, 34267), (68531, 34358), (68713, 34449), (68899, 34542), (69073, 34629), (69259, 34722), (69439, 34812), (69623, 34904), (69809, 34997), (69991, 35089), (70177, 35182), (70351, 35269), (70537, 35362), (70717, 35452), (70901, 35544), (71089, 35638), (71263, 35725), (71443, 35816), (71633, 35911), (71821, 36005), (71999, 36094), (72173, 36181), (72353, 36271), (72533, 36361), (72719, 36454), (72907, 36548), (73091, 36641), (73277, 36734), (73459, 36825), (73651, 36921), (73823, 37007), (73999, 37095), (74189, 37190), (74381, 37286), (74573, 37383), (74761, 37477), (74941, 37567), (75133, 37663), (75323, 37758), (75511, 37852), (75703, 37948), (75883, 38038), (76039, 38117), (76231, 38213), (76423, 38309), (76607, 38401), (76801, 38498), (76991, 38593), (77171, 38683), (77359, 38777), (77551, 38873), (77747, 38972), (77933, 39065), (78121, 39159), (78317, 39257), (78511, 39354), (78707, 39452), (78901, 39549), (79087, 39642), (79283, 39741), (79481, 39840), (79669, 39934), (79867, 40033), (80051, 40125), (80251, 40225), (80449, 40324), (80629, 40414), (80819, 40510), (81019, 40610), (81203, 40702), (81401, 40801), (81569, 40885), (81769, 40985), (81971, 41086), (82171, 41186), (82373, 41287), (82571, 41387), (82763, 41483), (82963, 41583), (83137, 41670), (83341, 41772), (83537, 41870), (83737, 41970), (83939, 42071), (84143, 42174), (84349, 42277), (84551, 42378), (84751, 42478), (84947, 42576), (85147, 42676), (85333, 42769), (85531, 42868), (85733, 42970), (85933, 43070), (86137, 43172), (86341, 43274), (86539, 43373), (86743, 43475), (86951, 43579), (87151, 43679), (87359, 43783), (87559, 43884), (87767, 43988), (87977, 44093), (88177, 44193), (88379, 44294), (88589, 44399), (88799, 44504), (89009, 44609), (89213, 44712), (89417, 44814), (89627, 44919), (89839, 45025), (90031, 45121), (90239, 45225), (90439, 45325), (90647, 45429), (90847, 45530), (91033, 45623), (91243, 45728), (91457, 45835), (91639, 45926), (91841, 46027), (92051, 46132), (92251, 46232), (92461, 46338), (92671, 46443), (92867, 46541), (93083, 46649), (93287, 46751), (93503, 46859), (93719, 46967), (93923, 47069), (94121, 47168), (94331, 47274), (94547, 47382), (94747, 47482), (94961, 47589), (95177, 47697), (95393, 47805), (95603, 47910), (95819, 48018), (96017, 48118), (96233, 48226), (96451, 48335), (96671, 48445), (96857, 48538), (97073, 48646), (97283, 48751), (97501, 48860), (97711, 48966), (97931, 49076), (98143, 49182), (98347, 49284), (98563, 49392), (98779, 49500), (98999, 49610), (99191, 49706), (99409, 49815), (99623, 49923), (99839, 50031), (100057, 50140), (100279, 50251), (100501, 50362), (100703, 50463), (100927, 50575), (101149, 50686), (101363, 50794), (101581, 50903), (101807, 51016), (102031, 51128), (102253, 51239), (102461, 51343), (102679, 51452), (102881, 51553), (103099, 51663), (103319, 51773), (103529, 51878), (103723, 51975), (103951, 52089), (104179, 52203), (104399, 52313), (104623, 52425), (104851, 52539), (105071, 52650), (105277, 52753), (105503, 52866), (105733, 52981), (105953, 53091), (106181, 53205), (106411, 53320), (106637, 53433), (106867, 53549), (107099, 53665), (107323, 53777), (107509, 53870), (107741, 53986), (107971, 54101), (108203, 54217), (108421, 54326), (108649, 54441), (108883, 54558), (109111, 54672), (109331, 54782), (109547, 54890), (109751, 54992), (109961, 55097), (110183, 55208), (110359, 55296), (110587, 55411), (110821, 55528), (111053, 55644), (111271, 55753), (111497, 55866), (111733, 55984), (111959, 56097), (112181, 56208), (112403, 56320), (112621, 56429), (112859, 56548), (113093, 56665), (113329, 56783), (113567, 56902), (113797, 57017), (114031, 57134), (114269, 57254), (114493, 57366), (114713, 57476), (114941, 57590), (115163, 57701), (115399, 57819), (115637, 57938), (115877, 58058), (116113, 58176), (116351, 58296), (116593, 58417), (116833, 58537), (117071, 58656), (117307, 58774), (117541, 58891), (117779, 59010), (117991, 59116), (118219, 59231), (118463, 59353), (118691, 59467), (118931, 59587), (119173, 59708), (119417, 59830), (119659, 59951), (119891, 60067), (120121, 60183), (120349, 60297), (120587, 60416), (120833, 60539), (121067, 60656), (121313, 60779), (121559, 60902), (121789, 61017), (122033, 61140), (122279, 61263), (122527, 61387), (122761, 61504), (123007, 61627), (123239, 61743), (123479, 61863), (123727, 61987), (123973, 62110), (124213, 62231), (124459, 62354), (124703, 62476), (124951, 62600), (125201, 62725), (125441, 62845), (125687, 62968), (125933, 63091), (126173, 63212), (126421, 63336), (126653, 63452), (126859, 63555), (127103, 63677), (127343, 63797), (127591, 63921), (127843, 64047), (128053, 64153), (128291, 64272), (128521, 64387), (128767, 64510), (129011, 64632), (129263, 64758), (129517, 64885), (129769, 65011), (130021, 65137), (130267, 65261), (130523, 65389), (130769, 65512), (131023, 65639), (131267, 65761), (131519, 65887), (131771, 66013), (132019, 66137), (132263, 66260), (132511, 66384), (132763, 66510), (133013, 66635), (133271, 66764), (133519, 66888), (133769, 67013), (133999, 67128), (134257, 67258), (134513, 67386), (134753, 67506), (135007, 67633), (135257, 67758), (135511, 67885), (135757, 68008), (136013, 68136), (136273, 68267), (136531, 68396), (136777, 68519), (137029, 68645), (137279, 68770), (137537, 68899), (137791, 69026), (138053, 69157), (138311, 69286), (138571, 69417), (138829, 69546), (139091, 69677), (139343, 69803), (139597, 69930), (139861, 70062), (140123, 70193), (140381, 70322), (140639, 70452), (140897, 70581), (141161, 70713), (141413, 70839), (141679, 70972), (141941, 71103), (142193, 71229), (142453, 71359), (142711, 71489), (142979, 71623), (143243, 71755), (143509, 71888), (143743, 72005), (143999, 72133), (144259, 72263), (144511, 72389), (144779, 72524), (145043, 72656), (145307, 72788), (145577, 72923), (145829, 73049), (146099, 73184), (146369, 73319), (146639, 73454), (146893, 73582), (147163, 73717), (147419, 73845), (147689, 73980), (147949, 74110), (148207, 74239), (148471, 74371), (148727, 74499), (148997, 74634), (149269, 74771), (149543, 74908), (149803, 75038), (150077, 75175), (150343, 75308), (150617, 75445), (150889, 75581), (151163, 75718), (151433, 75854), (151703, 75989), (151969, 76122), (152239, 76257), (152501, 76388), (152777, 76526), (153001, 76638), (153277, 76776), (153533, 76905), (153763, 77020), (154027, 77152), (154303, 77290), (154579, 77428), (154849, 77563), (155119, 77698), (155387, 77832), (155663, 77970), (155921, 78100), (156157, 78218), (156437, 78358), (156707, 78493), (156979, 78629), (157259, 78769), (157523, 78901), (157799, 79039), (158077, 79179), (158359, 79320), (158633, 79457), (158909, 79595), (159191, 79736), (159473, 79877), (159739, 80010), (160019, 80150), (160253, 80268), (160507, 80395), (160789, 80536), (161071, 80677), (161341, 80812), (161611, 80947), (161881, 81082), (162143, 81213), (162419, 81351), (162703, 81494), (162989, 81637), (163259, 81772), (163543, 81914), (163819, 82052), (164093, 82189), (164377, 82331), (164663, 82474), (164911, 82599), (165181, 82734), (165469, 82878), (165749, 83018), (166031, 83159), (166319, 83303), (166603, 83445), (166871, 83579), (167159, 83724), (167449, 83869), (167729, 84009), (168013, 84151), (168293, 84291), (168559, 84424), (168803, 84546), (169093, 84691), (169373, 84832), (169661, 84976), (169951, 85121), (170243, 85267), (170509, 85400), (170801, 85546), (171091, 85691), (171383, 85837), (171673, 85982), (171947, 86120), (172223, 86258), (172517, 86405), (172807, 86550), (173099, 86696), (173359, 86826), (173651, 86972), (173933, 87113), (174221, 87258), (174491, 87393), (174773, 87534), (175069, 87682), (175361, 87828), (175649, 87972), (175939, 88117), (176227, 88261), (176521, 88409), (176819, 88558), (177113, 88705), (177409, 88853), (177691, 88994), (177979, 89138), (178261, 89279), (178559, 89428), (178853, 89576), (179143, 89721), (179441, 89870), (179737, 90018), (180023, 90161), (180317, 90308), (180617, 90458), (180907, 90603), (181201, 90751), (181501, 90901), (181789, 91045), (182089, 91195), (182389, 91345), (182687, 91494), (182981, 91641), (183283, 91792), (183581, 91941), (183881, 92092), (184181, 92242), (184477, 92390), (184777, 92540), (185077, 92690), (185371, 92837), (185651, 92977), (185951, 93127), (186253, 93279), (186551, 93428), (186841, 93573), (187141, 93723), (187441, 93873), (187721, 94013), (188021, 94163), (188323, 94314), (188621, 94464), (188927, 94617), (189229, 94768), (189529, 94918), (189823, 95065), (190129, 95218), (190409, 95358), (190717, 95512), (191021, 95665), (191299, 95804), (191599, 95954), (191903, 96106), (192193, 96251), (192499, 96404), (192799, 96554), (193093, 96701), (193393, 96851), (193703, 97007), (194003, 97157), (194309, 97310), (194609, 97460), (194917, 97614), (195229, 97770), (195541, 97926), (195817, 98064), (196117, 98215), (196429, 98371), (196739, 98526), (197033, 98673), (197347, 98830), (197651, 98982), (197963, 99138), (198277, 99295), (198589, 99452), (198901, 99608), (199211, 99763), (199523, 99919), (199831, 100073), (200131, 100223), (200443, 100379), (200731, 100523), (201037, 100677), (201337, 100827), (201653, 100985), (201961, 101139), (202277, 101297), (202591, 101454), (202907, 101612), (203221, 101769), (203531, 101925), (203843, 102081), (204163, 102241), (204481, 102400), (204797, 102558), (205111, 102715), (205427, 102873), (205721, 103020), (206039, 103179), (206351, 103336), (206651, 103486), (206953, 103637), (207269, 103795), (207589, 103955), (207877, 104099), (208189, 104255), (208511, 104416), (208807, 104565), (209123, 104723), (209441, 104882), (209743, 105033), (210053, 105188), (210361, 105342), (210671, 105497), (210967, 105645), (211291, 105808), (211597, 105961), (211891, 106108), (212209, 106267), (212507, 106416), (212827, 106576), (213149, 106737), (213467, 106896), (213791, 107058), (214091, 107209), (214399, 107363), (214723, 107525), (215051, 107689), (215359, 107843), (215687, 108007), (215983, 108155), (216289, 108308), (216617, 108473), (216947, 108638), (217271, 108800), (217579, 108954), (217909, 109119), (218233, 109281), (218551, 109440), (218873, 109601), (219187, 109759), (219517, 109924), (219847, 110089), (220177, 110254), (220471, 110401), (220793, 110562), (221101, 110716), (221413, 110872), (221737, 111034), (222067, 111200), (222389, 111361), (222713, 111523), (223037, 111685), (223367, 111850), (223697, 112015), (224027, 112180), (224359, 112346), (224683, 112509), (224993, 112664), (225307, 112821), (225637, 112986), (225961, 113148), (226283, 113309), (226609, 113472), (226943, 113639), (227267, 113802), (227603, 113970), (227893, 114115), (228223, 114280), (228559, 114448), (228887, 114612), (229223, 114780), (229561, 114949), (229897, 115118), (230233, 115286), (230567, 115453), (230891, 115615), (231223, 115781), (231563, 115951), (231901, 116120), (232217, 116278), (232549, 116444), (232877, 116609), (233201, 116771), (233509, 116925), (233851, 117096), (234193, 117267), (234529, 117435), (234869, 117605), (235211, 117776), (235553, 117948), (235891, 118117), (236231, 118287), (236573, 118458), (236917, 118630), (237257, 118800), (237581, 118962), (237911, 119127), (238247, 119296), (238591, 119468), (238921, 119633), (239263, 119804), (239597, 119971), (239933, 120139), (240271, 120308), (240607, 120476), (240953, 120650), (241291, 120819), (241639, 120993), (241981, 121164), (242329, 121338), (242677, 121512), (243011, 121679), (243343, 121845), (243673, 122011), (244021, 122185), (244367, 122358), (244711, 122530), (245039, 122694), (245389, 122869), (245723, 123036), (246073, 123211), (246403, 123377), (246739, 123545), (247087, 123719), (247439, 123895), (247781, 124066), (248119, 124235), (248461, 124406), (248813, 124582), (249143, 124747), (249463, 124908), (249811, 125082), (250153, 125253), (250501, 125427), (250853, 125603), (251203, 125778), (251543, 125948), (251897, 126125), (252233, 126294), (252589, 126472), (252937, 126646), (253273, 126814), (253613, 126984), (253969, 127162), (254299, 127327), (254647, 127501), (254993, 127675), (255349, 127853), (255679, 128018), (256033, 128195), (256391, 128374), (256723, 128540), (257077, 128717), (257407, 128882), (257731, 129045), (258067, 129213), (258421, 129390), (258779, 129569), (259123, 129741), (259459, 129909), (259813, 130086), (260171, 130265), (260527, 130443), (260879, 130620), (261241, 130801), (261601, 130981), (261959, 131160), (262321, 131341), (262681, 131521), (263023, 131692), (263383, 131872), (263737, 132050), (264101, 132232), (264463, 132413), (264827, 132595), (265169, 132766), (265513, 132938), (265873, 133118), (266221, 133292), (266549, 133457), (266909, 133637), (267271, 133818), (267637, 134001), (268003, 134184), (268343, 134354), (268693, 134529), (269057, 134711), (269419, 134893), (269783, 135075), (270143, 135255), (270509, 135438), (270859, 135613), (271217, 135792), (271573, 135970), (271939, 136153), (272299, 136333), (272659, 136514), (273029, 136699), (273367, 136868), (273727, 137048), (274093, 137231), (274457, 137413), (274817, 137593), (275183, 137776), (275549, 137960), (275921, 138146), (276293, 138332), (276637, 138504), (277007, 138689), (277373, 138872), (277741, 139056), (278111, 139241), (278479, 139426), (278849, 139611), (279221, 139797), (279593, 139983), (279967, 140170), (280339, 140356), (280711, 140542), (281081, 140727), (281431, 140903), (281807, 141091), (282167, 141271), (282493, 141434), (282869, 141622), (283211, 141793), (283583, 141979), (283957, 142166), (284311, 142344), (284689, 142533), (285049, 142713), (285421, 142899), (285781, 143079), (286129, 143253), (286499, 143438), (286873, 143625), (287251, 143814), (287629, 144004), (288007, 144193), (288383, 144381), (288751, 144565), (289129, 144754), (289489, 144934), (289859, 145119), (290233, 145306), (290611, 145496), (290993, 145687), (291373, 145877), (291751, 146066), (292133, 146257), (292493, 146437), (292867, 146624), (293221, 146801), (293603, 146993), (293983, 147183), (294353, 147368), (294731, 147557), (295111, 147747), (295459, 147921), (295843, 148113), (296221, 148302), (296591, 148488), (296971, 148678), (297317, 148851), (297691, 149038), (298063, 149224), (298427, 149406), (298801, 149593), (299179, 149782), (299539, 149963), (299909, 150148), (300277, 150332), (300661, 150524), (301039, 150713), (301423, 150905), (301793, 151090), (302173, 151280), (302551, 151469), (302927, 151658), (303313, 151851), (303703, 152046), (304091, 152240), (304481, 152435), (304867, 152628), (305243, 152816), (305633, 153011), (306023, 153207), (306407, 153399), (306781, 153586), (307171, 153781), (307543, 153967), (307919, 154155), (308311, 154351), (308701, 154546), (309091, 154742), (309481, 154937), (309857, 155125), (310243, 155318), (310627, 155510), (311021, 155707), (311407, 155900), (311791, 156092), (312161, 156278), (312553, 156474), (312943, 156669), (313333, 156864), (313727, 157061), (314117, 157256), (314513, 157454), (314903, 157649), (315281, 157839), (315677, 158037), (316073, 158235), (316471, 158434), (316861, 158629), (317257, 158827), (317651, 159024), (318023, 159210), (318419, 159409), (318817, 159608), (319211, 159805), (319607, 160003), (319993, 160196), (320389, 160394), (320767, 160583), (321163, 160781), (321553, 160976), (321949, 161175), (322351, 161376), (322747, 161574), (323149, 161775), (323549, 161975), (323951, 162176), (324341, 162371), (324743, 162572), (325133, 162768), (325537, 162970), (325939, 163171), (326323, 163363), (326707, 163555), (327079, 163741), (327479, 163941), (327881, 164142), (328283, 164344), (328687, 164546), (329089, 164747), (329489, 164947), (329891, 165148), (330289, 165347), (330689, 165547), (331081, 165743), (331451, 165929), (331843, 166125), (332251, 166329), (332641, 166524), (333049, 166728), (333457, 166932), (333857, 167132), (334261, 167334), (334667, 167538), (335077, 167743), (335477, 167943), (335879, 168144), (336263, 168336), (336671, 168540), (337081, 168745), (337489, 168949), (337891, 169151), (338297, 169354), (338707, 169559), (339107, 169759), (339517, 169964), (339907, 170159), (340297, 170354), (340709, 170560), (341087, 170749), (341491, 170952), (341879, 171146), (342283, 171348), (342697, 171555), (343087, 171750), (343489, 171951), (343901, 172157), (344293, 172353), (344693, 172554), (345109, 172762), (345517, 172966), (345923, 173169), (346337, 173376), (346751, 173583), (347167, 173791), (347579, 173997), (347993, 174205), (348407, 174412), (348811, 174614), (349211, 174814), (349603, 175010), (350003, 175210), (350411, 175414), (350809, 175613), (351223, 175821), (351643, 176031), (352057, 176238), (352463, 176441), (352883, 176651), (353293, 176856), (353711, 177065), (354121, 177270), (354539, 177480), (354961, 177691), (355379, 177900), (355799, 178110), (356219, 178320), (356621, 178521), (357031, 178726), (357437, 178929), (357859, 179141), (358279, 179351), (358703, 179563), (359111, 179767), (359509, 179966), (359929, 180176), (360337, 180380), (360749, 180586), (361159, 180791), (361577, 181001), (362003, 181214), (362429, 181427), (362851, 181638), (363277, 181851), (363691, 182058), (364103, 182264), (364523, 182474), (364943, 182685), (365369, 182898), (365797, 183112), (366221, 183324), (366631, 183529), (367049, 183738), (367469, 183948), (367889, 184158), (368293, 184361), (368717, 184573), (369143, 184786), (369557, 184993), (369983, 185206), (370411, 185420), (370837, 185633), (371257, 185843), (371669, 186050), (372067, 186249), (372497, 186464), (372917, 186674), (373349, 186890), (373777, 187104), (374203, 187317), (374603, 187517), (375029, 187731), (375457, 187945), (375857, 188145), (376291, 188362), (376721, 188577), (377147, 188790), (377581, 189007), (378011, 189222), (378439, 189436), (378869, 189652), (379289, 189862), (379723, 190079), (380147, 190291), (380563, 190499), (380983, 190709), (381419, 190927), (381853, 191144), (382271, 191354), (382709, 191573), (383147, 191792), (383573, 192005), (384001, 192219), (384437, 192437), (384851, 192644), (385289, 192863), (385709, 193074), (386149, 193294), (386587, 193513), (387017, 193728), (387449, 193944), (387857, 194148), (388277, 194358), (388711, 194575), (389149, 194795), (389591, 195016), (390001, 195221), (390437, 195439), (390877, 195659), (391301, 195871), (391739, 196090), (392177, 196309), (392611, 196527), (393031, 196737), (393473, 196958), (393901, 197172), (394327, 197385), (394759, 197601), (395201, 197822), (395627, 198035), (396061, 198253), (396479, 198462), (396919, 198682), (397361, 198903), (397807, 199126), (398249, 199347), (398693, 199569), (399137, 199791), (399583, 200014)] 681 (by decide +kernel) n (by omega) s200014)

targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, line 278 at feeca055f8c6 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000360.json, merge commit feeca055f8c6.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean, sha256 9171615422a0.

import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2--h2».Context

open Filter

/-! Hole `hs2` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h3_v2__h1__h1__h1__h2__h2 : ∀ (n : ℕ),
  (229 : ℕ) ≤ n →
    n ≤ (200014 : ℕ) →
      ∃ (p : ℕ),
        Nat.Prime p ∧
          n < p ∧
            p < (2 : ℕ) * n ∧
              (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧
                ∀ α < n,
                  p < α + n →
                    (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                      ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y := by
  have lvl : ∀ B Q : ℕ, (∀ q : ℕ, q < B → 2 ≤ q → Nat.gcd q Q ≠ 1) →
      ∀ p : ℕ, 1 < p → p < B * B → Nat.gcd p Q = 1 → p.Prime := by
    intro B Q small p h1 h2 hg
    by_contra hnp
    have hq : p.minFac.Prime := Nat.minFac_prime (by omega)
    have hsq : p.minFac ^ 2 ≤ p := Nat.minFac_sq_le_self (by omega) hnp
    have hlt : p.minFac < B := by nlinarith
    apply small _ hlt hq.two_le
    have hd := Nat.gcd_dvd_gcd_of_dvd_left Q (Nat.minFac_dvd p)
    rw [hg] at hd
    exact Nat.eq_one_of_dvd_one hd
  have hP : ∀ p : ℕ, (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1))) = true → p.Prime := by
    intro p h
    simp only [Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] at h
    obtain ⟨h1, (⟨h2, h3⟩ | ⟨h2, h3⟩) | ⟨h2, h3⟩⟩ := h
    · exact lvl 7 30 (by decide +kernel) p h1 h2 h3
    · exact lvl 30 6469693230 (by decide +kernel) p h1 h2 h3
    · exact lvl 634 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 (by decide +kernel) p h1 h2 h3
  have key : ∀ t : ℕ → Bool, (∀ p : ℕ, t p = true → p.Prime) →
      ∀ (b : ℕ) (L : List (ℕ × ℕ)) (a : ℕ),
      List.foldr (fun (x : ℕ × ℕ) (f : ℕ → Bool) (lo : ℕ) =>
        (t x.1 && decide (x.2 < x.1) &&
          decide (x.1 < 2 * lo) && decide ((2 * x.2 - x.1) * (2 * x.2 - x.1) ≤ lo)) && f (x.2 + 1))
        (fun lo => decide (b < lo)) L a = true →
      ∀ n : ℕ, a ≤ n → n ≤ b → ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ (2 * n - p) * (2 * n - p) ≤ n := by
    intro t ht b L
    induction L with
    | nil =>
      intro a h n h1 h2
      simp only [List.foldr_nil, decide_eq_true_eq] at h
      omega
    | cons x L ih =>
      intro a h n h1 h2
      simp only [List.foldr_cons, Bool.and_eq_true, decide_eq_true_eq] at h
      obtain ⟨⟨⟨⟨c1, c4⟩, c5⟩, c6⟩, c7⟩ := h
      by_cases hn : n ≤ x.2
      · refine ⟨x.1, ht x.1 c1, by omega, by omega, ?_⟩
        have h3 : 2 * n - x.1 ≤ 2 * x.2 - x.1 := by omega
        exact le_trans (Nat.mul_le_mul h3 h3) (le_trans c6 h1)
      · exact ih (x.2 + 1) c7 n (by omega) h2
  have r5b_bridge : ∀ n p : ℕ, n < p → p < 2 * n → (2 * n - p) * (2 * n - p) ≤ n →
      2 * (2 * n - p) ≤ n + 2 ∧
      ∀ α : ℕ, α < n → p < α + n →
        (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
    intro n p h1 h2 h3
    generalize hk : 2 * n - p = k at *
    constructor
    · rcases Nat.lt_or_ge k 3 with h | h
      · omega
      · have : 3 * k ≤ k * k := Nat.mul_le_mul_right _ h
        omega
    · intro α hα1 hα2
      right
      intro x y hxy hd
      by_contra hc
      have h : α * y < n * x := by omega
      have α0 : 0 < α := by omega
      have hx : x * y ≤ α := Nat.le_of_dvd α0 hd
      obtain ⟨s, rfl⟩ : ∃ s, n = α + s := ⟨n - α, by omega⟩
      have hs : s < k := by omega
      have a1 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
      have a2 : α < s * x := by nlinarith
      have a3 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
      have a4 : x + 1 < s := by
        by_contra hc
        have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega)
        nlinarith
      have a5 : (s + 1) * (s + 1) ≤ k * k := Nat.mul_le_mul hs hs
      have a6 : s * x ≤ s * s := Nat.mul_le_mul_left _ (by omega)
      nlinarith
  have fin : ∀ n : ℕ, (∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ (2 * n - p) * (2 * n - p) ≤ n) →
      ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
        ∀ α : ℕ, α < n → p < α + n →
          (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
          (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
    intro n hw
    obtain ⟨p, hp, a, b, c⟩ := hw
    have br := r5b_bridge n p a b c
    exact ⟨p, hp, a, b, br.1, br.2⟩
  have r5b_cert_270 : ∃ p : ℕ, p.Prime ∧ 270 < p ∧ p < 2 * 270 ∧ 2 * (2 * 270 - p) ≤ 270 + 2 ∧
      ∀ α : ℕ, α < 270 → p < α + 270 →
        (∃ q : ℕ, q.Prime ∧ 270 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 270 * x ≤ α * y) := by
    refine ⟨523, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
    intro α h1 h2
    right
    intro x y hxy hd
    obtain ⟨m, hm⟩ := hd
    by_contra hc
    have hc' : α * y < 270 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 254 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
    have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
    have b2' : α * (x + 1) = α * x + α := by ring
    have b3 : 254 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
    have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
    have b4' : x * (x + 1) = x * x + x := by ring
    have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
    have x1 : 16 ≤ x := by omega
    have x2 : x ≤ 15 := by
      by_contra h
      have : 16 * 16 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_677 : ∃ p : ℕ, p.Prime ∧ 677 < p ∧ p < 2 * 677 ∧ 2 * (2 * 677 - p) ≤ 677 + 2 ∧
      ∀ α : ℕ, α < 677 → p < α + 677 →
        (∃ q : ℕ, q.Prime ∧ 677 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 677 * x ≤ α * y) := by
    refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
    intro α h1 h2
    right
    intro x y hxy hd
    obtain ⟨m, hm⟩ := hd
    by_contra hc
    have hc' : α * y < 677 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 651 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
    have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
    have b2' : α * (x + 1) = α * x + α := by ring
    have b3 : 651 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
    have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
    have b4' : x * (x + 1) = x * x + x := by ring
    have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
    have x1 : 26 ≤ x := by omega
    have x2 : x ≤ 25 := by
      by_contra h
      have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_678 : ∃ p : ℕ, p.Prime ∧ 678 < p ∧ p < 2 * 678 ∧ 2 * (2 * 678 - p) ≤ 678 + 2 ∧
      ∀ α : ℕ, α < 678 → p < α + 678 →
        (∃ q : ℕ, q.Prime ∧ 678 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 678 * x ≤ α * y) := by
    refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
    intro α h1 h2
    by_cases e650 : α = 650
    · left
      exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
    right
    intro x y hxy hd
    obtain ⟨m, hm⟩ := hd
    by_contra hc
    have hc' : α * y < 678 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 650 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
    have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
    have b2' : α * (x + 1) = α * x + α := by ring
    have b3 : 650 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
    have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
    have b4' : x * (x + 1) = x * x + x := by ring
    have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
    have x1 : 24 ≤ x := by omega
    have x2 : x ≤ 25 := by
      by_contra h
      have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 25 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 26 := by omega
      interval_cases y <;> omega
  have r5b_cert_679 : ∃ p : ℕ, p.Prime ∧ 679 < p ∧ p < 2 * 679 ∧ 2 * (2 * 679 - p) ≤ 679 + 2 ∧
      ∀ α : ℕ, α < 679 → p < α + 679 →
        (∃ q : ℕ, q.Prime ∧ 679 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 679 * x ≤ α * y) := by
    refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
    intro α h1 h2
    by_cases e650 : α = 650
    · left
      exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
    right
    intro x y hxy hd
    obtain ⟨m, hm⟩ := hd
    by_contra hc
    have hc' : α * y < 679 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 649 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
    have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
    have b2' : α * (x + 1) = α * x + α := by ring
    have b3 : 649 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
    have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
    have b4' : x * (x + 1) = x * x + x := by ring
    have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
    have x1 : 22 ≤ x := by omega
    have x2 : x ≤ 25 := by
      by_contra h
      have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 23 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 24 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 25 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 26 := by omega
      interval_cases y <;> omega
  have r5b_cert_680 : ∃ p : ℕ, p.Prime ∧ 680 < p ∧ p < 2 * 680 ∧ 2 * (2 * 680 - p) ≤ 680 + 2 ∧
      ∀ α : ℕ, α < 680 → p < α + 680 →
        (∃ q : ℕ, q.Prime ∧ 680 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 680 * x ≤ α * y) := by
    refine ⟨1327, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩
    intro α h1 h2
    by_cases e650 : α = 650
    · left
      exact ⟨677, by norm_num, by norm_num, by subst e650; norm_num⟩
    right
    intro x y hxy hd
    obtain ⟨m, hm⟩ := hd
    by_contra hc
    have hc' : α * y < 680 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 648 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
    have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
    have b2' : α * (x + 1) = α * x + α := by ring
    have b3 : 648 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
    have b4 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
    have b4' : x * (x + 1) = x * x + x := by ring
    have b5 : x * y ≤ x * y * m := Nat.le_mul_of_pos_right _ m0
    have x1 : 21 ≤ x := by omega
    have x2 : x ≤ 25 := by
      by_contra h
      have : 26 * 26 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 22 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 23 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 24 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 25 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 26 := by omega
      interval_cases y <;> omega
  intro n hl hh
  by_cases e270 : n = 270
  · subst e270
    exact r5b_cert_270
  by_cases e677 : n = 677
  · subst e677
    exact r5b_cert_677
  by_cases e678 : n = 678
  · subst e678
    exact r5b_cert_678
  by_cases e679 : n = 679
  · subst e679
    exact r5b_cert_679
  by_cases e680 : n = 680
  · subst e680
    exact r5b_cert_680
  by_cases s269 : n ≤ 269
  · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 269 [(457, 236), (467, 241), (479, 247), (491, 253), (503, 259), (509, 262), (523, 269)] 229 (by decide +kernel) n (by omega) s269)
  by_cases s676 : n ≤ 676
  · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 676 [(541, 278), (557, 286), (571, 293), (587, 302), (601, 309), (619, 318), (631, 324), (647, 332), (661, 339), (677, 347), (691, 354), (709, 363), (727, 373), (743, 381), (761, 390), (773, 396), (787, 403), (797, 408), (811, 415), (829, 424), (839, 429), (859, 439), (877, 448), (887, 454), (907, 464), (929, 475), (947, 484), (967, 494), (983, 502), (997, 509), (1019, 520), (1039, 530), (1061, 542), (1069, 546), (1093, 558), (1117, 570), (1129, 576), (1153, 588), (1171, 597), (1193, 608), (1217, 620), (1237, 630), (1259, 642), (1283, 654), (1307, 666), (1327, 676)] 271 (by decide +kernel) n (by omega) s676)
  by_cases s200014 : n ≤ 200014
  · exact fin n (key (fun p => (decide (1 < p) && (decide (p < 49) && decide (Nat.gcd p 30 = 1) || decide (p < 900) && decide (Nat.gcd p 6469693230 = 1) || decide (p < 401956) && decide (Nat.gcd p 1702638442551072365617326631534342245041465988544372563961893321511809758012320472936554398121035062403896046404654753749168137340872368042807946221263167725872661266685741122100016726950864909508767802965271369340352229248204502328104750019252611639587225304330 = 1)))) hP 200014 [(1361, 693), (1381, 703), (1399, 712), (1423, 724), (1447, 736), (1471, 749), (1499, 763), (1523, 775), (1549, 788), (1571, 799), (1597, 812), (1621, 824), (1637, 832), (1663, 845), (1669, 849), (1699, 864), (1723, 876), (1753, 891), (1783, 906), (1811, 920), (1831, 930), (1861, 945), (1889, 959), (1913, 971), (1933, 982), (1951, 991), (1979, 1005), (2011, 1021), (2039, 1035), (2069, 1050), (2099, 1065), (2131, 1081), (2161, 1096), (2179, 1106), (2213, 1123), (2243, 1138), (2273, 1153), (2297, 1165), (2311, 1172), (2341, 1187), (2371, 1202), (2399, 1216), (2423, 1228), (2447, 1241), (2477, 1256), (2503, 1269), (2539, 1287), (2557, 1296), (2593, 1314), (2621, 1328), (2657, 1346), (2693, 1364), (2729, 1382), (2753, 1395), (2791, 1414), (2819, 1428), (2857, 1447), (2887, 1462), (2917, 1477), (2953, 1495), (2971, 1504), (3001, 1519), (3037, 1537), (3067, 1553), (3089, 1564), (3121, 1580), (3137, 1588), (3169, 1604), (3209, 1624), (3229, 1634), (3259, 1649), (3299, 1669), (3331, 1685), (3371, 1706), (3413, 1727), (3449, 1745), (3491, 1766), (3533, 1787), (3571, 1806), (3613, 1827), (3643, 1842), (3677, 1859), (3719, 1881), (3761, 1902), (3803, 1923), (3847, 1945), (3889, 1966), (3931, 1987), (3967, 2005), (4007, 2025), (4051, 2048), (4093, 2069), (4139, 2092), (4177, 2111), (4219, 2132), (4261, 2153), (4297, 2171), (4339, 2192), (4373, 2209), (4409, 2228), (4457, 2252), (4493, 2270), (4523, 2285), (4567, 2307), (4603, 2325), (4651, 2349), (4691, 2369), (4733, 2390), (4759, 2403), (4801, 2425), (4831, 2440), (4877, 2463), (4919, 2484), (4969, 2509), (5011, 2530), (5059, 2554), (5107, 2578), (5153, 2601), (5197, 2624), (5237, 2644), (5281, 2666), (5333, 2692), (5381, 2716), (5431, 2741), (5483, 2767), (5531, 2791), (5581, 2816), (5623, 2838), (5669, 2861), (5717, 2885), (5749, 2901), (5801, 2927), (5851, 2952), (5903, 2978), (5953, 3003), (6007, 3030), (6053, 3054), (6101, 3078), (6151, 3103), (6203, 3129), (6257, 3156), (6311, 3183), (6367, 3211), (6421, 3238), (6473, 3264), (6529, 3293), (6581, 3319), (6637, 3347), (6691, 3374), (6737, 3397), (6793, 3425), (6841, 3449), (6899, 3478), (6949, 3503), (7001, 3530), (7057, 3558), (7109, 3584), (7159, 3609), (7219, 3639), (7253, 3656), (7309, 3684), (7369, 3714), (7417, 3738), (7477, 3769), (7537, 3799), (7591, 3826), (7649, 3855), (7703, 3882), (7759, 3910), (7817, 3939), (7879, 3970), (7937, 4000), (7993, 4028), (8053, 4058), (8117, 4090), (8179, 4121), (8243, 4153), (8297, 4180), (8353, 4208), (8389, 4226), (8447, 4256), (8513, 4289), (8573, 4319), (8629, 4347), (8693, 4379), (8753, 4409), (8819, 4442), (8867, 4466), (8933, 4499), (8999, 4533), (9067, 4567), (9133, 4600), (9199, 4633), (9257, 4662), (9323, 4695), (9391, 4729), (9439, 4753), (9497, 4782), (9551, 4810), (9619, 4844), (9689, 4879), (9749, 4909), (9817, 4943), (9887, 4978), (9949, 5009), (10009, 5039), (10079, 5074), (10141, 5106), (10211, 5141), (10273, 5172), (10343, 5207), (10399, 5235), (10463, 5267), (10531, 5301), (10601, 5336), (10667, 5370), (10739, 5406), (10799, 5436), (10867, 5470), (10939, 5506), (11003, 5538), (11071, 5572), (11131, 5602), (11197, 5635), (11261, 5668), (11329, 5702), (11399, 5737), (11471, 5773), (11527, 5801), (11597, 5836), (11657, 5866), (11731, 5903), (11807, 5941), (11867, 5972), (11941, 6009), (12011, 6044), (12073, 6075), (12149, 6113), (12227, 6152), (12301, 6189), (12379, 6228), (12457, 6267), (12527, 6303), (12601, 6340), (12671, 6375), (12743, 6411), (12823, 6451), (12899, 6489), (12979, 6529), (13049, 6564), (13127, 6604), (13187, 6634), (13267, 6674), (13339, 6710), (13421, 6751), (13499, 6790), (13577, 6829), (13649, 6865), (13729, 6905), (13807, 6945), (13883, 6983), (13967, 7025), (14051, 7067), (14107, 7095), (14177, 7130), (14251, 7167), (14327, 7205), (14411, 7247), (14489, 7287), (14563, 7324), (14639, 7362), (14723, 7404), (14797, 7441), (14879, 7482), (14957, 7521), (15031, 7558), (15107, 7596), (15193, 7640), (15277, 7682), (15361, 7724), (15443, 7765), (15527, 7807), (15607, 7847), (15683, 7885), (15767, 7927), (15823, 7956), (15913, 8001), (16001, 8045), (16091, 8090), (16141, 8115), (16231, 8160), (16319, 8204), (16381, 8235), (16453, 8271), (16529, 8309), (16619, 8355), (16703, 8397), (16787, 8439), (16879, 8485), (16963, 8527), (17053, 8572), (17137, 8614), (17209, 8650), (17299, 8696), (17393, 8743), (17483, 8788), (17573, 8833), (17659, 8876), (17749, 8921), (17839, 8966), (17929, 9011), (18013, 9053), (18097, 9096), (18191, 9143), (18287, 9191), (18379, 9237), (18461, 9278), (18553, 9324), (18637, 9366), (18731, 9413), (18803, 9450), (18899, 9498), (18979, 9538), (19073, 9585), (19163, 9630), (19259, 9678), (19333, 9715), (19429, 9763), (19507, 9802), (19603, 9851), (19699, 9899), (19793, 9946), (19891, 9995), (19991, 10045), (20089, 10094), (20183, 10141), (20269, 10184), (20369, 10234), (20443, 10272), (20543, 10322), (20641, 10371), (20743, 10422), (20809, 10455), (20903, 10502), (21001, 10551), (21101, 10601), (21193, 10647), (21283, 10693), (21383, 10743), (21487, 10795), (21589, 10846), (21683, 10893), (21787, 10945), (21881, 10992), (21977, 11040), (22079, 11092), (22171, 11138), (22277, 11191), (22381, 11243), (22483, 11294), (22573, 11339), (22679, 11392), (22783, 11444), (22877, 11491), (22973, 11540), (23081, 11594), (23189, 11648), (23297, 11702), (23399, 11753), (23497, 11802), (23603, 11855), (23689, 11898), (23789, 11949), (23899, 12004), (24007, 12058), (24113, 12111), (24223, 12166), (24329, 12219), (24439, 12274), (24547, 12328), (24631, 12371), (24733, 12422), (24841, 12476), (24953, 12532), (25057, 12584), (25169, 12640), (25261, 12686), (25373, 12742), (25471, 12791), (25583, 12848), (25693, 12903), (25801, 12957), (25913, 13013), (26021, 13067), (26119, 13116), (26227, 13170), (26339, 13226), (26449, 13282), (26561, 13338), (26669, 13392), (26783, 13449), (26893, 13504), (26993, 13554), (27109, 13612), (27211, 13663), (27299, 13707), (27409, 13763), (27527, 13822), (27631, 13874), (27749, 13933), (27851, 13984), (27967, 14042), (28081, 14099), (28183, 14150), (28297, 14207), (28411, 14265), (28517, 14318), (28631, 14375), (28751, 14435), (28871, 14495), (28979, 14549), (29077, 14598), (29191, 14655), (29311, 14716), (29429, 14775), (29537, 14829), (29641, 14881), (29761, 14941), (29881, 15001), (29989, 15055), (30109, 15115), (30223, 15172), (30341, 15232), (30449, 15286), (30559, 15341), (30677, 15400), (30781, 15452), (30893, 15508), (31013, 15568), (31123, 15623), (31247, 15685), (31357, 15741), (31481, 15803), (31607, 15866), (31729, 15927), (31849, 15987), (31973, 16049), (32099, 16112), (32213, 16169), (32327, 16227), (32443, 16285), (32569, 16348), (32693, 16410), (32803, 16465), (32917, 16522), (33037, 16582), (33161, 16644), (33289, 16709), (33413, 16771), (33533, 16831), (33647, 16888), (33773, 16951), (33893, 17011), (34019, 17074), (34147, 17138), (34273, 17201), (34403, 17267), (34519, 17325), (34651, 17391), (34781, 17456), (34913, 17522), (35027, 17579), (35159, 17645), (35291, 17711), (35423, 17778), (35543, 17838), (35677, 17905), (35809, 17971), (35933, 18033), (36067, 18100), (36191, 18162), (36319, 18226), (36451, 18293), (36587, 18361), (36721, 18428), (36857, 18496), (36979, 18557), (37097, 18616), (37223, 18679), (37357, 18746), (37493, 18814), (37619, 18878), (37747, 18942), (37879, 19008), (38011, 19074), (38149, 19143), (38287, 19212), (38393, 19265), (38501, 19319), (38639, 19388), (38767, 19453), (38903, 19521), (39043, 19591), (39181, 19660), (39317, 19728), (39451, 19795), (39581, 19860), (39719, 19929), (39857, 19999), (39989, 20065), (40129, 20135), (40253, 20197), (40387, 20264), (40529, 20335), (40639, 20390), (40771, 20456), (40903, 20523), (41047, 20595), (41189, 20666), (41333, 20738), (41467, 20805), (41611, 20877), (41737, 20940), (41879, 21011), (42023, 21083), (42157, 21151), (42299, 21222), (42443, 21294), (42589, 21367), (42727, 21436), (42863, 21504), (43003, 21574), (43133, 21639), (43271, 21709), (43411, 21779), (43543, 21845), (43691, 21919), (43801, 21974), (43943, 22045), (44089, 22118), (44221, 22184), (44357, 22252), (44501, 22325), (44651, 22400), (44797, 22473), (44939, 22544), (45083, 22616), (45233, 22691), (45377, 22763), (45523, 22836), (45673, 22912), (45823, 22987), (45971, 23061), (46103, 23127), (46237, 23194), (46381, 23266), (46523, 23337), (46663, 23407), (46811, 23481), (46957, 23555), (47111, 23632), (47251, 23702), (47389, 23771), (47543, 23848), (47681, 23917), (47819, 23986), (47969, 24061), (48121, 24138), (48271, 24213), (48413, 24284), (48563, 24359), (48679, 24417), (48823, 24489), (48973, 24564), (49123, 24639), (49279, 24717), (49433, 24795), (49559, 24858), (49711, 24934), (49853, 25005), (49999, 25078), (50153, 25155), (50311, 25234), (50461, 25309), (50599, 25379), (50753, 25456), (50909, 25534), (51061, 25610), (51217, 25688), (51361, 25760), (51521, 25840), (51679, 25919), (51839, 25999), (51991, 26076), (52153, 26157), (52313, 26237), (52457, 26309), (52609, 26385), (52769, 26465), (52919, 26540), (53077, 26619), (53239, 26701), (53401, 26782), (53551, 26857), (53699, 26931), (53861, 27012), (54013, 27088), (54167, 27165), (54331, 27247), (54493, 27329), (54647, 27406), (54799, 27482), (54959, 27562), (55117, 27641), (55259, 27712), (55411, 27788), (55547, 27856), (55711, 27938), (55871, 28019), (56039, 28103), (56207, 28187), (56369, 28268), (56533, 28350), (56701, 28434), (56857, 28512), (56999, 28583), (57163, 28666), (57331, 28750), (57493, 28831), (57653, 28911), (57809, 28989), (57977, 29073), (58147, 29158), (58313, 29241), (58481, 29326), (58631, 29401), (58789, 29480), (58943, 29557), (59113, 29642), (59281, 29726), (59453, 29812), (59621, 29896), (59791, 29981), (59957, 30065), (60127, 30150), (60293, 30233), (60457, 30315), (60631, 30402), (60793, 30483), (60961, 30567), (61129, 30651), (61297, 30736), (61471, 30823), (61643, 30909), (61819, 30997), (61991, 31083), (62143, 31159), (62311, 31243), (62483, 31329), (62659, 31418), (62827, 31502), (62989, 31583), (63149, 31663), (63317, 31747), (63493, 31835), (63671, 31924), (63841, 32009), (64019, 32098), (64189, 32184), (64333, 32256), (64513, 32346), (64693, 32436), (64871, 32525), (65033, 32606), (65213, 32696), (65393, 32786), (65563, 32872), (65731, 32956), (65899, 33040), (66071, 33126), (66239, 33210), (66413, 33297), (66593, 33387), (66763, 33472), (66943, 33562), (67121, 33652), (67289, 33736), (67453, 33818), (67631, 33907), (67807, 33995), (67987, 34085), (68171, 34177), (68351, 34267), (68531, 34358), (68713, 34449), (68899, 34542), (69073, 34629), (69259, 34722), (69439, 34812), (69623, 34904), (69809, 34997), (69991, 35089), (70177, 35182), (70351, 35269), (70537, 35362), (70717, 35452), (70901, 35544), (71089, 35638), (71263, 35725), (71443, 35816), (71633, 35911), (71821, 36005), (71999, 36094), (72173, 36181), (72353, 36271), (72533, 36361), (72719, 36454), (72907, 36548), (73091, 36641), (73277, 36734), (73459, 36825), (73651, 36921), (73823, 37007), (73999, 37095), (74189, 37190), (74381, 37286), (74573, 37383), (74761, 37477), (74941, 37567), (75133, 37663), (75323, 37758), (75511, 37852), (75703, 37948), (75883, 38038), (76039, 38117), (76231, 38213), (76423, 38309), (76607, 38401), (76801, 38498), (76991, 38593), (77171, 38683), (77359, 38777), (77551, 38873), (77747, 38972), (77933, 39065), (78121, 39159), (78317, 39257), (78511, 39354), (78707, 39452), (78901, 39549), (79087, 39642), (79283, 39741), (79481, 39840), (79669, 39934), (79867, 40033), (80051, 40125), (80251, 40225), (80449, 40324), (80629, 40414), (80819, 40510), (81019, 40610), (81203, 40702), (81401, 40801), (81569, 40885), (81769, 40985), (81971, 41086), (82171, 41186), (82373, 41287), (82571, 41387), (82763, 41483), (82963, 41583), (83137, 41670), (83341, 41772), (83537, 41870), (83737, 41970), (83939, 42071), (84143, 42174), (84349, 42277), (84551, 42378), (84751, 42478), (84947, 42576), (85147, 42676), (85333, 42769), (85531, 42868), (85733, 42970), (85933, 43070), (86137, 43172), (86341, 43274), (86539, 43373), (86743, 43475), (86951, 43579), (87151, 43679), (87359, 43783), (87559, 43884), (87767, 43988), (87977, 44093), (88177, 44193), (88379, 44294), (88589, 44399), (88799, 44504), (89009, 44609), (89213, 44712), (89417, 44814), (89627, 44919), (89839, 45025), (90031, 45121), (90239, 45225), (90439, 45325), (90647, 45429), (90847, 45530), (91033, 45623), (91243, 45728), (91457, 45835), (91639, 45926), (91841, 46027), (92051, 46132), (92251, 46232), (92461, 46338), (92671, 46443), (92867, 46541), (93083, 46649), (93287, 46751), (93503, 46859), (93719, 46967), (93923, 47069), (94121, 47168), (94331, 47274), (94547, 47382), (94747, 47482), (94961, 47589), (95177, 47697), (95393, 47805), (95603, 47910), (95819, 48018), (96017, 48118), (96233, 48226), (96451, 48335), (96671, 48445), (96857, 48538), (97073, 48646), (97283, 48751), (97501, 48860), (97711, 48966), (97931, 49076), (98143, 49182), (98347, 49284), (98563, 49392), (98779, 49500), (98999, 49610), (99191, 49706), (99409, 49815), (99623, 49923), (99839, 50031), (100057, 50140), (100279, 50251), (100501, 50362), (100703, 50463), (100927, 50575), (101149, 50686), (101363, 50794), (101581, 50903), (101807, 51016), (102031, 51128), (102253, 51239), (102461, 51343), (102679, 51452), (102881, 51553), (103099, 51663), (103319, 51773), (103529, 51878), (103723, 51975), (103951, 52089), (104179, 52203), (104399, 52313), (104623, 52425), (104851, 52539), (105071, 52650), (105277, 52753), (105503, 52866), (105733, 52981), (105953, 53091), (106181, 53205), (106411, 53320), (106637, 53433), (106867, 53549), (107099, 53665), (107323, 53777), (107509, 53870), (107741, 53986), (107971, 54101), (108203, 54217), (108421, 54326), (108649, 54441), (108883, 54558), (109111, 54672), (109331, 54782), (109547, 54890), (109751, 54992), (109961, 55097), (110183, 55208), (110359, 55296), (110587, 55411), (110821, 55528), (111053, 55644), (111271, 55753), (111497, 55866), (111733, 55984), (111959, 56097), (112181, 56208), (112403, 56320), (112621, 56429), (112859, 56548), (113093, 56665), (113329, 56783), (113567, 56902), (113797, 57017), (114031, 57134), (114269, 57254), (114493, 57366), (114713, 57476), (114941, 57590), (115163, 57701), (115399, 57819), (115637, 57938), (115877, 58058), (116113, 58176), (116351, 58296), (116593, 58417), (116833, 58537), (117071, 58656), (117307, 58774), (117541, 58891), (117779, 59010), (117991, 59116), (118219, 59231), (118463, 59353), (118691, 59467), (118931, 59587), (119173, 59708), (119417, 59830), (119659, 59951), (119891, 60067), (120121, 60183), (120349, 60297), (120587, 60416), (120833, 60539), (121067, 60656), (121313, 60779), (121559, 60902), (121789, 61017), (122033, 61140), (122279, 61263), (122527, 61387), (122761, 61504), (123007, 61627), (123239, 61743), (123479, 61863), (123727, 61987), (123973, 62110), (124213, 62231), (124459, 62354), (124703, 62476), (124951, 62600), (125201, 62725), (125441, 62845), (125687, 62968), (125933, 63091), (126173, 63212), (126421, 63336), (126653, 63452), (126859, 63555), (127103, 63677), (127343, 63797), (127591, 63921), (127843, 64047), (128053, 64153), (128291, 64272), (128521, 64387), (128767, 64510), (129011, 64632), (129263, 64758), (129517, 64885), (129769, 65011), (130021, 65137), (130267, 65261), (130523, 65389), (130769, 65512), (131023, 65639), (131267, 65761), (131519, 65887), (131771, 66013), (132019, 66137), (132263, 66260), (132511, 66384), (132763, 66510), (133013, 66635), (133271, 66764), (133519, 66888), (133769, 67013), (133999, 67128), (134257, 67258), (134513, 67386), (134753, 67506), (135007, 67633), (135257, 67758), (135511, 67885), (135757, 68008), (136013, 68136), (136273, 68267), (136531, 68396), (136777, 68519), (137029, 68645), (137279, 68770), (137537, 68899), (137791, 69026), (138053, 69157), (138311, 69286), (138571, 69417), (138829, 69546), (139091, 69677), (139343, 69803), (139597, 69930), (139861, 70062), (140123, 70193), (140381, 70322), (140639, 70452), (140897, 70581), (141161, 70713), (141413, 70839), (141679, 70972), (141941, 71103), (142193, 71229), (142453, 71359), (142711, 71489), (142979, 71623), (143243, 71755), (143509, 71888), (143743, 72005), (143999, 72133), (144259, 72263), (144511, 72389), (144779, 72524), (145043, 72656), (145307, 72788), (145577, 72923), (145829, 73049), (146099, 73184), (146369, 73319), (146639, 73454), (146893, 73582), (147163, 73717), (147419, 73845), (147689, 73980), (147949, 74110), (148207, 74239), (148471, 74371), (148727, 74499), (148997, 74634), (149269, 74771), (149543, 74908), (149803, 75038), (150077, 75175), (150343, 75308), (150617, 75445), (150889, 75581), (151163, 75718), (151433, 75854), (151703, 75989), (151969, 76122), (152239, 76257), (152501, 76388), (152777, 76526), (153001, 76638), (153277, 76776), (153533, 76905), (153763, 77020), (154027, 77152), (154303, 77290), (154579, 77428), (154849, 77563), (155119, 77698), (155387, 77832), (155663, 77970), (155921, 78100), (156157, 78218), (156437, 78358), (156707, 78493), (156979, 78629), (157259, 78769), (157523, 78901), (157799, 79039), (158077, 79179), (158359, 79320), (158633, 79457), (158909, 79595), (159191, 79736), (159473, 79877), (159739, 80010), (160019, 80150), (160253, 80268), (160507, 80395), (160789, 80536), (161071, 80677), (161341, 80812), (161611, 80947), (161881, 81082), (162143, 81213), (162419, 81351), (162703, 81494), (162989, 81637), (163259, 81772), (163543, 81914), (163819, 82052), (164093, 82189), (164377, 82331), (164663, 82474), (164911, 82599), (165181, 82734), (165469, 82878), (165749, 83018), (166031, 83159), (166319, 83303), (166603, 83445), (166871, 83579), (167159, 83724), (167449, 83869), (167729, 84009), (168013, 84151), (168293, 84291), (168559, 84424), (168803, 84546), (169093, 84691), (169373, 84832), (169661, 84976), (169951, 85121), (170243, 85267), (170509, 85400), (170801, 85546), (171091, 85691), (171383, 85837), (171673, 85982), (171947, 86120), (172223, 86258), (172517, 86405), (172807, 86550), (173099, 86696), (173359, 86826), (173651, 86972), (173933, 87113), (174221, 87258), (174491, 87393), (174773, 87534), (175069, 87682), (175361, 87828), (175649, 87972), (175939, 88117), (176227, 88261), (176521, 88409), (176819, 88558), (177113, 88705), (177409, 88853), (177691, 88994), (177979, 89138), (178261, 89279), (178559, 89428), (178853, 89576), (179143, 89721), (179441, 89870), (179737, 90018), (180023, 90161), (180317, 90308), (180617, 90458), (180907, 90603), (181201, 90751), (181501, 90901), (181789, 91045), (182089, 91195), (182389, 91345), (182687, 91494), (182981, 91641), (183283, 91792), (183581, 91941), (183881, 92092), (184181, 92242), (184477, 92390), (184777, 92540), (185077, 92690), (185371, 92837), (185651, 92977), (185951, 93127), (186253, 93279), (186551, 93428), (186841, 93573), (187141, 93723), (187441, 93873), (187721, 94013), (188021, 94163), (188323, 94314), (188621, 94464), (188927, 94617), (189229, 94768), (189529, 94918), (189823, 95065), (190129, 95218), (190409, 95358), (190717, 95512), (191021, 95665), (191299, 95804), (191599, 95954), (191903, 96106), (192193, 96251), (192499, 96404), (192799, 96554), (193093, 96701), (193393, 96851), (193703, 97007), (194003, 97157), (194309, 97310), (194609, 97460), (194917, 97614), (195229, 97770), (195541, 97926), (195817, 98064), (196117, 98215), (196429, 98371), (196739, 98526), (197033, 98673), (197347, 98830), (197651, 98982), (197963, 99138), (198277, 99295), (198589, 99452), (198901, 99608), (199211, 99763), (199523, 99919), (199831, 100073), (200131, 100223), (200443, 100379), (200731, 100523), (201037, 100677), (201337, 100827), (201653, 100985), (201961, 101139), (202277, 101297), (202591, 101454), (202907, 101612), (203221, 101769), (203531, 101925), (203843, 102081), (204163, 102241), (204481, 102400), (204797, 102558), (205111, 102715), (205427, 102873), (205721, 103020), (206039, 103179), (206351, 103336), (206651, 103486), (206953, 103637), (207269, 103795), (207589, 103955), (207877, 104099), (208189, 104255), (208511, 104416), (208807, 104565), (209123, 104723), (209441, 104882), (209743, 105033), (210053, 105188), (210361, 105342), (210671, 105497), (210967, 105645), (211291, 105808), (211597, 105961), (211891, 106108), (212209, 106267), (212507, 106416), (212827, 106576), (213149, 106737), (213467, 106896), (213791, 107058), (214091, 107209), (214399, 107363), (214723, 107525), (215051, 107689), (215359, 107843), (215687, 108007), (215983, 108155), (216289, 108308), (216617, 108473), (216947, 108638), (217271, 108800), (217579, 108954), (217909, 109119), (218233, 109281), (218551, 109440), (218873, 109601), (219187, 109759), (219517, 109924), (219847, 110089), (220177, 110254), (220471, 110401), (220793, 110562), (221101, 110716), (221413, 110872), (221737, 111034), (222067, 111200), (222389, 111361), (222713, 111523), (223037, 111685), (223367, 111850), (223697, 112015), (224027, 112180), (224359, 112346), (224683, 112509), (224993, 112664), (225307, 112821), (225637, 112986), (225961, 113148), (226283, 113309), (226609, 113472), (226943, 113639), (227267, 113802), (227603, 113970), (227893, 114115), (228223, 114280), (228559, 114448), (228887, 114612), (229223, 114780), (229561, 114949), (229897, 115118), (230233, 115286), (230567, 115453), (230891, 115615), (231223, 115781), (231563, 115951), (231901, 116120), (232217, 116278), (232549, 116444), (232877, 116609), (233201, 116771), (233509, 116925), (233851, 117096), (234193, 117267), (234529, 117435), (234869, 117605), (235211, 117776), (235553, 117948), (235891, 118117), (236231, 118287), (236573, 118458), (236917, 118630), (237257, 118800), (237581, 118962), (237911, 119127), (238247, 119296), (238591, 119468), (238921, 119633), (239263, 119804), (239597, 119971), (239933, 120139), (240271, 120308), (240607, 120476), (240953, 120650), (241291, 120819), (241639, 120993), (241981, 121164), (242329, 121338), (242677, 121512), (243011, 121679), (243343, 121845), (243673, 122011), (244021, 122185), (244367, 122358), (244711, 122530), (245039, 122694), (245389, 122869), (245723, 123036), (246073, 123211), (246403, 123377), (246739, 123545), (247087, 123719), (247439, 123895), (247781, 124066), (248119, 124235), (248461, 124406), (248813, 124582), (249143, 124747), (249463, 124908), (249811, 125082), (250153, 125253), (250501, 125427), (250853, 125603), (251203, 125778), (251543, 125948), (251897, 126125), (252233, 126294), (252589, 126472), (252937, 126646), (253273, 126814), (253613, 126984), (253969, 127162), (254299, 127327), (254647, 127501), (254993, 127675), (255349, 127853), (255679, 128018), (256033, 128195), (256391, 128374), (256723, 128540), (257077, 128717), (257407, 128882), (257731, 129045), (258067, 129213), (258421, 129390), (258779, 129569), (259123, 129741), (259459, 129909), (259813, 130086), (260171, 130265), (260527, 130443), (260879, 130620), (261241, 130801), (261601, 130981), (261959, 131160), (262321, 131341), (262681, 131521), (263023, 131692), (263383, 131872), (263737, 132050), (264101, 132232), (264463, 132413), (264827, 132595), (265169, 132766), (265513, 132938), (265873, 133118), (266221, 133292), (266549, 133457), (266909, 133637), (267271, 133818), (267637, 134001), (268003, 134184), (268343, 134354), (268693, 134529), (269057, 134711), (269419, 134893), (269783, 135075), (270143, 135255), (270509, 135438), (270859, 135613), (271217, 135792), (271573, 135970), (271939, 136153), (272299, 136333), (272659, 136514), (273029, 136699), (273367, 136868), (273727, 137048), (274093, 137231), (274457, 137413), (274817, 137593), (275183, 137776), (275549, 137960), (275921, 138146), (276293, 138332), (276637, 138504), (277007, 138689), (277373, 138872), (277741, 139056), (278111, 139241), (278479, 139426), (278849, 139611), (279221, 139797), (279593, 139983), (279967, 140170), (280339, 140356), (280711, 140542), (281081, 140727), (281431, 140903), (281807, 141091), (282167, 141271), (282493, 141434), (282869, 141622), (283211, 141793), (283583, 141979), (283957, 142166), (284311, 142344), (284689, 142533), (285049, 142713), (285421, 142899), (285781, 143079), (286129, 143253), (286499, 143438), (286873, 143625), (287251, 143814), (287629, 144004), (288007, 144193), (288383, 144381), (288751, 144565), (289129, 144754), (289489, 144934), (289859, 145119), (290233, 145306), (290611, 145496), (290993, 145687), (291373, 145877), (291751, 146066), (292133, 146257), (292493, 146437), (292867, 146624), (293221, 146801), (293603, 146993), (293983, 147183), (294353, 147368), (294731, 147557), (295111, 147747), (295459, 147921), (295843, 148113), (296221, 148302), (296591, 148488), (296971, 148678), (297317, 148851), (297691, 149038), (298063, 149224), (298427, 149406), (298801, 149593), (299179, 149782), (299539, 149963), (299909, 150148), (300277, 150332), (300661, 150524), (301039, 150713), (301423, 150905), (301793, 151090), (302173, 151280), (302551, 151469), (302927, 151658), (303313, 151851), (303703, 152046), (304091, 152240), (304481, 152435), (304867, 152628), (305243, 152816), (305633, 153011), (306023, 153207), (306407, 153399), (306781, 153586), (307171, 153781), (307543, 153967), (307919, 154155), (308311, 154351), (308701, 154546), (309091, 154742), (309481, 154937), (309857, 155125), (310243, 155318), (310627, 155510), (311021, 155707), (311407, 155900), (311791, 156092), (312161, 156278), (312553, 156474), (312943, 156669), (313333, 156864), (313727, 157061), (314117, 157256), (314513, 157454), (314903, 157649), (315281, 157839), (315677, 158037), (316073, 158235), (316471, 158434), (316861, 158629), (317257, 158827), (317651, 159024), (318023, 159210), (318419, 159409), (318817, 159608), (319211, 159805), (319607, 160003), (319993, 160196), (320389, 160394), (320767, 160583), (321163, 160781), (321553, 160976), (321949, 161175), (322351, 161376), (322747, 161574), (323149, 161775), (323549, 161975), (323951, 162176), (324341, 162371), (324743, 162572), (325133, 162768), (325537, 162970), (325939, 163171), (326323, 163363), (326707, 163555), (327079, 163741), (327479, 163941), (327881, 164142), (328283, 164344), (328687, 164546), (329089, 164747), (329489, 164947), (329891, 165148), (330289, 165347), (330689, 165547), (331081, 165743), (331451, 165929), (331843, 166125), (332251, 166329), (332641, 166524), (333049, 166728), (333457, 166932), (333857, 167132), (334261, 167334), (334667, 167538), (335077, 167743), (335477, 167943), (335879, 168144), (336263, 168336), (336671, 168540), (337081, 168745), (337489, 168949), (337891, 169151), (338297, 169354), (338707, 169559), (339107, 169759), (339517, 169964), (339907, 170159), (340297, 170354), (340709, 170560), (341087, 170749), (341491, 170952), (341879, 171146), (342283, 171348), (342697, 171555), (343087, 171750), (343489, 171951), (343901, 172157), (344293, 172353), (344693, 172554), (345109, 172762), (345517, 172966), (345923, 173169), (346337, 173376), (346751, 173583), (347167, 173791), (347579, 173997), (347993, 174205), (348407, 174412), (348811, 174614), (349211, 174814), (349603, 175010), (350003, 175210), (350411, 175414), (350809, 175613), (351223, 175821), (351643, 176031), (352057, 176238), (352463, 176441), (352883, 176651), (353293, 176856), (353711, 177065), (354121, 177270), (354539, 177480), (354961, 177691), (355379, 177900), (355799, 178110), (356219, 178320), (356621, 178521), (357031, 178726), (357437, 178929), (357859, 179141), (358279, 179351), (358703, 179563), (359111, 179767), (359509, 179966), (359929, 180176), (360337, 180380), (360749, 180586), (361159, 180791), (361577, 181001), (362003, 181214), (362429, 181427), (362851, 181638), (363277, 181851), (363691, 182058), (364103, 182264), (364523, 182474), (364943, 182685), (365369, 182898), (365797, 183112), (366221, 183324), (366631, 183529), (367049, 183738), (367469, 183948), (367889, 184158), (368293, 184361), (368717, 184573), (369143, 184786), (369557, 184993), (369983, 185206), (370411, 185420), (370837, 185633), (371257, 185843), (371669, 186050), (372067, 186249), (372497, 186464), (372917, 186674), (373349, 186890), (373777, 187104), (374203, 187317), (374603, 187517), (375029, 187731), (375457, 187945), (375857, 188145), (376291, 188362), (376721, 188577), (377147, 188790), (377581, 189007), (378011, 189222), (378439, 189436), (378869, 189652), (379289, 189862), (379723, 190079), (380147, 190291), (380563, 190499), (380983, 190709), (381419, 190927), (381853, 191144), (382271, 191354), (382709, 191573), (383147, 191792), (383573, 192005), (384001, 192219), (384437, 192437), (384851, 192644), (385289, 192863), (385709, 193074), (386149, 193294), (386587, 193513), (387017, 193728), (387449, 193944), (387857, 194148), (388277, 194358), (388711, 194575), (389149, 194795), (389591, 195016), (390001, 195221), (390437, 195439), (390877, 195659), (391301, 195871), (391739, 196090), (392177, 196309), (392611, 196527), (393031, 196737), (393473, 196958), (393901, 197172), (394327, 197385), (394759, 197601), (395201, 197822), (395627, 198035), (396061, 198253), (396479, 198462), (396919, 198682), (397361, 198903), (397807, 199126), (398249, 199347), (398693, 199569), (399137, 199791), (399583, 200014)] 681 (by decide +kernel) n (by omega) s200014)
  omega

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2--h2».Context

open Filter

/-! Hole `hs2` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h3_v2__h1__h1__h1__h2__h2 : ∀ (n : ℕ),
  (229 : ℕ) ≤ n →
    n ≤ (200014 : ℕ) →
      ∃ (p : ℕ),
        Nat.Prime p ∧
          n < p ∧
            p < (2 : ℕ) * n ∧
              (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧
                ∀ α < n,
                  p < α + n →
                    (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                      ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

Rendered from gloss/0db9c68f9a82….md · Improve these words →

Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000360.json, merge commit feeca055f8c6.

Verdict pass, from attestations/000360.json.

Submitter: t1001-402a
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000360.json, merge commit feeca055f8c6.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Witness.lean, sha256 21cfbf7f41e7.

import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2--h2».Context

open Filter

theorem witness : ∃ n : ℕ, 229 ≤ n ∧ n ≤ 200014 := ⟨229, le_refl _, by norm_num⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

How to read this page

How to read a statement’s page →