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

Window primes for 10 ≤ n ≤ 228

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

proved

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

$\displaystyle \forall n \in \mathbb{N},\ 10 \le n \le 228:\ \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 10 to 228 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__h1 : ∀ (n : ℕ),
  (10 : ℕ) ≤ n →
    n ≤ (228 : ℕ) →
      ∃ (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, 000359, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000359.json, merge commit 14ac3cf837a0.

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 : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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--h1/Proof.lean, lines 21–31 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 25 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 26 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 27 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 29 at 14ac3cf837a0 ↗
hP have ∀ (p : ℕ), (decide ((1 : ℕ) < p) && (decide (p < (49 : ℕ)) && decide (p.gcd (30 : ℕ) = (1 : ℕ)) || decide (p < (900 : ℕ)) && decide (p.gcd (6469693230 : ℕ) = (1 : ℕ)) || decide (p < (529 : ℕ)) && decide (p.gcd (9699690 : ℕ) = (1 : ℕ)))) = true → Nat.Prime p
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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 < (529 : ℕ)) && decide (p.gcd (9699690 : ℕ) = (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 < 529) && decide (Nat.gcd p 9699690 = 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 23 9699690 (by decide +kernel) p h1 h2 h3
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 32–38 at 14ac3cf837a0 ↗
1. hP.s1 obtain (1 : ℕ) < p ∧ ((p < (49 : ℕ) ∧ p.gcd (30 : ℕ) = (1 : ℕ) ∨ p < (900 : ℕ) ∧ p.gcd (6469693230 : ℕ) = (1 : ℕ)) ∨ p < (529 : ℕ) ∧ p.gcd (9699690 : ℕ) = (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--h1/Proof.lean, line 35 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 36 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 37 at 14ac3cf837a0 ↗
4. hP.s4 case
 Leaves Nat.Prime p.
 Uses library Lean.Parser.Tactic.DecideConfig.kernel.
 Lean, line 38
 · exact lvl 23 9699690 (by decide +kernel) p h1 h2 h3
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 38 at 14ac3cf837a0 ↗
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 : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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--h1/Proof.lean, lines 39–60 at 14ac3cf837a0 ↗
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--h1/Proof.lean, lines 48–51 at 14ac3cf837a0 ↗
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--h1/Proof.lean, lines 52–60 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 55 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, lines 57–59 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 58 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 60 at 14ac3cf837a0 ↗
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 : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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--h1/Proof.lean, lines 61–91 at 14ac3cf837a0 ↗
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--h1/Proof.lean, lines 69–72 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 70 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, lines 71–72 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 71 at 14ac3cf837a0 ↗
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--h1/Proof.lean, lines 73–91 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 77 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 78 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 79 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 80 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 81 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 82 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 83 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 84 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, lines 85–88 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 87 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 89 at 14ac3cf837a0 ↗
 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--h1/Proof.lean, line 90 at 14ac3cf837a0 ↗
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 : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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--h1/Proof.lean, lines 92–100 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 98 at 14ac3cf837a0 ↗
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--h1/Proof.lean, line 99 at 14ac3cf837a0 ↗
r5b_cert_14 have ∃ (p : ℕ), Nat.Prime p ∧ (14 : ℕ) < p ∧ p < (2 : ℕ) * (14 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (14 : ℕ) - p) ≤ (14 : ℕ) + (2 : ℕ) ∧ ∀ α < (14 : ℕ), p < α + (14 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (14 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (14 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_14 : ∃ (p : ℕ), Nat.Prime p ∧ (14 : ℕ) < p ∧ p < (2 : ℕ) * (14 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (14 : ℕ) - p) ≤ (14 : ℕ) + (2 : ℕ) ∧ ∀ α < (14 : ℕ), p < α + (14 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (14 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (14 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 101–127
```
 have r5b_cert_14 : ∃ p : ℕ, p.Prime ∧ 14 < p ∧ p < 2 * 14 ∧ 2 * (2 * 14 - p) ≤ 14 + 2 ∧
 ∀ α : ℕ, α < 14 → p < α + 14 →
 (∃ q : ℕ, q.Prime ∧ 14 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 14 * x ≤ α * y) := by
 refine ⟨23, 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 < 14 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 10 * 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 : 10 * 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 : 3 ≤ x := by omega
 have x2 : x ≤ 3 := by
 by_contra h
 have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 4 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 101–127 at 14ac3cf837a0 ↗
1. r5b_cert_14.s1 obtain x * y ∣ α
 Leaves (14 : ℕ) * 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--h1/Proof.lean, line 109 at 14ac3cf837a0 ↗
2. r5b_cert_14.hc' have α * y < (14 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (14 : ℕ) * x.
 Lean, line 111
 have hc' : α * y < 14 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 111 at 14ac3cf837a0 ↗
3. r5b_cert_14.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--h1/Proof.lean, line 112 at 14ac3cf837a0 ↗
4. r5b_cert_14.b1 have (10 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (10 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 113
 have b1 : 10 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 113 at 14ac3cf837a0 ↗
5. r5b_cert_14.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--h1/Proof.lean, line 114 at 14ac3cf837a0 ↗
6. r5b_cert_14.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--h1/Proof.lean, line 115 at 14ac3cf837a0 ↗
7. r5b_cert_14.b3 have (10 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (10 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 116
 have b3 : 10 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 116 at 14ac3cf837a0 ↗
8. r5b_cert_14.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--h1/Proof.lean, line 117 at 14ac3cf837a0 ↗
9. r5b_cert_14.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--h1/Proof.lean, line 118 at 14ac3cf837a0 ↗
10. r5b_cert_14.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--h1/Proof.lean, line 119 at 14ac3cf837a0 ↗
11. r5b_cert_14.x1 have (3 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (3 : ℕ) ≤ x.
 Lean, line 120
 have x1 : 3 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 120 at 14ac3cf837a0 ↗
12. r5b_cert_14.x2 have x ≤ (3 : ℕ)
 Leaves False, with x2 : x ≤ (3 : ℕ).
 Lean, lines 121–124
 have x2 : x ≤ 3 := by by_contra h have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 121–124 at 14ac3cf837a0 ↗
 r5b_cert_14.x2.this have (4 : ℕ) * (4 : ℕ) ≤ x * x
 Leaves False, with this : (4 : ℕ) * (4 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 123
 have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 123 at 14ac3cf837a0 ↗
13. r5b_cert_14.s13 case
 Leaves False.
 Lean, lines 126–127
 · have y2 : y ≤ 4 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 126–127 at 14ac3cf837a0 ↗
 r5b_cert_14.s13.y2 have y ≤ (4 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (4 : ℕ).
 Lean, line 126
 · have y2 : y ≤ 4 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 126 at 14ac3cf837a0 ↗
r5b_cert_18 have ∃ (p : ℕ), Nat.Prime p ∧ (18 : ℕ) < p ∧ p < (2 : ℕ) * (18 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (18 : ℕ) - p) ≤ (18 : ℕ) + (2 : ℕ) ∧ ∀ α < (18 : ℕ), p < α + (18 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (18 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (18 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_18 : ∃ (p : ℕ), Nat.Prime p ∧ (18 : ℕ) < p ∧ p < (2 : ℕ) * (18 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (18 : ℕ) - p) ≤ (18 : ℕ) + (2 : ℕ) ∧ ∀ α < (18 : ℕ), p < α + (18 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (18 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (18 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 128–152
```
 have r5b_cert_18 : ∃ p : ℕ, p.Prime ∧ 18 < p ∧ p < 2 * 18 ∧ 2 * (2 * 18 - p) ≤ 18 + 2 ∧
 ∀ α : ℕ, α < 18 → p < α + 18 →
 (∃ q : ℕ, q.Prime ∧ 18 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 18 * x ≤ α * y) := by
 refine ⟨31, 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 < 18 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 14 * 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 : 14 * 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 : 4 ≤ x := by omega
 have x2 : x ≤ 3 := by
 by_contra h
 have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 128–152 at 14ac3cf837a0 ↗
1. r5b_cert_18.s1 obtain x * y ∣ α
 Leaves (18 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 136
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 136 at 14ac3cf837a0 ↗
2. r5b_cert_18.hc' have α * y < (18 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (18 : ℕ) * x.
 Lean, line 138
 have hc' : α * y < 18 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 138 at 14ac3cf837a0 ↗
3. r5b_cert_18.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 139
 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--h1/Proof.lean, line 139 at 14ac3cf837a0 ↗
4. r5b_cert_18.b1 have (14 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (14 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 140
 have b1 : 14 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 140 at 14ac3cf837a0 ↗
5. r5b_cert_18.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 141
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 141 at 14ac3cf837a0 ↗
6. r5b_cert_18.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 142
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 142 at 14ac3cf837a0 ↗
7. r5b_cert_18.b3 have (14 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (14 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 143
 have b3 : 14 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 143 at 14ac3cf837a0 ↗
8. r5b_cert_18.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 144
 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--h1/Proof.lean, line 144 at 14ac3cf837a0 ↗
9. r5b_cert_18.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 145
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 145 at 14ac3cf837a0 ↗
10. r5b_cert_18.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 146
 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--h1/Proof.lean, line 146 at 14ac3cf837a0 ↗
11. r5b_cert_18.x1 have (4 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (4 : ℕ) ≤ x.
 Lean, line 147
 have x1 : 4 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 147 at 14ac3cf837a0 ↗
12. r5b_cert_18.x2 have x ≤ (3 : ℕ)
 Leaves False, with x2 : x ≤ (3 : ℕ).
 Lean, lines 148–151
 have x2 : x ≤ 3 := by by_contra h have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 148–151 at 14ac3cf837a0 ↗
 r5b_cert_18.x2.this have (4 : ℕ) * (4 : ℕ) ≤ x * x
 Leaves False, with this : (4 : ℕ) * (4 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 150
 have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 150 at 14ac3cf837a0 ↗
r5b_cert_48 have ∃ (p : ℕ), Nat.Prime p ∧ (48 : ℕ) < p ∧ p < (2 : ℕ) * (48 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (48 : ℕ) - p) ≤ (48 : ℕ) + (2 : ℕ) ∧ ∀ α < (48 : ℕ), p < α + (48 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (48 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (48 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_48 : ∃ (p : ℕ), Nat.Prime p ∧ (48 : ℕ) < p ∧ p < (2 : ℕ) * (48 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (48 : ℕ) - p) ≤ (48 : ℕ) + (2 : ℕ) ∧ ∀ α < (48 : ℕ), p < α + (48 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (48 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (48 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 153–177
```
 have r5b_cert_48 : ∃ p : ℕ, p.Prime ∧ 48 < p ∧ p < 2 * 48 ∧ 2 * (2 * 48 - p) ≤ 48 + 2 ∧
 ∀ α : ℕ, α < 48 → p < α + 48 →
 (∃ q : ℕ, q.Prime ∧ 48 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 48 * x ≤ α * y) := by
 refine ⟨89, 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 < 48 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 42 * 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 : 42 * 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 : 8 ≤ x := by omega
 have x2 : x ≤ 6 := by
 by_contra h
 have : 7 * 7 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 153–177 at 14ac3cf837a0 ↗
1. r5b_cert_48.s1 obtain x * y ∣ α
 Leaves (48 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 161
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 161 at 14ac3cf837a0 ↗
2. r5b_cert_48.hc' have α * y < (48 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (48 : ℕ) * x.
 Lean, line 163
 have hc' : α * y < 48 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 163 at 14ac3cf837a0 ↗
3. r5b_cert_48.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 164
 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--h1/Proof.lean, line 164 at 14ac3cf837a0 ↗
4. r5b_cert_48.b1 have (42 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (42 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 165
 have b1 : 42 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 165 at 14ac3cf837a0 ↗
5. r5b_cert_48.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 166
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 166 at 14ac3cf837a0 ↗
6. r5b_cert_48.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 167
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 167 at 14ac3cf837a0 ↗
7. r5b_cert_48.b3 have (42 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (42 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 168
 have b3 : 42 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 168 at 14ac3cf837a0 ↗
8. r5b_cert_48.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 169
 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--h1/Proof.lean, line 169 at 14ac3cf837a0 ↗
9. r5b_cert_48.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 170
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 170 at 14ac3cf837a0 ↗
10. r5b_cert_48.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 171
 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--h1/Proof.lean, line 171 at 14ac3cf837a0 ↗
11. r5b_cert_48.x1 have (8 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (8 : ℕ) ≤ x.
 Lean, line 172
 have x1 : 8 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 172 at 14ac3cf837a0 ↗
12. r5b_cert_48.x2 have x ≤ (6 : ℕ)
 Leaves False, with x2 : x ≤ (6 : ℕ).
 Lean, lines 173–176
 have x2 : x ≤ 6 := by by_contra h have : 7 * 7 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 173–176 at 14ac3cf837a0 ↗
 r5b_cert_48.x2.this have (7 : ℕ) * (7 : ℕ) ≤ x * x
 Leaves False, with this : (7 : ℕ) * (7 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 175
 have : 7 * 7 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 175 at 14ac3cf837a0 ↗
r5b_cert_61 have ∃ (p : ℕ), Nat.Prime p ∧ (61 : ℕ) < p ∧ p < (2 : ℕ) * (61 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (61 : ℕ) - p) ≤ (61 : ℕ) + (2 : ℕ) ∧ ∀ α < (61 : ℕ), p < α + (61 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (61 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (61 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_61 : ∃ (p : ℕ), Nat.Prime p ∧ (61 : ℕ) < p ∧ p < (2 : ℕ) * (61 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (61 : ℕ) - p) ≤ (61 : ℕ) + (2 : ℕ) ∧ ∀ α < (61 : ℕ), p < α + (61 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (61 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (61 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 178–204
```
 have r5b_cert_61 : ∃ p : ℕ, p.Prime ∧ 61 < p ∧ p < 2 * 61 ∧ 2 * (2 * 61 - p) ≤ 61 + 2 ∧
 ∀ α : ℕ, α < 61 → p < α + 61 →
 (∃ q : ℕ, q.Prime ∧ 61 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 61 * x ≤ α * y) := by
 refine ⟨113, 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 < 61 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 53 * 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 : 53 * 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 : 7 ≤ x := by omega
 have x2 : x ≤ 7 := by
 by_contra h
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 8 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 178–204 at 14ac3cf837a0 ↗
1. r5b_cert_61.s1 obtain x * y ∣ α
 Leaves (61 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 186
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 186 at 14ac3cf837a0 ↗
2. r5b_cert_61.hc' have α * y < (61 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (61 : ℕ) * x.
 Lean, line 188
 have hc' : α * y < 61 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 188 at 14ac3cf837a0 ↗
3. r5b_cert_61.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 189
 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--h1/Proof.lean, line 189 at 14ac3cf837a0 ↗
4. r5b_cert_61.b1 have (53 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (53 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 190
 have b1 : 53 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 190 at 14ac3cf837a0 ↗
5. r5b_cert_61.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 191
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 191 at 14ac3cf837a0 ↗
6. r5b_cert_61.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 192
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 192 at 14ac3cf837a0 ↗
7. r5b_cert_61.b3 have (53 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (53 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 193
 have b3 : 53 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 193 at 14ac3cf837a0 ↗
8. r5b_cert_61.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 194
 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--h1/Proof.lean, line 194 at 14ac3cf837a0 ↗
9. r5b_cert_61.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 195
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 195 at 14ac3cf837a0 ↗
10. r5b_cert_61.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 196
 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--h1/Proof.lean, line 196 at 14ac3cf837a0 ↗
11. r5b_cert_61.x1 have (7 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (7 : ℕ) ≤ x.
 Lean, line 197
 have x1 : 7 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 197 at 14ac3cf837a0 ↗
12. r5b_cert_61.x2 have x ≤ (7 : ℕ)
 Leaves False, with x2 : x ≤ (7 : ℕ).
 Lean, lines 198–201
 have x2 : x ≤ 7 := by by_contra h have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 198–201 at 14ac3cf837a0 ↗
 r5b_cert_61.x2.this have (8 : ℕ) * (8 : ℕ) ≤ x * x
 Leaves False, with this : (8 : ℕ) * (8 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 200
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 200 at 14ac3cf837a0 ↗
13. r5b_cert_61.s13 case
 Leaves False.
 Lean, lines 203–204
 · have y2 : y ≤ 8 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 203–204 at 14ac3cf837a0 ↗
 r5b_cert_61.s13.y2 have y ≤ (8 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (8 : ℕ).
 Lean, line 203
 · have y2 : y ≤ 8 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 203 at 14ac3cf837a0 ↗
r5b_cert_62 have ∃ (p : ℕ), Nat.Prime p ∧ (62 : ℕ) < p ∧ p < (2 : ℕ) * (62 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (62 : ℕ) - p) ≤ (62 : ℕ) + (2 : ℕ) ∧ ∀ α < (62 : ℕ), p < α + (62 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (62 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (62 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_62 : ∃ (p : ℕ), Nat.Prime p ∧ (62 : ℕ) < p ∧ p < (2 : ℕ) * (62 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (62 : ℕ) - p) ≤ (62 : ℕ) + (2 : ℕ) ∧ ∀ α < (62 : ℕ), p < α + (62 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (62 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (62 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 205–233
```
 have r5b_cert_62 : ∃ p : ℕ, p.Prime ∧ 62 < p ∧ p < 2 * 62 ∧ 2 * (2 * 62 - p) ≤ 62 + 2 ∧
 ∀ α : ℕ, α < 62 → p < α + 62 →
 (∃ q : ℕ, q.Prime ∧ 62 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 62 * x ≤ α * y) := by
 refine ⟨113, 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 < 62 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 52 * 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 : 52 * 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 : 6 ≤ x := by omega
 have x2 : x ≤ 7 := by
 by_contra h
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 7 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 8 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 205–233 at 14ac3cf837a0 ↗
1. r5b_cert_62.s1 obtain x * y ∣ α
 Leaves (62 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 213
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 213 at 14ac3cf837a0 ↗
2. r5b_cert_62.hc' have α * y < (62 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (62 : ℕ) * x.
 Lean, line 215
 have hc' : α * y < 62 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 215 at 14ac3cf837a0 ↗
3. r5b_cert_62.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 216
 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--h1/Proof.lean, line 216 at 14ac3cf837a0 ↗
4. r5b_cert_62.b1 have (52 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (52 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 217
 have b1 : 52 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 217 at 14ac3cf837a0 ↗
5. r5b_cert_62.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 218
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 218 at 14ac3cf837a0 ↗
6. r5b_cert_62.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 219
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 219 at 14ac3cf837a0 ↗
7. r5b_cert_62.b3 have (52 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (52 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 220
 have b3 : 52 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 220 at 14ac3cf837a0 ↗
8. r5b_cert_62.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 221
 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--h1/Proof.lean, line 221 at 14ac3cf837a0 ↗
9. r5b_cert_62.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 222
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 222 at 14ac3cf837a0 ↗
10. r5b_cert_62.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 223
 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--h1/Proof.lean, line 223 at 14ac3cf837a0 ↗
11. r5b_cert_62.x1 have (6 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (6 : ℕ) ≤ x.
 Lean, line 224
 have x1 : 6 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 224 at 14ac3cf837a0 ↗
12. r5b_cert_62.x2 have x ≤ (7 : ℕ)
 Leaves False, with x2 : x ≤ (7 : ℕ).
 Lean, lines 225–228
 have x2 : x ≤ 7 := by by_contra h have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 225–228 at 14ac3cf837a0 ↗
 r5b_cert_62.x2.this have (8 : ℕ) * (8 : ℕ) ≤ x * x
 Leaves False, with this : (8 : ℕ) * (8 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 227
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 227 at 14ac3cf837a0 ↗
13. r5b_cert_62.s13 case
 Leaves False.
 Lean, lines 230–231
 · have y2 : y ≤ 7 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 230–231 at 14ac3cf837a0 ↗
 r5b_cert_62.s13.y2 have y ≤ (7 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (7 : ℕ).
 Lean, line 230
 · have y2 : y ≤ 7 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 230 at 14ac3cf837a0 ↗
14. r5b_cert_62.s14 case
 Leaves False.
 Lean, lines 232–233
 · have y2 : y ≤ 8 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 232–233 at 14ac3cf837a0 ↗
 r5b_cert_62.s14.y2 have y ≤ (8 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (8 : ℕ).
 Lean, line 232
 · have y2 : y ≤ 8 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 232 at 14ac3cf837a0 ↗
r5b_cert_63 have ∃ (p : ℕ), Nat.Prime p ∧ (63 : ℕ) < p ∧ p < (2 : ℕ) * (63 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (63 : ℕ) - p) ≤ (63 : ℕ) + (2 : ℕ) ∧ ∀ α < (63 : ℕ), p < α + (63 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (63 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (63 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_63 : ∃ (p : ℕ), Nat.Prime p ∧ (63 : ℕ) < p ∧ p < (2 : ℕ) * (63 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (63 : ℕ) - p) ≤ (63 : ℕ) + (2 : ℕ) ∧ ∀ α < (63 : ℕ), p < α + (63 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (63 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (63 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 234–264
```
 have r5b_cert_63 : ∃ p : ℕ, p.Prime ∧ 63 < p ∧ p < 2 * 63 ∧ 2 * (2 * 63 - p) ≤ 63 + 2 ∧
 ∀ α : ℕ, α < 63 → p < α + 63 →
 (∃ q : ℕ, q.Prime ∧ 63 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 63 * x ≤ α * y) := by
 refine ⟨113, 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 < 63 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 51 * 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 : 51 * 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 : 5 ≤ x := by omega
 have x2 : x ≤ 7 := by
 by_contra h
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 interval_cases x
 · have y2 : y ≤ 6 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 7 := by omega
 interval_cases y <;> omega
 · have y2 : y ≤ 8 := by omega
 interval_cases y <;> omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 234–264 at 14ac3cf837a0 ↗
1. r5b_cert_63.s1 obtain x * y ∣ α
 Leaves (63 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 242
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 242 at 14ac3cf837a0 ↗
2. r5b_cert_63.hc' have α * y < (63 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (63 : ℕ) * x.
 Lean, line 244
 have hc' : α * y < 63 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 244 at 14ac3cf837a0 ↗
3. r5b_cert_63.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 245
 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--h1/Proof.lean, line 245 at 14ac3cf837a0 ↗
4. r5b_cert_63.b1 have (51 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (51 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 246
 have b1 : 51 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 246 at 14ac3cf837a0 ↗
5. r5b_cert_63.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 247
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 247 at 14ac3cf837a0 ↗
6. r5b_cert_63.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 248
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 248 at 14ac3cf837a0 ↗
7. r5b_cert_63.b3 have (51 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (51 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 249
 have b3 : 51 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 249 at 14ac3cf837a0 ↗
8. r5b_cert_63.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 250
 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--h1/Proof.lean, line 250 at 14ac3cf837a0 ↗
9. r5b_cert_63.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 251
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 251 at 14ac3cf837a0 ↗
10. r5b_cert_63.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 252
 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--h1/Proof.lean, line 252 at 14ac3cf837a0 ↗
11. r5b_cert_63.x1 have (5 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (5 : ℕ) ≤ x.
 Lean, line 253
 have x1 : 5 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 253 at 14ac3cf837a0 ↗
12. r5b_cert_63.x2 have x ≤ (7 : ℕ)
 Leaves False, with x2 : x ≤ (7 : ℕ).
 Lean, lines 254–257
 have x2 : x ≤ 7 := by by_contra h have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 254–257 at 14ac3cf837a0 ↗
 r5b_cert_63.x2.this have (8 : ℕ) * (8 : ℕ) ≤ x * x
 Leaves False, with this : (8 : ℕ) * (8 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 256
 have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 256 at 14ac3cf837a0 ↗
13. r5b_cert_63.s13 case
 Leaves False.
 Lean, lines 259–260
 · have y2 : y ≤ 6 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 259–260 at 14ac3cf837a0 ↗
 r5b_cert_63.s13.y2 have y ≤ (6 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (6 : ℕ).
 Lean, line 259
 · have y2 : y ≤ 6 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 259 at 14ac3cf837a0 ↗
14. r5b_cert_63.s14 case
 Leaves False.
 Lean, lines 261–262
 · have y2 : y ≤ 7 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 261–262 at 14ac3cf837a0 ↗
 r5b_cert_63.s14.y2 have y ≤ (7 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (7 : ℕ).
 Lean, line 261
 · have y2 : y ≤ 7 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 261 at 14ac3cf837a0 ↗
15. r5b_cert_63.s15 case
 Leaves False.
 Lean, lines 263–264
 · have y2 : y ≤ 8 := by omega interval_cases y <;> omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 263–264 at 14ac3cf837a0 ↗
 r5b_cert_63.s15.y2 have y ≤ (8 : ℕ) routine: omega
 Leaves False, with y2 : y ≤ (8 : ℕ).
 Lean, line 263
 · have y2 : y ≤ 8 := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 263 at 14ac3cf837a0 ↗
r5b_cert_74 have ∃ (p : ℕ), Nat.Prime p ∧ (74 : ℕ) < p ∧ p < (2 : ℕ) * (74 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (74 : ℕ) - p) ≤ (74 : ℕ) + (2 : ℕ) ∧ ∀ α < (74 : ℕ), p < α + (74 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (74 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (74 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_74 : ∃ (p : ℕ), Nat.Prime p ∧ (74 : ℕ) < p ∧ p < (2 : ℕ) * (74 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (74 : ℕ) - p) ≤ (74 : ℕ) + (2 : ℕ) ∧ ∀ α < (74 : ℕ), p < α + (74 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (74 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (74 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 265–289
```
 have r5b_cert_74 : ∃ p : ℕ, p.Prime ∧ 74 < p ∧ p < 2 * 74 ∧ 2 * (2 * 74 - p) ≤ 74 + 2 ∧
 ∀ α : ℕ, α < 74 → p < α + 74 →
 (∃ q : ℕ, q.Prime ∧ 74 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 74 * x ≤ α * y) := by
 refine ⟨139, 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 < 74 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 66 * 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 : 66 * 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 : 9 ≤ x := by omega
 have x2 : x ≤ 8 := by
 by_contra h
 have : 9 * 9 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 265–289 at 14ac3cf837a0 ↗
1. r5b_cert_74.s1 obtain x * y ∣ α
 Leaves (74 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 273
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 273 at 14ac3cf837a0 ↗
2. r5b_cert_74.hc' have α * y < (74 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (74 : ℕ) * x.
 Lean, line 275
 have hc' : α * y < 74 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 275 at 14ac3cf837a0 ↗
3. r5b_cert_74.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 276
 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--h1/Proof.lean, line 276 at 14ac3cf837a0 ↗
4. r5b_cert_74.b1 have (66 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (66 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 277
 have b1 : 66 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 277 at 14ac3cf837a0 ↗
5. r5b_cert_74.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 278
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 278 at 14ac3cf837a0 ↗
6. r5b_cert_74.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 279
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 279 at 14ac3cf837a0 ↗
7. r5b_cert_74.b3 have (66 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (66 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 280
 have b3 : 66 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 280 at 14ac3cf837a0 ↗
8. r5b_cert_74.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 281
 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--h1/Proof.lean, line 281 at 14ac3cf837a0 ↗
9. r5b_cert_74.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 282
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 282 at 14ac3cf837a0 ↗
10. r5b_cert_74.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 283
 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--h1/Proof.lean, line 283 at 14ac3cf837a0 ↗
11. r5b_cert_74.x1 have (9 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (9 : ℕ) ≤ x.
 Lean, line 284
 have x1 : 9 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 284 at 14ac3cf837a0 ↗
12. r5b_cert_74.x2 have x ≤ (8 : ℕ)
 Leaves False, with x2 : x ≤ (8 : ℕ).
 Lean, lines 285–288
 have x2 : x ≤ 8 := by by_contra h have : 9 * 9 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 285–288 at 14ac3cf837a0 ↗
 r5b_cert_74.x2.this have (9 : ℕ) * (9 : ℕ) ≤ x * x
 Leaves False, with this : (9 : ℕ) * (9 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 287
 have : 9 * 9 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 287 at 14ac3cf837a0 ↗
r5b_cert_105 have ∃ (p : ℕ), Nat.Prime p ∧ (105 : ℕ) < p ∧ p < (2 : ℕ) * (105 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (105 : ℕ) - p) ≤ (105 : ℕ) + (2 : ℕ) ∧ ∀ α < (105 : ℕ), p < α + (105 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (105 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (105 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_105 : ∃ (p : ℕ), Nat.Prime p ∧ (105 : ℕ) < p ∧ p < (2 : ℕ) * (105 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (105 : ℕ) - p) ≤ (105 : ℕ) + (2 : ℕ) ∧ ∀ α < (105 : ℕ), p < α + (105 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (105 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (105 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 290–314
```
 have r5b_cert_105 : ∃ p : ℕ, p.Prime ∧ 105 < p ∧ p < 2 * 105 ∧ 2 * (2 * 105 - p) ≤ 105 + 2 ∧
 ∀ α : ℕ, α < 105 → p < α + 105 →
 (∃ q : ℕ, q.Prime ∧ 105 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 105 * x ≤ α * y) := by
 refine ⟨199, 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 < 105 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 95 * 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 : 95 * 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 : 10 ≤ x := by omega
 have x2 : x ≤ 9 := by
 by_contra h
 have : 10 * 10 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 290–314 at 14ac3cf837a0 ↗
1. r5b_cert_105.s1 obtain x * y ∣ α
 Leaves (105 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 298
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 298 at 14ac3cf837a0 ↗
2. r5b_cert_105.hc' have α * y < (105 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (105 : ℕ) * x.
 Lean, line 300
 have hc' : α * y < 105 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 300 at 14ac3cf837a0 ↗
3. r5b_cert_105.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 301
 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--h1/Proof.lean, line 301 at 14ac3cf837a0 ↗
4. r5b_cert_105.b1 have (95 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (95 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 302
 have b1 : 95 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 302 at 14ac3cf837a0 ↗
5. r5b_cert_105.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 303
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 303 at 14ac3cf837a0 ↗
6. r5b_cert_105.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 304
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 304 at 14ac3cf837a0 ↗
7. r5b_cert_105.b3 have (95 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (95 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 305
 have b3 : 95 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 305 at 14ac3cf837a0 ↗
8. r5b_cert_105.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 306
 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--h1/Proof.lean, line 306 at 14ac3cf837a0 ↗
9. r5b_cert_105.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 307
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 307 at 14ac3cf837a0 ↗
10. r5b_cert_105.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 308
 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--h1/Proof.lean, line 308 at 14ac3cf837a0 ↗
11. r5b_cert_105.x1 have (10 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (10 : ℕ) ≤ x.
 Lean, line 309
 have x1 : 10 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 309 at 14ac3cf837a0 ↗
12. r5b_cert_105.x2 have x ≤ (9 : ℕ)
 Leaves False, with x2 : x ≤ (9 : ℕ).
 Lean, lines 310–313
 have x2 : x ≤ 9 := by by_contra h have : 10 * 10 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 310–313 at 14ac3cf837a0 ↗
 r5b_cert_105.x2.this have (10 : ℕ) * (10 : ℕ) ≤ x * x
 Leaves False, with this : (10 : ℕ) * (10 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 312
 have : 10 * 10 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 312 at 14ac3cf837a0 ↗
r5b_cert_111 have ∃ (p : ℕ), Nat.Prime p ∧ (111 : ℕ) < p ∧ p < (2 : ℕ) * (111 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (111 : ℕ) - p) ≤ (111 : ℕ) + (2 : ℕ) ∧ ∀ α < (111 : ℕ), p < α + (111 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (111 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (111 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_111 : ∃ (p : ℕ), Nat.Prime p ∧ (111 : ℕ) < p ∧ p < (2 : ℕ) * (111 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (111 : ℕ) - p) ≤ (111 : ℕ) + (2 : ℕ) ∧ ∀ α < (111 : ℕ), p < α + (111 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (111 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (111 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 315–339
```
 have r5b_cert_111 : ∃ p : ℕ, p.Prime ∧ 111 < p ∧ p < 2 * 111 ∧ 2 * (2 * 111 - p) ≤ 111 + 2 ∧
 ∀ α : ℕ, α < 111 → p < α + 111 →
 (∃ q : ℕ, q.Prime ∧ 111 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 111 * x ≤ α * y) := by
 refine ⟨211, 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 < 111 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 101 * 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 : 101 * 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 : 11 ≤ x := by omega
 have x2 : x ≤ 10 := by
 by_contra h
 have : 11 * 11 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 315–339 at 14ac3cf837a0 ↗
1. r5b_cert_111.s1 obtain x * y ∣ α
 Leaves (111 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 323
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 323 at 14ac3cf837a0 ↗
2. r5b_cert_111.hc' have α * y < (111 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (111 : ℕ) * x.
 Lean, line 325
 have hc' : α * y < 111 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 325 at 14ac3cf837a0 ↗
3. r5b_cert_111.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 326
 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--h1/Proof.lean, line 326 at 14ac3cf837a0 ↗
4. r5b_cert_111.b1 have (101 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (101 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 327
 have b1 : 101 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 327 at 14ac3cf837a0 ↗
5. r5b_cert_111.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 328
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 328 at 14ac3cf837a0 ↗
6. r5b_cert_111.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 329
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 329 at 14ac3cf837a0 ↗
7. r5b_cert_111.b3 have (101 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (101 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 330
 have b3 : 101 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 330 at 14ac3cf837a0 ↗
8. r5b_cert_111.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 331
 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--h1/Proof.lean, line 331 at 14ac3cf837a0 ↗
9. r5b_cert_111.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 332
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 332 at 14ac3cf837a0 ↗
10. r5b_cert_111.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 333
 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--h1/Proof.lean, line 333 at 14ac3cf837a0 ↗
11. r5b_cert_111.x1 have (11 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (11 : ℕ) ≤ x.
 Lean, line 334
 have x1 : 11 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 334 at 14ac3cf837a0 ↗
12. r5b_cert_111.x2 have x ≤ (10 : ℕ)
 Leaves False, with x2 : x ≤ (10 : ℕ).
 Lean, lines 335–338
 have x2 : x ≤ 10 := by by_contra h have : 11 * 11 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 335–338 at 14ac3cf837a0 ↗
 r5b_cert_111.x2.this have (11 : ℕ) * (11 : ℕ) ≤ x * x
 Leaves False, with this : (11 : ℕ) * (11 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 337
 have : 11 * 11 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 337 at 14ac3cf837a0 ↗
r5b_cert_153 have ∃ (p : ℕ), Nat.Prime p ∧ (153 : ℕ) < p ∧ p < (2 : ℕ) * (153 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (153 : ℕ) - p) ≤ (153 : ℕ) + (2 : ℕ) ∧ ∀ α < (153 : ℕ), p < α + (153 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (153 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (153 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_153 : ∃ (p : ℕ), Nat.Prime p ∧ (153 : ℕ) < p ∧ p < (2 : ℕ) * (153 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (153 : ℕ) - p) ≤ (153 : ℕ) + (2 : ℕ) ∧ ∀ α < (153 : ℕ), p < α + (153 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (153 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (153 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 340–364
```
 have r5b_cert_153 : ∃ p : ℕ, p.Prime ∧ 153 < p ∧ p < 2 * 153 ∧ 2 * (2 * 153 - p) ≤ 153 + 2 ∧
 ∀ α : ℕ, α < 153 → p < α + 153 →
 (∃ q : ℕ, q.Prime ∧ 153 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 153 * x ≤ α * y) := by
 refine ⟨293, 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 < 153 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 141 * 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 : 141 * 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 : 12 ≤ x := by omega
 have x2 : x ≤ 11 := by
 by_contra h
 have : 12 * 12 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 340–364 at 14ac3cf837a0 ↗
1. r5b_cert_153.s1 obtain x * y ∣ α
 Leaves (153 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 348
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 348 at 14ac3cf837a0 ↗
2. r5b_cert_153.hc' have α * y < (153 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (153 : ℕ) * x.
 Lean, line 350
 have hc' : α * y < 153 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 350 at 14ac3cf837a0 ↗
3. r5b_cert_153.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 351
 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--h1/Proof.lean, line 351 at 14ac3cf837a0 ↗
4. r5b_cert_153.b1 have (141 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (141 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 352
 have b1 : 141 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 352 at 14ac3cf837a0 ↗
5. r5b_cert_153.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 353
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 353 at 14ac3cf837a0 ↗
6. r5b_cert_153.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 354
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 354 at 14ac3cf837a0 ↗
7. r5b_cert_153.b3 have (141 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (141 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 355
 have b3 : 141 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 355 at 14ac3cf837a0 ↗
8. r5b_cert_153.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 356
 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--h1/Proof.lean, line 356 at 14ac3cf837a0 ↗
9. r5b_cert_153.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 357
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 357 at 14ac3cf837a0 ↗
10. r5b_cert_153.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 358
 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--h1/Proof.lean, line 358 at 14ac3cf837a0 ↗
11. r5b_cert_153.x1 have (12 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (12 : ℕ) ≤ x.
 Lean, line 359
 have x1 : 12 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 359 at 14ac3cf837a0 ↗
12. r5b_cert_153.x2 have x ≤ (11 : ℕ)
 Leaves False, with x2 : x ≤ (11 : ℕ).
 Lean, lines 360–363
 have x2 : x ≤ 11 := by by_contra h have : 12 * 12 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 360–363 at 14ac3cf837a0 ↗
 r5b_cert_153.x2.this have (12 : ℕ) * (12 : ℕ) ≤ x * x
 Leaves False, with this : (12 : ℕ) * (12 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 362
 have : 12 * 12 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 362 at 14ac3cf837a0 ↗
r5b_cert_165 have ∃ (p : ℕ), Nat.Prime p ∧ (165 : ℕ) < p ∧ p < (2 : ℕ) * (165 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (165 : ℕ) - p) ≤ (165 : ℕ) + (2 : ℕ) ∧ ∀ α < (165 : ℕ), p < α + (165 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (165 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (165 : ℕ) * x ≤ α * y
Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (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_165 : ∃ (p : ℕ), Nat.Prime p ∧ (165 : ℕ) < p ∧ p < (2 : ℕ) * (165 : ℕ) ∧ (2 : ℕ) * ((2 : ℕ) * (165 : ℕ) - p) ≤ (165 : ℕ) + (2 : ℕ) ∧ ∀ α < (165 : ℕ), p < α + (165 : ℕ) → (∃ (q : ℕ), Nat.Prime q ∧ (165 : ℕ) ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → (165 : ℕ) * x ≤ α * y.
Uses library Exists.intro.
Lean, lines 365–389
```
 have r5b_cert_165 : ∃ p : ℕ, p.Prime ∧ 165 < p ∧ p < 2 * 165 ∧ 2 * (2 * 165 - p) ≤ 165 + 2 ∧
 ∀ α : ℕ, α < 165 → p < α + 165 →
 (∃ q : ℕ, q.Prime ∧ 165 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
 (∀ x y : ℕ, x < y → x * y ∣ α → 165 * x ≤ α * y) := by
 refine ⟨317, 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 < 165 * x := by omega
 have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
 have b1 : 153 * 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 : 153 * 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 : 13 ≤ x := by omega
 have x2 : x ≤ 12 := by
 by_contra h
 have : 13 * 13 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 omega
 omega
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 365–389 at 14ac3cf837a0 ↗
1. r5b_cert_165.s1 obtain x * y ∣ α
 Leaves (165 : ℕ) * x ≤ α * y, with m : ℕ, hm : α = x * y * m.
 Lean, line 373
 obtain ⟨m, hm⟩ := hd
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 373 at 14ac3cf837a0 ↗
2. r5b_cert_165.hc' have α * y < (165 : ℕ) * x routine: omega
 Leaves False, with hc' : α * y < (165 : ℕ) * x.
 Lean, line 375
 have hc' : α * y < 165 * x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 375 at 14ac3cf837a0 ↗
3. r5b_cert_165.m0 have (0 : ℕ) < m
 Leaves False, with m0 : (0 : ℕ) < m.
 Uses library Nat.pos_of_ne_zero.
 Lean, line 376
 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--h1/Proof.lean, line 376 at 14ac3cf837a0 ↗
4. r5b_cert_165.b1 have (153 : ℕ) * x ≤ α * x
 Leaves False, with b1 : (153 : ℕ) * x ≤ α * x.
 Uses library Nat.mul_le_mul_right.
 Lean, line 377
 have b1 : 153 * x ≤ α * x := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 377 at 14ac3cf837a0 ↗
5. r5b_cert_165.b2 have α * (x + (1 : ℕ)) ≤ α * y
 Leaves False, with b2 : α * (x + (1 : ℕ)) ≤ α * y.
 Uses library Nat.mul_le_mul_left.
 Lean, line 378
 have b2 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 378 at 14ac3cf837a0 ↗
6. r5b_cert_165.b2' have α * (x + (1 : ℕ)) = α * x + α routine: ring
 Leaves False, with b2' : α * (x + (1 : ℕ)) = α * x + α.
 Lean, line 379
 have b2' : α * (x + 1) = α * x + α := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 379 at 14ac3cf837a0 ↗
7. r5b_cert_165.b3 have (153 : ℕ) * y ≤ α * y
 Leaves False, with b3 : (153 : ℕ) * y ≤ α * y.
 Uses library Nat.mul_le_mul_right.
 Lean, line 380
 have b3 : 153 * y ≤ α * y := Nat.mul_le_mul_right _ (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 380 at 14ac3cf837a0 ↗
8. r5b_cert_165.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 381
 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--h1/Proof.lean, line 381 at 14ac3cf837a0 ↗
9. r5b_cert_165.b4' have x * (x + (1 : ℕ)) = x * x + x routine: ring
 Leaves False, with b4' : x * (x + (1 : ℕ)) = x * x + x.
 Lean, line 382
 have b4' : x * (x + 1) = x * x + x := by ring
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 382 at 14ac3cf837a0 ↗
10. r5b_cert_165.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 383
 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--h1/Proof.lean, line 383 at 14ac3cf837a0 ↗
11. r5b_cert_165.x1 have (13 : ℕ) ≤ x routine: omega
 Leaves False, with x1 : (13 : ℕ) ≤ x.
 Lean, line 384
 have x1 : 13 ≤ x := by omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 384 at 14ac3cf837a0 ↗
12. r5b_cert_165.x2 have x ≤ (12 : ℕ)
 Leaves False, with x2 : x ≤ (12 : ℕ).
 Lean, lines 385–388
 have x2 : x ≤ 12 := by by_contra h have : 13 * 13 ≤ x * x := Nat.mul_le_mul (by omega) (by omega) omega
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 385–388 at 14ac3cf837a0 ↗
 r5b_cert_165.x2.this have (13 : ℕ) * (13 : ℕ) ≤ x * x
 Leaves False, with this : (13 : ℕ) * (13 : ℕ) ≤ x * x.
 Uses library Nat.mul_le_mul.
 Lean, line 387
 have : 13 * 13 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
 targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 387 at 14ac3cf837a0 ↗
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.
Lean, lines 392–393
```
 · subst e14
 exact r5b_cert_14
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 392–393 at 14ac3cf837a0 ↗
s18 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 395–396
```
 · subst e18
 exact r5b_cert_18
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 395–396 at 14ac3cf837a0 ↗
s19 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 398–399
```
 · subst e48
 exact r5b_cert_48
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 398–399 at 14ac3cf837a0 ↗
s20 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 401–402
```
 · subst e61
 exact r5b_cert_61
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 401–402 at 14ac3cf837a0 ↗
s21 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 404–405
```
 · subst e62
 exact r5b_cert_62
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 404–405 at 14ac3cf837a0 ↗
s22 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 407–408
```
 · subst e63
 exact r5b_cert_63
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 407–408 at 14ac3cf837a0 ↗
s23 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 410–411
```
 · subst e74
 exact r5b_cert_74
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 410–411 at 14ac3cf837a0 ↗
s24 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 413–414
```
 · subst e105
 exact r5b_cert_105
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 413–414 at 14ac3cf837a0 ↗
s25 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 416–417
```
 · subst e111
 exact r5b_cert_111
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 416–417 at 14ac3cf837a0 ↗
s26 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 419–420
```
 · subst e153
 exact r5b_cert_153
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 419–420 at 14ac3cf837a0 ↗
s27 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 422–423
```
 · subst e165
 exact r5b_cert_165
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, lines 422–423 at 14ac3cf837a0 ↗
s28 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 425
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 13 [(19, 11), (23, 13)] 10 (by decide +kernel) n (by omega) s13)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 425 at 14ac3cf837a0 ↗
s29 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 427
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 17 [(29, 16), (31, 17)] 15 (by decide +kernel) n (by omega) s17)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 427 at 14ac3cf837a0 ↗
s30 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 429
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 47 [(37, 20), (41, 22), (43, 23), (47, 25), (47, 26), (53, 29), (59, 32), (61, 33), (67, 36), (73, 39), (79, 42), (83, 44), (89, 47)] 19 (by decide +kernel) n (by omega) s47)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 429 at 14ac3cf837a0 ↗
s31 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 431
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 60 [(97, 52), (103, 55), (109, 58), (113, 60)] 49 (by decide +kernel) n (by omega) s60)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 431 at 14ac3cf837a0 ↗
s32 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 433
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 73 [(127, 67), (131, 69), (139, 73)] 64 (by decide +kernel) n (by omega) s73)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 433 at 14ac3cf837a0 ↗
s33 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 435
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 104 [(149, 78), (157, 82), (163, 86), (173, 91), (181, 95), (191, 100), (199, 104)] 75 (by decide +kernel) n (by omega) s104)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 435 at 14ac3cf837a0 ↗
s34 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 437
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 110 [(211, 110)] 106 (by decide +kernel) n (by omega) s110)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 437 at 14ac3cf837a0 ↗
s35 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 439
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 152 [(223, 116), (233, 121), (241, 126), (251, 131), (263, 137), (271, 141), (283, 147), (293, 152)] 112 (by decide +kernel) n (by omega) s152)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 439 at 14ac3cf837a0 ↗
s36 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 441
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 164 [(307, 159), (317, 164)] 154 (by decide +kernel) n (by omega) s164)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 441 at 14ac3cf837a0 ↗
s37 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 443
```
 · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 228 [(331, 171), (337, 175), (349, 181), (359, 186), (373, 193), (383, 198), (397, 205), (409, 211), (421, 217), (433, 223), (443, 228)] 166 (by decide +kernel) n (by omega) s228)
```
targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean, line 443 at 14ac3cf837a0 ↗

The proof in Lean (Proof.lean)

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

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--h1/Proof.lean, sha256 cd6a820a7f86.

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

open Filter

/-! Hole `hs1` 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__h1 : ∀ (n : ℕ),
  (10 : ℕ) ≤ n →
    n ≤ (228 : ℕ) →
      ∃ (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 < 529) && decide (Nat.gcd p 9699690 = 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 23 9699690 (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_14 : ∃ p : ℕ, p.Prime ∧ 14 < p ∧ p < 2 * 14 ∧ 2 * (2 * 14 - p) ≤ 14 + 2 ∧
      ∀ α : ℕ, α < 14 → p < α + 14 →
        (∃ q : ℕ, q.Prime ∧ 14 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 14 * x ≤ α * y) := by
    refine ⟨23, 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 < 14 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 10 * 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 : 10 * 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 : 3 ≤ x := by omega
    have x2 : x ≤ 3 := by
      by_contra h
      have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 4 := by omega
      interval_cases y <;> omega
  have r5b_cert_18 : ∃ p : ℕ, p.Prime ∧ 18 < p ∧ p < 2 * 18 ∧ 2 * (2 * 18 - p) ≤ 18 + 2 ∧
      ∀ α : ℕ, α < 18 → p < α + 18 →
        (∃ q : ℕ, q.Prime ∧ 18 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 18 * x ≤ α * y) := by
    refine ⟨31, 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 < 18 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 14 * 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 : 14 * 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 : 4 ≤ x := by omega
    have x2 : x ≤ 3 := by
      by_contra h
      have : 4 * 4 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_48 : ∃ p : ℕ, p.Prime ∧ 48 < p ∧ p < 2 * 48 ∧ 2 * (2 * 48 - p) ≤ 48 + 2 ∧
      ∀ α : ℕ, α < 48 → p < α + 48 →
        (∃ q : ℕ, q.Prime ∧ 48 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 48 * x ≤ α * y) := by
    refine ⟨89, 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 < 48 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 42 * 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 : 42 * 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 : 8 ≤ x := by omega
    have x2 : x ≤ 6 := by
      by_contra h
      have : 7 * 7 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_61 : ∃ p : ℕ, p.Prime ∧ 61 < p ∧ p < 2 * 61 ∧ 2 * (2 * 61 - p) ≤ 61 + 2 ∧
      ∀ α : ℕ, α < 61 → p < α + 61 →
        (∃ q : ℕ, q.Prime ∧ 61 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 61 * x ≤ α * y) := by
    refine ⟨113, 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 < 61 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 53 * 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 : 53 * 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 : 7 ≤ x := by omega
    have x2 : x ≤ 7 := by
      by_contra h
      have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 8 := by omega
      interval_cases y <;> omega
  have r5b_cert_62 : ∃ p : ℕ, p.Prime ∧ 62 < p ∧ p < 2 * 62 ∧ 2 * (2 * 62 - p) ≤ 62 + 2 ∧
      ∀ α : ℕ, α < 62 → p < α + 62 →
        (∃ q : ℕ, q.Prime ∧ 62 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 62 * x ≤ α * y) := by
    refine ⟨113, 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 < 62 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 52 * 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 : 52 * 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 : 6 ≤ x := by omega
    have x2 : x ≤ 7 := by
      by_contra h
      have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 7 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 8 := by omega
      interval_cases y <;> omega
  have r5b_cert_63 : ∃ p : ℕ, p.Prime ∧ 63 < p ∧ p < 2 * 63 ∧ 2 * (2 * 63 - p) ≤ 63 + 2 ∧
      ∀ α : ℕ, α < 63 → p < α + 63 →
        (∃ q : ℕ, q.Prime ∧ 63 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 63 * x ≤ α * y) := by
    refine ⟨113, 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 < 63 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 51 * 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 : 51 * 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 : 5 ≤ x := by omega
    have x2 : x ≤ 7 := by
      by_contra h
      have : 8 * 8 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    interval_cases x
    · have y2 : y ≤ 6 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 7 := by omega
      interval_cases y <;> omega
    · have y2 : y ≤ 8 := by omega
      interval_cases y <;> omega
  have r5b_cert_74 : ∃ p : ℕ, p.Prime ∧ 74 < p ∧ p < 2 * 74 ∧ 2 * (2 * 74 - p) ≤ 74 + 2 ∧
      ∀ α : ℕ, α < 74 → p < α + 74 →
        (∃ q : ℕ, q.Prime ∧ 74 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 74 * x ≤ α * y) := by
    refine ⟨139, 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 < 74 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 66 * 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 : 66 * 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 : 9 ≤ x := by omega
    have x2 : x ≤ 8 := by
      by_contra h
      have : 9 * 9 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_105 : ∃ p : ℕ, p.Prime ∧ 105 < p ∧ p < 2 * 105 ∧ 2 * (2 * 105 - p) ≤ 105 + 2 ∧
      ∀ α : ℕ, α < 105 → p < α + 105 →
        (∃ q : ℕ, q.Prime ∧ 105 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 105 * x ≤ α * y) := by
    refine ⟨199, 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 < 105 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 95 * 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 : 95 * 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 : 10 ≤ x := by omega
    have x2 : x ≤ 9 := by
      by_contra h
      have : 10 * 10 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_111 : ∃ p : ℕ, p.Prime ∧ 111 < p ∧ p < 2 * 111 ∧ 2 * (2 * 111 - p) ≤ 111 + 2 ∧
      ∀ α : ℕ, α < 111 → p < α + 111 →
        (∃ q : ℕ, q.Prime ∧ 111 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 111 * x ≤ α * y) := by
    refine ⟨211, 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 < 111 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 101 * 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 : 101 * 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 : 11 ≤ x := by omega
    have x2 : x ≤ 10 := by
      by_contra h
      have : 11 * 11 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_153 : ∃ p : ℕ, p.Prime ∧ 153 < p ∧ p < 2 * 153 ∧ 2 * (2 * 153 - p) ≤ 153 + 2 ∧
      ∀ α : ℕ, α < 153 → p < α + 153 →
        (∃ q : ℕ, q.Prime ∧ 153 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 153 * x ≤ α * y) := by
    refine ⟨293, 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 < 153 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 141 * 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 : 141 * 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 : 12 ≤ x := by omega
    have x2 : x ≤ 11 := by
      by_contra h
      have : 12 * 12 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  have r5b_cert_165 : ∃ p : ℕ, p.Prime ∧ 165 < p ∧ p < 2 * 165 ∧ 2 * (2 * 165 - p) ≤ 165 + 2 ∧
      ∀ α : ℕ, α < 165 → p < α + 165 →
        (∃ q : ℕ, q.Prime ∧ 165 ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → 165 * x ≤ α * y) := by
    refine ⟨317, 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 < 165 * x := by omega
    have m0 : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; simp at hm; omega)
    have b1 : 153 * 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 : 153 * 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 : 13 ≤ x := by omega
    have x2 : x ≤ 12 := by
      by_contra h
      have : 13 * 13 ≤ x * x := Nat.mul_le_mul (by omega) (by omega)
      omega
    omega
  intro n hl hh
  by_cases e14 : n = 14
  · subst e14
    exact r5b_cert_14
  by_cases e18 : n = 18
  · subst e18
    exact r5b_cert_18
  by_cases e48 : n = 48
  · subst e48
    exact r5b_cert_48
  by_cases e61 : n = 61
  · subst e61
    exact r5b_cert_61
  by_cases e62 : n = 62
  · subst e62
    exact r5b_cert_62
  by_cases e63 : n = 63
  · subst e63
    exact r5b_cert_63
  by_cases e74 : n = 74
  · subst e74
    exact r5b_cert_74
  by_cases e105 : n = 105
  · subst e105
    exact r5b_cert_105
  by_cases e111 : n = 111
  · subst e111
    exact r5b_cert_111
  by_cases e153 : n = 153
  · subst e153
    exact r5b_cert_153
  by_cases e165 : n = 165
  · subst e165
    exact r5b_cert_165
  by_cases s13 : n ≤ 13
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 13 [(19, 11), (23, 13)] 10 (by decide +kernel) n (by omega) s13)
  by_cases s17 : n ≤ 17
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 17 [(29, 16), (31, 17)] 15 (by decide +kernel) n (by omega) s17)
  by_cases s47 : n ≤ 47
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 47 [(37, 20), (41, 22), (43, 23), (47, 25), (47, 26), (53, 29), (59, 32), (61, 33), (67, 36), (73, 39), (79, 42), (83, 44), (89, 47)] 19 (by decide +kernel) n (by omega) s47)
  by_cases s60 : n ≤ 60
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 60 [(97, 52), (103, 55), (109, 58), (113, 60)] 49 (by decide +kernel) n (by omega) s60)
  by_cases s73 : n ≤ 73
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 73 [(127, 67), (131, 69), (139, 73)] 64 (by decide +kernel) n (by omega) s73)
  by_cases s104 : n ≤ 104
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 104 [(149, 78), (157, 82), (163, 86), (173, 91), (181, 95), (191, 100), (199, 104)] 75 (by decide +kernel) n (by omega) s104)
  by_cases s110 : n ≤ 110
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 110 [(211, 110)] 106 (by decide +kernel) n (by omega) s110)
  by_cases s152 : n ≤ 152
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 152 [(223, 116), (233, 121), (241, 126), (251, 131), (263, 137), (271, 141), (283, 147), (293, 152)] 112 (by decide +kernel) n (by omega) s152)
  by_cases s164 : n ≤ 164
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 164 [(307, 159), (317, 164)] 154 (by decide +kernel) n (by omega) s164)
  by_cases s228 : n ≤ 228
  · 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 < 529) && decide (Nat.gcd p 9699690 = 1)))) hP 228 [(331, 171), (337, 175), (349, 181), (359, 186), (373, 193), (383, 198), (397, 205), (409, 211), (421, 217), (433, 223), (443, 228)] 166 (by decide +kernel) n (by omega) s228)
  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--h1».Context

open Filter

/-! Hole `hs1` 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__h1 : ∀ (n : ℕ),
  (10 : ℕ) ≤ n →
    n ≤ (228 : ℕ) →
      ∃ (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/00facf2c55c0….md · Improve these words →

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000359.json, merge commit 14ac3cf837a0.

Verdict pass, from attestations/000359.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/000359.json, merge commit 14ac3cf837a0.

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--h1/Witness.lean, sha256 1c48fca55b62.

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

open Filter

theorem witness : ∃ n : ℕ, 10 ≤ n ∧ n ≤ 228 := ⟨10, 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 →