Problems / erdos-1094 / erdos-1094--h2--h2--h2--h1

small range 2k < n ≤ k^(2−21/40)/2

erdos-1094--h2--h2--h2--h1

proved

Hole h_small of erdos-1094--h2--h2--h2 (split by 20261014T111800Z-t1014-x-partial.lean).

$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\tfrac12\,k^{2-21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$

Either the Baker–Harman–Pintz short-interval prime count fails, or for all large $k$ and every integer $n$ with $2k<n\le\tfrac12 k^{2-21/40}$, some prime $p$ in $(k,\,k+3k^{21/40})$ divides $(n-1)(n-2)\cdots(n-k)$. Here BHP is the Baker–Harman–Pintz short-interval prime count $\exists C>0\ \exists k_0\ \forall k\ge k_0:\ C\,k^{21/40}/\log k\le\#\{p\text{ prime}:k<p<k+k^{21/40}\}$, the primes counted as the integers of the interval $(\lfloor k\rfloor,\lceil k+k^{21/40}\rceil)$ that are positive, prime in absolute value and lie strictly between $k$ and $k+k^{21/40}$ over the reals. $n$ ranges over $\mathbb{Z}$ and the product $\prod_{i=1}^{k}(n-i)$ is taken in $\mathbb{Z}$; the bounds on $n$ and $p$ are over the reals with $21/40$ a real exponent, and $\log$ is the natural logarithm.

unverified · history

Lean

theorem erdos_1094__h2__h2__h2__h1 : (¬∃ (C : ℝ),
      (0 : ℝ) < C ∧
        ∃ (k₀ : ℕ),
          ∀ (k : ℕ),
            k₀ ≤ k →
              C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
                (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                        (0 : ℤ) < p ∧
                          Nat.Prime p.natAbs ∧
                            (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
                  ℝ)) ∨
  ∃ (k₀ : ℕ),
    ∀ (k : ℕ),
      k₀ ≤ k →
        ∀ (n : ℤ),
          (2 : ℤ) * (↑k : ℤ) < n →
            (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) →
              ∃ (p : ℕ),
                Nat.Prime p ∧
                  (↑k : ℝ) < (↑p : ℝ) ∧
                    (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
                      (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := 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, 000524, records the gate’s run.

The proof step by step (outline)

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

Outline of Proof.lean, extracted by the gate at 15d1d4647b94 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.

h_x3b80 (hθ0) have (0 : ℝ) < θ
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hθ0 : (0 : ℝ) < θ.
Lean, line 32
```
 have hθ0 : (0 : ℝ) < θ := by rw [← hθ]; norm_num
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 32 at cd7163d4891e ↗
h_x3b81 (hθ1) have θ < (1 : ℝ)
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hθ1 : θ < (1 : ℝ).
Lean, line 33
```
 have hθ1 : θ < 1 := by rw [← hθ]; norm_num
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 33 at cd7163d4891e ↗
s3 obtain ∃ (pc : ℝ → ℝ → ℕ), ∀ (a b : ℝ), pc a b = {p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.card
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with pc : ℝ → ℝ → ℕ, hpc : ∀ (a b : ℝ), pc a b = {p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.card.
Uses library Finset.Ioo, Exists.intro, rfl.
Lean, line 35
```
 obtain ⟨pc, hpc⟩ : ∃ pc : ℝ → ℝ → ℕ, ∀ a b : ℝ, pc a b = ((Finset.Ioo ⌊a⌋ ⌈b⌉).filter (fun p : ℤ => 0 rfl⟩
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 35 at cd7163d4891e ↗
primeCard_le_add have ∀ (a b c : ℝ), b ≤ c → (↑(pc a c) : ℝ) ≤ (↑(pc a b) : ℝ) + (c - b + (1 : ℝ))
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with primeCard_le_add : ∀ (a b c : ℝ), b ≤ c → (↑(pc a c) : ℝ) ≤ (↑(pc a b) : ℝ) + (c - b + (1 : ℝ)).
Uses library Finset.filter, Finset.Ioo, le_trans, Nat.cast_le.
Lean, lines 36–58
```
 have primeCard_le_add : ∀ (a b c : ℝ), b ≤ c → (pc a c : ℝ) ≤ (pc a b : ℝ) + (c - b + 1) := by
 intro a b c hbc; rw [hpc, hpc]; clear hpc hθ0 hθ1
 -- Let S(t) := (Finset.Ioo ⌊a⌋ ⌈t⌉).filter (fun p : ℤ => 0 Finset.filter (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < t) (Finset.Ioo ⌊a⌋ ⌈t⌉);
 -- Show `S(c) ⊆ S(b) ∪ Finset.Ico ⌈b⌉ ⌈c⌉`.
 have h_subset : S c ⊆ S b ∪ Finset.Ico ⌈b⌉ ⌈c⌉ := by
 intro p hp; by_cases h : ( p : ℝ ) simp_all +decide ;
 · exact Or.inl <| Finset.mem_filter.mpr ⟨ Finset.mem_Ioo.mpr ⟨ Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.1, Int.lt_ceil.mpr h ⟩, Finset.mem_filter.mp hp |>.2.1, Finset.mem_filter.mp hp |>.2.2.1, Finset.mem_filter.mp hp |>.2.2.2.1, h ⟩;
 · exact Or.inr ⟨ Int.ceil_le.mpr h, Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.2 ⟩;
 -- Thus by `Finset.card_le_card` and `Finset.card_union_le`, `S(c).card ≤ S(b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card`.
 have h_card : (S c).card ≤ (S b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card := by
 exact le_trans ( Finset.card_le_card h_subset ) ( Finset.card_union_le _ _ );
 have hI : ((Finset.Ico ⌈b⌉ ⌈c⌉).card : ℝ) ≤ c - b + 1 := by
 rw [Int.card_Ico]
 have h0 : (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉ := sub_nonneg.mpr (Int.ceil_mono hbc)
 have h1 : (((⌈c⌉ - ⌈b⌉).toNat : ℕ) : ℝ) = ((⌈c⌉ - ⌈b⌉ : ℤ) : ℝ) := by
 rw [← Int.cast_natCast, Int.toNat_of_nonneg h0]
 rw [h1]
 push_cast
 linarith [Int.ceil_lt_add_one c, Int.le_ceil b]
 refine le_trans (Nat.cast_le.mpr h_card) ?_
 push_cast
 linarith [hI]
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 36–58 at cd7163d4891e ↗
1. primeCard_le_add.h_subset have S c ⊆ S b ∪ Finset.Ico ⌈b⌉ ⌈c⌉
 Leaves (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈c⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < c}.card : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.card : ℝ) + (c - b + (1 : ℝ)), with h_subset : S c ⊆ S b ∪ Finset.Ico ⌈b⌉ ⌈c⌉.
 Uses library Finset.Ico, Lean.Meta.Simp.Config.decide.
 Lean, lines 41–44
 have h_subset : S c ⊆ S b ∪ Finset.Ico ⌈b⌉ ⌈c⌉ := by intro p hp; by_cases h : ( p : ℝ ) simp_all +decide ; · exact Or.inl <| Finset.mem_filter.mpr ⟨ Finset.mem_Ioo.mpr ⟨ Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.1, Int.lt_ceil.mpr h ⟩, Finset.mem_filter.mp hp |>.2.1, Finset.mem_filter.mp hp |>.2.2.1, Finset.mem_filter.mp hp |>.2.2.2.1, h ⟩; · exact Or.inr ⟨ Int.ceil_le.mpr h, Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.2 ⟩;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 41–44 at cd7163d4891e ↗
 primeCard_le_add.h_subset.s1 case
 Leaves p ∈ S b ∨ ⌈b⌉ ≤ p ∧ p < ⌈c⌉.
 Uses library Or.inl, Finset.mem_filter, And.intro, Finset.mem_Ioo, Int.lt_ceil.
 Lean, line 43
 · exact Or.inl <| Finset.mem_filter.mpr ⟨ Finset.mem_Ioo.mpr ⟨ Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.1, Int.lt_ceil.mpr h ⟩, Finset.mem_filter.mp hp |>.2.1, Finset.mem_filter.mp hp |>.2.2.1, Finset.mem_filter.mp hp |>.2.2.2.1, h ⟩;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 43 at cd7163d4891e ↗
 primeCard_le_add.h_subset.s2 case
 Leaves p ∈ S b ∨ ⌈b⌉ ≤ p ∧ p < ⌈c⌉, with h : b ≤ (↑p : ℝ).
 Uses library Or.inr, And.intro, Int.ceil_le, Finset.mem_Ioo, Finset.mem_filter.
 Lean, line 44
 · exact Or.inr ⟨ Int.ceil_le.mpr h, Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.2 ⟩;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 44 at cd7163d4891e ↗
2. primeCard_le_add.h_card have (S c).card ≤ (S b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card
 Leaves (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈c⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < c}.card : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.card : ℝ) + (c - b + (1 : ℝ)), with h_card : (S c).card ≤ (S b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card.
 Uses library Finset.Ico, le_trans, Finset.card_le_card, Finset.card_union_le.
 Lean, lines 46–47
 have h_card : (S c).card ≤ (S b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card := by exact le_trans ( Finset.card_le_card h_subset ) ( Finset.card_union_le _ _ );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 46–47 at cd7163d4891e ↗
3. primeCard_le_add.hI have (↑(Finset.Ico ⌈b⌉ ⌈c⌉).card : ℝ) ≤ c - b + (1 : ℝ)
 Leaves (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈c⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < c}.card : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.card : ℝ) + (c - b + (1 : ℝ)), with hI : (↑(Finset.Ico ⌈b⌉ ⌈c⌉).card : ℝ) ≤ c - b + (1 : ℝ).
 Uses library Finset.Ico, Int.card_Ico, Int.ceil_lt_add_one, Int.le_ceil.
 Lean, lines 48–55
 have hI : ((Finset.Ico ⌈b⌉ ⌈c⌉).card : ℝ) ≤ c - b + 1 := by rw [Int.card_Ico] have h0 : (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉ := sub_nonneg.mpr (Int.ceil_mono hbc) have h1 : (((⌈c⌉ - ⌈b⌉).toNat : ℕ) : ℝ) = ((⌈c⌉ - ⌈b⌉ : ℤ) : ℝ) := by rw [← Int.cast_natCast, Int.toNat_of_nonneg h0] rw [h1] push_cast linarith [Int.ceil_lt_add_one c, Int.le_ceil b]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 48–55 at cd7163d4891e ↗
 primeCard_le_add.hI.h0 have (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉
 Leaves (↑(⌈c⌉ - ⌈b⌉).toNat : ℝ) ≤ c - b + (1 : ℝ), with h0 : (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉.
 Uses library sub_nonneg, Int.ceil_mono.
 Lean, line 50
 have h0 : (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉ := sub_nonneg.mpr (Int.ceil_mono hbc)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 50 at cd7163d4891e ↗
 primeCard_le_add.hI.h1 have (↑(⌈c⌉ - ⌈b⌉).toNat : ℝ) = (↑(⌈c⌉ - ⌈b⌉) : ℝ)
 Leaves (↑(⌈c⌉ - ⌈b⌉).toNat : ℝ) ≤ c - b + (1 : ℝ), with h1 : (↑(⌈c⌉ - ⌈b⌉).toNat : ℝ) = (↑(⌈c⌉ - ⌈b⌉) : ℝ).
 Uses library Int.cast_natCast, Int.toNat_of_nonneg.
 Lean, lines 51–52
 have h1 : (((⌈c⌉ - ⌈b⌉).toNat : ℕ) : ℝ) = ((⌈c⌉ - ⌈b⌉ : ℤ) : ℝ) := by rw [← Int.cast_natCast, Int.toNat_of_nonneg h0]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 51–52 at cd7163d4891e ↗
exists_prime_of_primeCard_pos have ∀ (a b : ℝ), (0 : ℕ) < pc a b → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with exists_prime_of_primeCard_pos : ∀ (a b : ℝ), (0 : ℕ) < pc a b → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b.
Lean, lines 59–62
```
 have exists_prime_of_primeCard_pos : ∀ (a b : ℝ), 0 < pc a b → ∃ p : ℕ, p.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) aesop
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 59–62 at cd7163d4891e ↗
1. exists_prime_of_primeCard_pos.s1 obtain {p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.Nonempty
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b, with p : ℤ, hp : p ∈ {p ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < b}.
 Uses library Finset.card_pos.
 Lean, line 61
 obtain ⟨ p, hp ⟩ := Finset.card_pos.mp h;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 61 at cd7163d4891e ↗
tendsto_log_rpow_mul_rpow_neg have ∀ (b c : ℝ), (0 : ℝ) < c → Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ))
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with tendsto_log_rpow_mul_rpow_neg : ∀ (b c : ℝ), (0 : ℝ) < c → Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ)).
Uses library Filter.Tendsto, Real.log, Filter.atTop, nhds, Filter.eventually_gt_atTop, div_eq_mul_inv, Real.rpow_neg.
Lean, lines 63–69
```
 have tendsto_log_rpow_mul_rpow_neg : ∀ (b c : ℝ), 0 < c → Filter.Tendsto (fun x : ℝ => (Real.log x) ^ b * x ^ (-c)) Filter.atTop (nhds 0) := by
 intro b c hc
 -- Use the fact that `Real.log x ^ b` is little-o of `x ^ c` as `x` tends to infinity.
 have h_log : (fun x : ℝ => Real.log x ^ b) =o[Filter.atTop] (fun x : ℝ => x ^ c) :=
 isLittleO_log_rpow_rpow_atTop b hc
 convert h_log.tendsto_div_nhds_zero.congr' _ using 1;
 filter_upwards [ Filter.eventually_gt_atTop 0 ] with x hx using by rw [ div_eq_mul_inv, Real.rpow_neg hx.le ] ;
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 63–69 at cd7163d4891e ↗
1. tendsto_log_rpow_mul_rpow_neg.h_log have (fun (x : ℝ) => Real.log x ^ b) =o[Filter.atTop] fun (x : ℝ) => x ^ c
 Leaves Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ)), with h_log : (fun (x : ℝ) => Real.log x ^ b) =o[Filter.atTop] fun (x : ℝ) => x ^ c.
 Uses library Real.log, Filter.atTop, isLittleO_log_rpow_rpow_atTop.
 Lean, lines 66–67
 have h_log : (fun x : ℝ => Real.log x ^ b) =o[Filter.atTop] (fun x : ℝ => x ^ c) := isLittleO_log_rpow_rpow_atTop b hc
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 66–67 at cd7163d4891e ↗
poly_log_lt have ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ)
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with poly_log_lt : ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ).
Uses library Filter.atTop, Real.log, gt_mem_nhds, Filter.eventually_gt_atTop, div_lt_iff₀, div_pos, Real.rpow_pos_of_pos, Nat.cast_pos, Real.log_pos, Nat.one_lt_cast.
Lean, lines 70–83
```
 have poly_log_lt : ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), 0 < C → ∀ᶠ k : ℕ in Filter.atTop, A * (k : ℝ) ^ α * (Real.log k) ^ β ≤ C * (k : ℝ) ^ tt / Real.log k := by
 intro A α β tt hα C hC
 -- Let's choose any $C > 0$ and derive a contradiction.
 have h_lim : Filter.Tendsto (fun k : ℕ => (A * (k : ℝ) ^ α * (Real.log k) ^ β) / ((k : ℝ) ^ tt / (Real.log k))) Filter.atTop (nhds 0) := by
 -- Simplify the expression inside the limit.
 suffices h_simp : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1) * (k : ℝ) ^ (α - tt)) Filter.atTop (nhds 0) by
 refine h_simp.congr' ?_;
 filter_upwards [ Filter.eventually_gt_atTop 1 ] with k hk ; rw [ Real.rpow_sub ( by positivity ) ] ; ring_nf;
 rw [ Real.rpow_add ( Real.log_pos ( Nat.one_lt_cast.mpr hk ) ), Real.rpow_one ] ; norm_num ; ring;
 have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_;
 · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring;
 · linarith;
 filter_upwards [ h_lim.eventually ( gt_mem_nhds hC ), Filter.eventually_gt_atTop 1 ] with k hk₁ hk₂;
 rw [ div_lt_iff₀ ( div_pos ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr hk₂.le ) _ ) ( Real.log_pos ( Nat.one_lt_cast.mpr hk₂ ) ) ) ] at hk₁ ; ring_nf at hk₁ ⊢ ; linarith
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 70–83 at cd7163d4891e ↗
1. poly_log_lt.h_lim have Filter.Tendsto (fun (k : ℕ) => A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β / ((↑k : ℝ) ^ tt / Real.log (↑k : ℝ))) Filter.atTop (nhds (0 : ℝ))
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with h_lim : Filter.Tendsto (fun (k : ℕ) => A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β / ((↑k : ℝ) ^ tt / Real.log (↑k : ℝ))) Filter.atTop (nhds (0 : ℝ)).
 Uses library Filter.Tendsto, Real.log, Filter.atTop, nhds.
 Lean, lines 73–81
 have h_lim : Filter.Tendsto (fun k : ℕ => (A * (k : ℝ) ^ α * (Real.log k) ^ β) / ((k : ℝ) ^ tt / (Real.log k))) Filter.atTop (nhds 0) := by -- Simplify the expression inside the limit. suffices h_simp : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1) * (k : ℝ) ^ (α - tt)) Filter.atTop (nhds 0) by refine h_simp.congr' ?_; filter_upwards [ Filter.eventually_gt_atTop 1 ] with k hk ; rw [ Real.rpow_sub ( by positivity ) ] ; ring_nf; rw [ Real.rpow_add ( Real.log_pos ( Nat.one_lt_cast.mpr hk ) ), Real.rpow_one ] ; norm_num ; ring; have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_; · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring; · linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 73–81 at cd7163d4891e ↗
 poly_log_lt.h_lim.h_simp suffices Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ))
 Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)).
 Uses library Filter.Tendsto, Real.log, Filter.atTop, nhds, Filter.eventually_gt_atTop, Real.rpow_sub, Real.rpow_add, Real.log_pos, Nat.one_lt_cast, Real.rpow_one.
 Lean, lines 75–78
 suffices h_simp : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1) * (k : ℝ) ^ (α - tt)) Filter.atTop (nhds 0) by refine h_simp.congr' ?_; filter_upwards [ Filter.eventually_gt_atTop 1 ] with k hk ; rw [ Real.rpow_sub ( by positivity ) ] ; ring_nf; rw [ Real.rpow_add ( Real.log_pos ( Nat.one_lt_cast.mpr hk ) ), Real.rpow_one ] ; norm_num ; ring;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 75–78 at cd7163d4891e ↗
 poly_log_lt.h_lim.this have Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ))
 Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)), with this : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ)).
 Lean, line 79
 have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 79 at cd7163d4891e ↗
 poly_log_lt.h_lim.s3 case
 Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)), with this : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ)).
 Uses library Filter.Tendsto.comp, tendsto_natCast_atTop_atTop.
 Lean, line 80
 · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 80 at cd7163d4891e ↗
 poly_log_lt.h_lim.s4 case routine: linarith
 Leaves (0 : ℝ) < tt - α.
 Lean, line 81
 · linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 81 at cd7163d4891e ↗
excess_le have ∀ (k N : ℕ), (1 : ℕ) ≤ k → (↑k : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ)
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with excess_le : ∀ (k N : ℕ), (1 : ℕ) ≤ k → (↑k : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ).
Uses library le_trans, Real.rpow_le_rpow, sub_nonneg, Real.one_le_rpow, Real.mul_rpow, Real.rpow_mul.
Lean, lines 84–95
```
 have excess_le : ∀ (k N : ℕ), 1 ≤ k → (k : ℝ) ≤ (N : ℝ) → (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 → (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by
 intro k N hk hkN hNk
 -- Subexcess bound: `(N:ℝ)^θ - (k:ℝ)^θ ≤ ((N:ℝ) - k)^θ`
 have h_subex : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ ((N : ℝ) - k) ^ θ := by
 rw [ sub_le_iff_le_add' ];
 convert Real.rpow_add_le_add_rpow _ _ _ _ using 1 <;> norm_num;
 · exact_mod_cast hkN;
 · exact hθ0.le;
 · exact le_of_lt hθ1;
 refine le_trans h_subex ?_;
 refine' le_trans ( Real.rpow_le_rpow ( sub_nonneg.mpr hkN ) ( show ( N : ℝ ) - k ≤ 3 * ( k : ℝ ) ^ θ by linarith [ show ( k : ℝ ) ^ θ ≥ 1 by exact Real.one_le_rpow ( by norm_cast ) ( by exact hθ0.le ) ] ) ( hθ0.le ) ) _;
 rw [ Real.mul_rpow ( by positivity ) ( by positivity ), ← Real.rpow_mul ( by positivity ) ]
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 84–95 at cd7163d4891e ↗
1. excess_le.h_subex have (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ ((↑N : ℝ) - (↑k : ℝ)) ^ θ
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ), with h_subex : (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ ((↑N : ℝ) - (↑k : ℝ)) ^ θ.
 Uses library sub_le_iff_le_add', Real.rpow_add_le_add_rpow.
 Lean, lines 87–92
 have h_subex : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ ((N : ℝ) - k) ^ θ := by rw [ sub_le_iff_le_add' ]; convert Real.rpow_add_le_add_rpow _ _ _ _ using 1 <;> norm_num; · exact_mod_cast hkN; · exact hθ0.le; · exact le_of_lt hθ1;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 87–92 at cd7163d4891e ↗
 excess_le.h_subex.s1 case
 Leaves k ≤ N.
 Lean, line 90
 · exact_mod_cast hkN;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 90 at cd7163d4891e ↗
 excess_le.h_subex.s2 case
 Leaves (0 : ℝ) ≤ θ.
 Lean, line 91
 · exact hθ0.le;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 91 at cd7163d4891e ↗
 excess_le.h_subex.s3 case
 Leaves θ ≤ (1 : ℝ).
 Uses library le_of_lt.
 Lean, line 92
 · exact le_of_lt hθ1;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 92 at cd7163d4891e ↗
count_beats_excess have ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (N : ℕ), (↑k : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ)
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with count_beats_excess : ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (N : ℕ), (↑k : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ).
Uses library Filter.atTop, Real.log, Filter.eventually_ge_atTop.
Lean, lines 96–130
```
 have count_beats_excess : ∀ (C : ℝ), 0 < C → ∀ᶠ k : ℕ in Filter.atTop, ∀ N : ℕ, (k : ℝ) ≤ (N : ℝ) → (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 → (N : ℝ) ^ θ - (k : ℝ) ^ θ + 2 < C * (N : ℝ) ^ θ / Real.log N := by
 intro C hC; clear primeCard_le_add exists_prime_of_primeCard_pos tendsto_log_rpow_mul_rpow_neg hpc
 -- Step 1: produce a purely-k bound and then specialize to N.
 have step1 : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) + 3 ≤ (C / 2) * (k : ℝ) ^ θ / Real.log k := by
 -- Apply `poly_log_lt` to each term separately.
 have hA : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by
 have := poly_log_lt ( ( 3 : ℝ ) ^ θ ) ( θ * θ ) 0 θ ( by nlinarith [ show 0 < θ by exact hθ0, show θ < 1 by exact hθ1 ] ) ( C / 4 ) ( by positivity );
 aesop
 have hB : ∀ᶠ k : ℕ in Filter.atTop, 3 ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by
 have := poly_log_lt ( 3 : ℝ ) 0 0 θ hθ0 ( C / 4 ) ( by positivity ) ; aesop;
 filter_upwards [ hA, hB ] with k hk₁ hk₂ using by ring_nf at hk₁ hk₂ ⊢; linarith;
 -- Step 2: Filter_upwards on [step1, eventually_ge_atTop 4] with k, hkA, hk4.
 filter_upwards [step1, Filter.eventually_ge_atTop 4] with k hkA hk4;
 intro N hkN hNk
 have hN_le_4k : (N : ℝ) ≤ 4 * (k : ℝ) := by
 linarith [ show ( k : ℝ ) ^ θ ≤ k by exact le_trans ( Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) <| show θ ≤ 1 by exact le_of_lt <| hθ1 ) <| by norm_num, show ( k : ℝ ) ≥ 4 by norm_cast ]
 have h_logN_le_2logk : Real.log (N : ℝ) ≤ 2 * Real.log (k : ℝ) := by
 erw [ ← Real.log_pow ] ; gcongr ; norm_cast at *;
 · linarith;
 · norm_cast at *; nlinarith;
 have h_logN_pos : 0 < Real.log (N : ℝ) := by
 exact Real.log_pos <| by norm_cast at *; linarith;
 have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ + 2 < (C / 2) * (k : ℝ) ^ θ / Real.log k := by
 have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by
 apply excess_le k N (by linarith) hkN hNk;
 linarith
 have h_rhs_bound : (C / 2) * (k : ℝ) ^ θ / Real.log k ≤ C * (N : ℝ) ^ θ / Real.log N := by
 rw [ div_le_div_iff₀ ] <;> try positivity;
 · have h_rhs_bound : (k : ℝ) ^ θ * Real.log N ≤ 2 * (N : ℝ) ^ θ * Real.log k := by
 have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by
 exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le );
 nlinarith [ Real.rpow_pos_of_pos ( by positivity : 0 < ( k : ℝ ) ) θ ];
 nlinarith;
 · exact Real.log_pos <| by norm_cast; linarith;
 linarith [h_exp_bound, h_rhs_bound]
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 96–130 at cd7163d4891e ↗
1. count_beats_excess.step1 have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) + (3 : ℝ) ≤ C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (N : ℕ), (↑k : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with step1 : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) + (3 : ℝ) ≤ C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Uses library Filter.atTop, Real.log.
 Lean, lines 99–106
 have step1 : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) + 3 ≤ (C / 2) * (k : ℝ) ^ θ / Real.log k := by -- Apply `poly_log_lt` to each term separately. have hA : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by have := poly_log_lt ( ( 3 : ℝ ) ^ θ ) ( θ * θ ) 0 θ ( by nlinarith [ show 0 < θ by exact hθ0, show θ < 1 by exact hθ1 ] ) ( C / 4 ) ( by positivity ); aesop have hB : ∀ᶠ k : ℕ in Filter.atTop, 3 ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by have := poly_log_lt ( 3 : ℝ ) 0 0 θ hθ0 ( C / 4 ) ( by positivity ) ; aesop; filter_upwards [ hA, hB ] with k hk₁ hk₂ using by ring_nf at hk₁ hk₂ ⊢; linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 99–106 at cd7163d4891e ↗
 count_beats_excess.step1.hA have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) + (3 : ℝ) ≤ C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ), with hA : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Uses library Filter.atTop, Real.log.
 Lean, lines 101–103
 have hA : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by have := poly_log_lt ( ( 3 : ℝ ) ^ θ ) ( θ * θ ) 0 θ ( by nlinarith [ show 0 < θ by exact hθ0, show θ < 1 by exact hθ1 ] ) ( C / 4 ) ( by positivity ); aesop
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 101–103 at cd7163d4891e ↗
 count_beats_excess.step1.hA.this have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ), with this : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Lean, line 102
 have := poly_log_lt ( ( 3 : ℝ ) ^ θ ) ( θ * θ ) 0 θ ( by nlinarith [ show 0 < θ by exact hθ0, show θ < 1 by exact hθ1 ] ) ( C / 4 ) ( by positivity );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 102 at cd7163d4891e ↗
 count_beats_excess.step1.hB have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ) + (3 : ℝ) ≤ C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ), with hB : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Uses library Filter.atTop, Real.log.
 Lean, lines 104–105
 have hB : ∀ᶠ k : ℕ in Filter.atTop, 3 ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by have := poly_log_lt ( 3 : ℝ ) 0 0 θ hθ0 ( C / 4 ) ( by positivity ) ; aesop;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 104–105 at cd7163d4891e ↗
 count_beats_excess.step1.hB.this have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) * (↑k : ℝ) ^ (0 : ℝ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ), with this : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) * (↑k : ℝ) ^ (0 : ℝ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (4 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Lean, line 105
 have := poly_log_lt ( 3 : ℝ ) 0 0 θ hθ0 ( C / 4 ) ( by positivity ) ; aesop;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 105 at cd7163d4891e ↗
2. count_beats_excess.hN_le_4k have (↑N : ℝ) ≤ (4 : ℝ) * (↑k : ℝ) routine: linarith
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with hN_le_4k : (↑N : ℝ) ≤ (4 : ℝ) * (↑k : ℝ).
 Uses library le_trans, Real.rpow_le_rpow_of_exponent_le, le_of_lt.
 Lean, lines 110–111
 have hN_le_4k : (N : ℝ) ≤ 4 * (k : ℝ) := by linarith [ show ( k : ℝ ) ^ θ ≤ k by exact le_trans ( Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) <| show θ ≤ 1 by exact le_of_lt <| hθ1 ) <| by norm_num, show ( k : ℝ ) ≥ 4 by norm_cast ]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 110–111 at cd7163d4891e ↗
3. count_beats_excess.h_logN_le_2logk have Real.log (↑N : ℝ) ≤ (2 : ℝ) * Real.log (↑k : ℝ)
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with h_logN_le_2logk : Real.log (↑N : ℝ) ≤ (2 : ℝ) * Real.log (↑k : ℝ).
 Uses library Real.log, Real.log_pow.
 Lean, lines 112–115
 have h_logN_le_2logk : Real.log (N : ℝ) ≤ 2 * Real.log (k : ℝ) := by erw [ ← Real.log_pow ] ; gcongr ; norm_cast at *; · linarith; · norm_cast at *; nlinarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 112–115 at cd7163d4891e ↗
 count_beats_excess.h_logN_le_2logk.s1 case routine: linarith
 Leaves (0 : ℕ) < N, with hθ0 : (0 : ℝ) < θ, hθ1 : θ < (1 : ℝ), poly_log_lt : ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), excess_le : ∀ (k N : ℕ), (1 : ℕ) ≤ k → k ≤ N → (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ), hC : (0 : ℝ) < C, hkN : k ≤ N, hNk : (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ), hN_le_4k : N ≤ (4 : ℕ) * k.
 Lean, line 114
 · linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 114 at cd7163d4891e ↗
 count_beats_excess.h_logN_le_2logk.s2 case
 Leaves (↑N : ℝ) ≤ (↑k : ℝ) ^ nat_lit 2.
 Lean, line 115
 · norm_cast at *; nlinarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 115 at cd7163d4891e ↗
4. count_beats_excess.h_logN_pos have (0 : ℝ) < Real.log (↑N : ℝ)
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with h_logN_pos : (0 : ℝ) < Real.log (↑N : ℝ).
 Uses library Real.log, Real.log_pos.
 Lean, lines 116–117
 have h_logN_pos : 0 < Real.log (N : ℝ) := by exact Real.log_pos <| by norm_cast at *; linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 116–117 at cd7163d4891e ↗
5. count_beats_excess.h_exp_bound have (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ)
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with h_exp_bound : (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ).
 Uses library Real.log.
 Lean, lines 118–121
 have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ + 2 < (C / 2) * (k : ℝ) ^ θ / Real.log k := by have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by apply excess_le k N (by linarith) hkN hNk; linarith
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 118–121 at cd7163d4891e ↗
 count_beats_excess.h_exp_bound.h_exp_bound have (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ)
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ), with h_exp_bound : (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (↑k : ℝ) ^ (θ * θ).
 Lean, lines 119–120
 have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by apply excess_le k N (by linarith) hkN hNk;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 119–120 at cd7163d4891e ↗
6. count_beats_excess.h_rhs_bound have C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ)
 Leaves (↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ), with h_rhs_bound : C / (2 : ℝ) * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ).
 Uses library Real.log, div_le_div_iff₀.
 Lean, lines 122–129
 have h_rhs_bound : (C / 2) * (k : ℝ) ^ θ / Real.log k ≤ C * (N : ℝ) ^ θ / Real.log N := by rw [ div_le_div_iff₀ ] <;> try positivity; · have h_rhs_bound : (k : ℝ) ^ θ * Real.log N ≤ 2 * (N : ℝ) ^ θ * Real.log k := by have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le ); nlinarith [ Real.rpow_pos_of_pos ( by positivity : 0 < ( k : ℝ ) ) θ ]; nlinarith; · exact Real.log_pos <| by norm_cast; linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 122–129 at cd7163d4891e ↗
 count_beats_excess.h_rhs_bound.s1 case
 Leaves C / (2 : ℝ) * (↑k : ℝ) ^ θ * Real.log (↑N : ℝ) ≤ C * (↑N : ℝ) ^ θ * Real.log (↑k : ℝ).
 Lean, lines 124–128
 · have h_rhs_bound : (k : ℝ) ^ θ * Real.log N ≤ 2 * (N : ℝ) ^ θ * Real.log k := by have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le ); nlinarith [ Real.rpow_pos_of_pos ( by positivity : 0 < ( k : ℝ ) ) θ ]; nlinarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 124–128 at cd7163d4891e ↗
 count_beats_excess.h_rhs_bound.s1.h_rhs_bound have (↑k : ℝ) ^ θ * Real.log (↑N : ℝ) ≤ (2 : ℝ) * (↑N : ℝ) ^ θ * Real.log (↑k : ℝ)
 Leaves C / (2 : ℝ) * (↑k : ℝ) ^ θ * Real.log (↑N : ℝ) ≤ C * (↑N : ℝ) ^ θ * Real.log (↑k : ℝ), with h_rhs_bound : (↑k : ℝ) ^ θ * Real.log (↑N : ℝ) ≤ (2 : ℝ) * (↑N : ℝ) ^ θ * Real.log (↑k : ℝ).
 Uses library Real.log, Real.rpow_pos_of_pos.
 Lean, lines 124–127
 · have h_rhs_bound : (k : ℝ) ^ θ * Real.log N ≤ 2 * (N : ℝ) ^ θ * Real.log k := by have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le ); nlinarith [ Real.rpow_pos_of_pos ( by positivity : 0 < ( k : ℝ ) ) θ ];
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 124–127 at cd7163d4891e ↗
 count_beats_excess.h_rhs_bound.s1.h_rhs_bound.h_rhs_bound have (↑k : ℝ) ^ θ ≤ (↑N : ℝ) ^ θ
 Leaves (↑k : ℝ) ^ θ * Real.log (↑N : ℝ) ≤ (2 : ℝ) * (↑N : ℝ) ^ θ * Real.log (↑k : ℝ), with h_rhs_bound : (↑k : ℝ) ^ θ ≤ (↑N : ℝ) ^ θ.
 Uses library Real.rpow_le_rpow.
 Lean, lines 125–126
 have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 125–126 at cd7163d4891e ↗
 count_beats_excess.h_rhs_bound.s2 case
 Leaves (0 : ℝ) < Real.log (↑k : ℝ).
 Uses library Real.log_pos.
 Lean, line 129
 · exact Real.log_pos <| by norm_cast; linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 129 at cd7163d4891e ↗
dvd_Pprod_of_factor have ∀ (k : ℕ) (n p : ℤ), ∀ i ∈ Finset.Icc (1 : ℕ) k, p ∣ n - (↑i : ℤ) → p ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ), ∀ i ∈ Finset.Icc (1 : ℕ) k, p ∣ n - (↑i : ℤ) → p ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).
Uses library Finset.Icc, Finset.dvd_prod_of_mem.
Lean, lines 131–133
```
 have dvd_Pprod_of_factor : ∀ (k : ℕ) (n : ℤ) (p : ℤ) (i : ℕ), i ∈ Finset.Icc 1 k → p ∣ (n - (i : ℤ)) → p ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
 intro k n p i hi hp
 exact hp.trans (Finset.dvd_prod_of_mem (fun i : ℕ => (n - (i : ℤ))) hi)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 131–133 at cd7163d4891e ↗
dvd_Pprod_of_mem have ∀ (k : ℕ) (n p t : ℤ), n - (↑k : ℤ) < t → t < n → p ∣ t → p ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with dvd_Pprod_of_mem : ∀ (k : ℕ) (n p t : ℤ), n - (↑k : ℤ) < t → t < n → p ∣ t → p ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).
Uses library Finset.Icc, Int.toNat, Int.toNat_of_nonneg, sub_nonneg.
Lean, lines 134–138
```
 have dvd_Pprod_of_mem : ∀ (k : ℕ) (n : ℤ) (p : ℤ) (t : ℤ), n - (k : ℤ) < t → t < n → p ∣ t → p ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
 intro k n p t h1 h2 hpt
 convert dvd_Pprod_of_factor k n p ( Int.toNat ( n - t ) ) ?_ ?_ using 1 <;> norm_num [ Int.toNat_of_nonneg ( sub_nonneg.mpr h2.le ) ];
 · omega;
 · assumption
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 134–138 at cd7163d4891e ↗
1. dvd_Pprod_of_mem.s1 case routine: omega
 Leaves (1 : ℕ) ≤ (n - t).toNat ∧ n ≤ (↑k : ℤ) + t.
 Lean, line 137
 · omega;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 137 at cd7163d4891e ↗
2. dvd_Pprod_of_mem.s2 case
 Leaves p ∣ t.
 Lean, line 138
 · assumption
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 138 at cd7163d4891e ↗
s12 case
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hB : ∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑(pc (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ θ)) : ℝ).
Uses library Max.max.
Lean, lines 140–235
```
 · right
 have exists_prime_in_window : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ a : ℝ, (k : ℝ) ≤ a → a ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ → ∃ p : ℕ, p.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < a + (k : ℝ) ^ θ := by
 clear tendsto_log_rpow_mul_rpow_neg poly_log_lt excess_le dvd_Pprod_of_factor dvd_Pprod_of_mem hpc
 obtain ⟨ C, hC, k₀, hk₀ ⟩ := hB;
 -- Choose `k₀' := max (max k₀ k₁) 2`.
 obtain ⟨ k₁, hk₁ ⟩ := Filter.eventually_atTop.mp (count_beats_excess C hC)
 use max (max k₀ k₁) 2;
 intros k hk a ha₁ ha₂
 set N := ⌈a⌉₊ with hN
 have hN₁ : (k : ℝ) ≤ (N : ℝ) := by
 exact_mod_cast ha₁.trans <| Nat.le_ceil _
 have hN₂ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by
 exact le_trans ( Nat.ceil_lt_add_one ( by linarith ) |> le_of_lt ) ( by linarith )
 have hN₃ : (N : ℝ) < a + 1 := by
 exact Nat.ceil_lt_add_one ( by linarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith [ le_max_right ( max k₀ k₁ ) 2 ] ] )
 have hN₄ : (k : ℝ) ≤ N := by
 exact_mod_cast hN₁
 have hN₅ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by
 convert hN₂ using 1;
 -- Apply `hk₀` to get `bhpN : C*(N:ℝ)^θ/Real.log N ≤ pc (N:ℝ) ((N:ℝ)+(N:ℝ)^θ)`.
 have h_bhpN : C * (N : ℝ) ^ θ / Real.log N ≤ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) := by
 exact hk₀ N ( by norm_cast at *; linarith [ Nat.le_max_left ( max k₀ k₁ ) 2, Nat.le_max_right ( max k₀ k₁ ) 2, Nat.le_max_left k₀ k₁, Nat.le_max_right k₀ k₁ ] );
 -- Apply `primeCard_le_add` to bound the prime count in `(N, a + k^θ)`.
 have h_primeCard_le_add : pc (N : ℝ) (a + (k : ℝ) ^ θ) ≥ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) - ((N : ℝ) ^ θ - (k : ℝ) ^ θ + 2) := by
 have h_primeCard_le_add : pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) ≤ pc (N : ℝ) (a + (k : ℝ) ^ θ) + ((N : ℝ) + (N : ℝ) ^ θ - (a + (k : ℝ) ^ θ) + 1) := by
 convert primeCard_le_add ( N : ℝ ) ( a + ( k : ℝ ) ^ θ ) ( N + ( N : ℝ ) ^ θ ) _ using 1;
 exact add_le_add ( Nat.le_ceil _ ) ( Real.rpow_le_rpow ( by linarith ) ( by linarith ) ( by exact hθ0.le ) );
 linarith;
 -- Therefore, `pc (N:ℝ) (a + k^θ) > 0`.
 have h_primeCard_pos : 0 < pc (N : ℝ) (a + (k : ℝ) ^ θ) := by
 exact_mod_cast ( by linarith [ hk₁ k ( by linarith [ le_max_left ( max k₀ k₁ ) 2, le_max_right ( max k₀ k₁ ) 2, le_max_left k₀ k₁, le_max_right k₀ k₁ ] ) N hN₄ hN₅ ] : ( 0 : ℝ ) < pc ( N : ℝ ) ( a + k ^ θ ) );
 exact exists_prime_of_primeCard_pos _ _ h_primeCard_pos |> fun ⟨ p, hp₁, hp₂, hp₃ ⟩ => ⟨ p, hp₁, by linarith [ Nat.le_ceil a, show ( p : ℝ ) ≥ N by exact_mod_cast hp₂.le ], hp₃ ⟩
 clear tendsto_log_rpow_mul_rpow_neg poly_log_lt excess_le count_beats_excess primeCard_le_add exists_prime_of_primeCard_pos dvd_Pprod_of_factor hB hpc
 obtain ⟨kw, hw⟩ := exists_prime_in_window
 clear pc
 use max kw 2
 intro k hk n hn1 hn2
 have hk2 : 2 ≤ k := le_trans (le_max_right _ _) hk
 have hkw : kw ≤ k := le_trans (le_max_left _ _) hk
 have hk0 : (0 : ℝ) < k := by exact_mod_cast (show 0 < k by omega)
 have hkθ : (0 : ℝ) < (k : ℝ) ^ θ := Real.rpow_pos_of_pos hk0 _
 have hN : (((n - 1).natAbs : ℕ) : ℤ) = n - 1 := Int.natAbs_of_nonneg (by omega)
 set m := (n - 1).natAbs / k with hmdef
 have hm : (m : ℤ) * k ≤ n - 1 ∧ n - 1 < ((m + 1) : ℤ) * k := by
 have h1 : k * m + (n - 1).natAbs % k = (n - 1).natAbs := Nat.div_add_mod _ _
 have h2 : (n - 1).natAbs % k < k := Nat.mod_lt _ (by omega)
 have h3 : (k : ℤ) * m + (((n - 1).natAbs % k : ℕ) : ℤ) = n - 1 := by rw [← hN]; exact_mod_cast h1
 have h4 : (((n - 1).natAbs % k : ℕ) : ℤ) < k := by exact_mod_cast h2
 have h5 : (0 : ℤ) ≤ (((n - 1).natAbs % k : ℕ) : ℤ) := by positivity
 constructor <;> linarith
 have hm_ge2 : 2 ≤ m := (Nat.le_div_iff_mul_le (by omega)).2 (by omega)
 have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast hm_ge2
 have hmk : (m : ℝ) * k ≤ n - 1 := by exact_mod_cast hm.1
 have hmk2 : (n : ℝ) - 1 < ((m : ℝ) + 1) * k := by exact_mod_cast hm.2
 have hm_lt : (m : ℝ) < (1 / 2) * (k : ℝ) ^ (1 - θ) := by
 have e : (k : ℝ) ^ ((2 : ℝ) - θ) = (k : ℝ) ^ (1 - θ) * k := by
 rw [show (2 : ℝ) - θ = (1 - θ) + 1 by ring, Real.rpow_add hk0, Real.rpow_one]
 rw [e] at hn2
 by_contra hc
 push Not at hc
 linarith [mul_le_mul_of_nonneg_right hc hk0.le]
 have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) := by
 have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) ^ (1 - θ) * (k : ℝ) ^ θ := by
 exact mul_lt_mul_of_pos_right (by linarith) hkθ
 convert hkey using 1 ; rw [ ← Real.rpow_add' ] <;> norm_num
 have hdiv : ((m : ℝ) - 1) * ((m : ℝ) / (m - 1) * (k : ℝ) ^ θ) = m * (k : ℝ) ^ θ := by
 have : (m : ℝ) - 1 ≠ 0 := by linarith
 field_simp
 have hdiv2 : (m : ℝ) / (m - 1) ≤ 2 := by
 rw [div_le_iff₀ (by linarith)]; linarith
 by_cases h_case : (n : ℝ) < (m : ℝ) * k + (m : ℝ) * (k : ℝ) ^ θ
 · obtain ⟨p, hp_prime, hp1, hp2⟩ := hw k hkw (k + (m : ℝ) / (m - 1) * (k : ℝ) ^ θ)
 (le_add_of_nonneg_right (mul_nonneg (div_nonneg (by positivity) (by linarith)) hkθ.le))
 (by linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le])
 have hpos : (0 : ℝ) < (m : ℝ) - 1 := by linarith
 have hA := mul_lt_mul_of_pos_left hp1 hpos
 have hB := mul_lt_mul_of_pos_left hp2 hpos
 refine ⟨p, hp_prime, ?_, ?_, ?_⟩
 · linarith [mul_nonneg (div_nonneg (by positivity : (0:ℝ) ≤ m) hpos.le) hkθ.le]
 · linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le]
 · apply dvd_Pprod_of_mem k n p (((m : ℤ) - 1) * p)
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hA, hdiv, h_case]
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hB, hdiv, hkey, hmk]
 · exact dvd_mul_left _ _
 · push Not at h_case
 obtain ⟨p, hp_prime, hp1, hp2⟩ : ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ p < (k : ℝ) + (k : ℝ) ^ θ :=
 hw k hkw k le_rfl (by linarith)
 have hpk : k + 1 ≤ p := by exact_mod_cast hp1
 refine ⟨p, hp_prime, hp1, by linarith, ?_⟩
 have hmp : (m : ℝ) * p < m * ((k : ℝ) + (k : ℝ) ^ θ) := mul_lt_mul_of_pos_left hp2 (by linarith)
 apply dvd_Pprod_of_mem k n p ((m : ℤ) * p)
 · have : (m : ℤ) * (k + 1) ≤ m * p := mul_le_mul_of_nonneg_left (by exact_mod_cast hpk) (by positivity)
 have hm1 : (1 : ℤ) ≤ m := by exact_mod_cast (show 1 ≤ m by omega)
 linarith [hm.2]
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hmp, h_case]
 · exact dvd_mul_left _ _
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 140–235 at cd7163d4891e ↗
1. s12.exists_prime_in_window have ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ
 Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with exists_prime_in_window : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ.
 Uses library Max.max, Exists.intro, Nat.le_ceil.
 Lean, lines 141–171
 have exists_prime_in_window : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ a : ℝ, (k : ℝ) ≤ a → a ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ → ∃ p : ℕ, p.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < a + (k : ℝ) ^ θ := by clear tendsto_log_rpow_mul_rpow_neg poly_log_lt excess_le dvd_Pprod_of_factor dvd_Pprod_of_mem hpc obtain ⟨ C, hC, k₀, hk₀ ⟩ := hB; -- Choose `k₀' := max (max k₀ k₁) 2`. obtain ⟨ k₁, hk₁ ⟩ := Filter.eventually_atTop.mp (count_beats_excess C hC) use max (max k₀ k₁) 2; intros k hk a ha₁ ha₂ set N := ⌈a⌉₊ with hN have hN₁ : (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast ha₁.trans <| Nat.le_ceil _ have hN₂ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by exact le_trans ( Nat.ceil_lt_add_one ( by linarith ) |> le_of_lt ) ( by linarith ) have hN₃ : (N : ℝ) < a + 1 := by exact Nat.ceil_lt_add_one ( by linarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith [ le_max_right ( max k₀ k₁ ) 2 ] ] ) have hN₄ : (k : ℝ) ≤ N := by exact_mod_cast hN₁ have hN₅ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by convert hN₂ using 1; -- Apply `hk₀` to get `bhpN : C*(N:ℝ)^θ/Real.log N ≤ pc (N:ℝ) ((N:ℝ)+(N:ℝ)^θ)`. have h_bhpN : C * (N : ℝ) ^ θ / Real.log N ≤ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) := by exact hk₀ N ( by norm_cast at *; linarith [ Nat.le_max_left ( max k₀ k₁ ) 2, Nat.le_max_right ( max k₀ k₁ ) 2, Nat.le_max_left k₀ k₁, Nat.le_max_right k₀ k₁ ] ); -- Apply `primeCard_le_add` to bound the prime count in `(N, a + k^θ)`. have h_primeCard_le_add : pc (N : ℝ) (a + (k : ℝ) ^ θ) ≥ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) - ((N : ℝ) ^ θ - (k : ℝ) ^ θ + 2) := by have h_primeCard_le_add : pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) ≤ pc (N : ℝ) (a + (k : ℝ) ^ θ) + ((N : ℝ) + (N : ℝ) ^ θ - (a + (k : ℝ) ^ θ) + 1) := by convert primeCard_le_add ( N : ℝ ) ( a + ( k : ℝ ) ^ θ ) ( N + ( N : ℝ ) ^ θ ) _ using 1; exact add_le_add ( Nat.le_ceil _ ) ( Real.rpow_le_rpow ( by linarith ) ( by linarith ) ( by exact hθ0.le ) ); linarith; -- Therefore, `pc (N:ℝ) (a + k^θ) > 0`. have h_primeCard_pos : 0 < pc (N : ℝ) (a + (k : ℝ) ^ θ) := by exact_mod_cast ( by linarith [ hk₁ k ( by linarith [ le_max_left ( max k₀ k₁ ) 2, le_max_right ( max k₀ k₁ ) 2, le_max_left k₀ k₁, le_max_right k₀ k₁ ] ) N hN₄ hN₅ ] : ( 0 : ℝ ) < pc ( N : ℝ ) ( a + k ^ θ ) ); exact exists_prime_of_primeCard_pos _ _ h_primeCard_pos |> fun ⟨ p, hp₁, hp₂, hp₃ ⟩ => ⟨ p, hp₁, by linarith [ Nat.le_ceil a, show ( p : ℝ ) ≥ N by exact_mod_cast hp₂.le ], hp₃ ⟩
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 141–171 at cd7163d4891e ↗
 s12.exists_prime_in_window.s1 obtain ∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑(pc (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ θ)) : ℝ)
 Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with C : ℝ, hC : (0 : ℝ) < C, k₀ : ℕ, hk₀ : ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑(pc (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ θ)) : ℝ).
 Lean, line 143
 obtain ⟨ C, hC, k₀, hk₀ ⟩ := hB;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 143 at cd7163d4891e ↗
 s12.exists_prime_in_window.s2 obtain ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → ∀ (N : ℕ), (↑b : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑b : ℝ) + (2 : ℝ) * (↑b : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑b : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ)
 Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with k₁ : ℕ, hk₁ : ∀ (b : ℕ), k₁ ≤ b → ∀ (N : ℕ), (↑b : ℝ) ≤ (↑N : ℝ) → (↑N : ℝ) ≤ (↑b : ℝ) + (2 : ℝ) * (↑b : ℝ) ^ θ + (1 : ℝ) → (↑N : ℝ) ^ θ - (↑b : ℝ) ^ θ + (2 : ℝ) < C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ).
 Uses library Filter.eventually_atTop.
 Lean, line 145
 obtain ⟨ k₁, hk₁ ⟩ := Filter.eventually_atTop.mp (count_beats_excess C hC)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 145 at cd7163d4891e ↗
 s12.exists_prime_in_window.hN1 have (↑k : ℝ) ≤ (↑N : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with hN₁ : (↑k : ℝ) ≤ (↑N : ℝ).
 Uses library Nat.le_ceil.
 Lean, lines 149–150
 have hN₁ : (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast ha₁.trans <| Nat.le_ceil _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 149–150 at cd7163d4891e ↗
 s12.exists_prime_in_window.hN2 have (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with hN₂ : (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ).
 Uses library le_trans, Nat.ceil_lt_add_one, le_of_lt.
 Lean, lines 151–152
 have hN₂ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by exact le_trans ( Nat.ceil_lt_add_one ( by linarith ) |> le_of_lt ) ( by linarith )
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 151–152 at cd7163d4891e ↗
 s12.exists_prime_in_window.hN3 have (↑N : ℝ) < a + (1 : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with hN₃ : (↑N : ℝ) < a + (1 : ℝ).
 Uses library Nat.ceil_lt_add_one, le_max_right, Max.max.
 Lean, lines 153–154
 have hN₃ : (N : ℝ) < a + 1 := by exact Nat.ceil_lt_add_one ( by linarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith [ le_max_right ( max k₀ k₁ ) 2 ] ] )
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 153–154 at cd7163d4891e ↗
 s12.exists_prime_in_window.hN4 have (↑k : ℝ) ≤ (↑N : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with hN₄ : (↑k : ℝ) ≤ (↑N : ℝ).
 Lean, lines 155–156
 have hN₄ : (k : ℝ) ≤ N := by exact_mod_cast hN₁
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 155–156 at cd7163d4891e ↗
 s12.exists_prime_in_window.hN5 have (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with hN₅ : (↑N : ℝ) ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ + (1 : ℝ).
 Lean, lines 157–158
 have hN₅ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by convert hN₂ using 1;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 157–158 at cd7163d4891e ↗
 s12.exists_prime_in_window.h_bhpN have C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ) ≤ (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with h_bhpN : C * (↑N : ℝ) ^ θ / Real.log (↑N : ℝ) ≤ (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ).
 Uses library Real.log, Nat.le_max_left, Max.max, Nat.le_max_right.
 Lean, lines 160–161
 have h_bhpN : C * (N : ℝ) ^ θ / Real.log N ≤ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) := by exact hk₀ N ( by norm_cast at *; linarith [ Nat.le_max_left ( max k₀ k₁ ) 2, Nat.le_max_right ( max k₀ k₁ ) 2, Nat.le_max_left k₀ k₁, Nat.le_max_right k₀ k₁ ] );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 160–161 at cd7163d4891e ↗
 s12.exists_prime_in_window.h_primeCard_le_add have (↑(pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)) : ℝ) ≥ (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ) - ((↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ))
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with h_primeCard_le_add : (↑(pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)) : ℝ) ≥ (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ) - ((↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ)).
 Lean, lines 163–167
 have h_primeCard_le_add : pc (N : ℝ) (a + (k : ℝ) ^ θ) ≥ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) - ((N : ℝ) ^ θ - (k : ℝ) ^ θ + 2) := by have h_primeCard_le_add : pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) ≤ pc (N : ℝ) (a + (k : ℝ) ^ θ) + ((N : ℝ) + (N : ℝ) ^ θ - (a + (k : ℝ) ^ θ) + 1) := by convert primeCard_le_add ( N : ℝ ) ( a + ( k : ℝ ) ^ θ ) ( N + ( N : ℝ ) ^ θ ) _ using 1; exact add_le_add ( Nat.le_ceil _ ) ( Real.rpow_le_rpow ( by linarith ) ( by linarith ) ( by exact hθ0.le ) ); linarith;
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 163–167 at cd7163d4891e ↗
 s12.exists_prime_in_window.h_primeCard_le_add.h_primeCard_le_add have (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ) ≤ (↑(pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)) : ℝ) + ((↑N : ℝ) + (↑N : ℝ) ^ θ - (a + (↑k : ℝ) ^ θ) + (1 : ℝ))
 Leaves (↑(pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)) : ℝ) ≥ (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ) - ((↑N : ℝ) ^ θ - (↑k : ℝ) ^ θ + (2 : ℝ)), with h_primeCard_le_add : (↑(pc (↑N : ℝ) ((↑N : ℝ) + (↑N : ℝ) ^ θ)) : ℝ) ≤ (↑(pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)) : ℝ) + ((↑N : ℝ) + (↑N : ℝ) ^ θ - (a + (↑k : ℝ) ^ θ) + (1 : ℝ)).
 Uses library add_le_add, Nat.le_ceil, Real.rpow_le_rpow.
 Lean, lines 164–166
 have h_primeCard_le_add : pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) ≤ pc (N : ℝ) (a + (k : ℝ) ^ θ) + ((N : ℝ) + (N : ℝ) ^ θ - (a + (k : ℝ) ^ θ) + 1) := by convert primeCard_le_add ( N : ℝ ) ( a + ( k : ℝ ) ^ θ ) ( N + ( N : ℝ ) ^ θ ) _ using 1; exact add_le_add ( Nat.le_ceil _ ) ( Real.rpow_le_rpow ( by linarith ) ( by linarith ) ( by exact hθ0.le ) );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 164–166 at cd7163d4891e ↗
 s12.exists_prime_in_window.h_primeCard_pos have (0 : ℕ) < pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ, with h_primeCard_pos : (0 : ℕ) < pc (↑N : ℝ) (a + (↑k : ℝ) ^ θ).
 Uses library le_max_left, Max.max, le_max_right.
 Lean, lines 169–170
 have h_primeCard_pos : 0 < pc (N : ℝ) (a + (k : ℝ) ^ θ) := by exact_mod_cast ( by linarith [ hk₁ k ( by linarith [ le_max_left ( max k₀ k₁ ) 2, le_max_right ( max k₀ k₁ ) 2, le_max_left k₀ k₁, le_max_right k₀ k₁ ] ) N hN₄ hN₅ ] : ( 0 : ℝ ) < pc ( N : ℝ ) ( a + k ^ θ ) );
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 169–170 at cd7163d4891e ↗
2. s12.s2 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ
 Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with kw : ℕ, hw : ∀ (k : ℕ), kw ≤ k → ∀ (a : ℝ), (↑k : ℝ) ≤ a → a ≤ (↑k : ℝ) + (2 : ℝ) * (↑k : ℝ) ^ θ → ∃ (p : ℕ), Nat.Prime p ∧ a < (↑p : ℝ) ∧ (↑p : ℝ) < a + (↑k : ℝ) ^ θ.
 Lean, line 173
 obtain ⟨kw, hw⟩ := exists_prime_in_window
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 173 at cd7163d4891e ↗
3. s12.hk2 have (2 : ℕ) ≤ k
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hk2 : (2 : ℕ) ≤ k.
 Uses library le_trans, le_max_right.
 Lean, line 177
 have hk2 : 2 ≤ k := le_trans (le_max_right _ _) hk
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 177 at cd7163d4891e ↗
4. s12.hkw have kw ≤ k
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hkw : kw ≤ k.
 Uses library le_trans, le_max_left.
 Lean, line 178
 have hkw : kw ≤ k := le_trans (le_max_left _ _) hk
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 178 at cd7163d4891e ↗
5. s12.hk0 have (0 : ℝ) < (↑k : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hk0 : (0 : ℝ) < (↑k : ℝ).
 Lean, line 179
 have hk0 : (0 : ℝ) < k := by exact_mod_cast (show 0 < k by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 179 at cd7163d4891e ↗
6. s12.hk_x3b8 (hkθ) have (0 : ℝ) < (↑k : ℝ) ^ θ
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hkθ : (0 : ℝ) < (↑k : ℝ) ^ θ.
 Uses library Real.rpow_pos_of_pos.
 Lean, line 180
 have hkθ : (0 : ℝ) < (k : ℝ) ^ θ := Real.rpow_pos_of_pos hk0 _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 180 at cd7163d4891e ↗
7. s12.hN have (↑(n - (1 : ℤ)).natAbs : ℤ) = n - (1 : ℤ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hN : (↑(n - (1 : ℤ)).natAbs : ℤ) = n - (1 : ℤ).
 Uses library Int.natAbs_of_nonneg.
 Lean, line 181
 have hN : (((n - 1).natAbs : ℕ) : ℤ) = n - 1 := Int.natAbs_of_nonneg (by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 181 at cd7163d4891e ↗
8. s12.hm have (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hm : (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ).
 Lean, lines 183–189
 have hm : (m : ℤ) * k ≤ n - 1 ∧ n - 1 < ((m + 1) : ℤ) * k := by have h1 : k * m + (n - 1).natAbs % k = (n - 1).natAbs := Nat.div_add_mod _ _ have h2 : (n - 1).natAbs % k < k := Nat.mod_lt _ (by omega) have h3 : (k : ℤ) * m + (((n - 1).natAbs % k : ℕ) : ℤ) = n - 1 := by rw [← hN]; exact_mod_cast h1 have h4 : (((n - 1).natAbs % k : ℕ) : ℤ) < k := by exact_mod_cast h2 have h5 : (0 : ℤ) ≤ (((n - 1).natAbs % k : ℕ) : ℤ) := by positivity constructor <;> linarith
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 183–189 at cd7163d4891e ↗
 s12.hm.h1 have k * m + (n - (1 : ℤ)).natAbs % k = (n - (1 : ℤ)).natAbs
 Leaves (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ), with h1 : k * m + (n - (1 : ℤ)).natAbs % k = (n - (1 : ℤ)).natAbs.
 Uses library Nat.div_add_mod.
 Lean, line 184
 have h1 : k * m + (n - 1).natAbs % k = (n - 1).natAbs := Nat.div_add_mod _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 184 at cd7163d4891e ↗
 s12.hm.h2 have (n - (1 : ℤ)).natAbs % k < k
 Leaves (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ), with h2 : (n - (1 : ℤ)).natAbs % k < k.
 Uses library Nat.mod_lt.
 Lean, line 185
 have h2 : (n - 1).natAbs % k < k := Nat.mod_lt _ (by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 185 at cd7163d4891e ↗
 s12.hm.h3 have (↑k : ℤ) * (↑m : ℤ) + (↑((n - (1 : ℤ)).natAbs % k) : ℤ) = n - (1 : ℤ)
 Leaves (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ), with h3 : (↑k : ℤ) * (↑m : ℤ) + (↑((n - (1 : ℤ)).natAbs % k) : ℤ) = n - (1 : ℤ).
 Lean, line 186
 have h3 : (k : ℤ) * m + (((n - 1).natAbs % k : ℕ) : ℤ) = n - 1 := by rw [← hN]; exact_mod_cast h1
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 186 at cd7163d4891e ↗
 s12.hm.h4 have (↑((n - (1 : ℤ)).natAbs % k) : ℤ) < (↑k : ℤ)
 Leaves (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ), with h4 : (↑((n - (1 : ℤ)).natAbs % k) : ℤ) < (↑k : ℤ).
 Lean, line 187
 have h4 : (((n - 1).natAbs % k : ℕ) : ℤ) < k := by exact_mod_cast h2
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 187 at cd7163d4891e ↗
 s12.hm.h5 have (0 : ℤ) ≤ (↑((n - (1 : ℤ)).natAbs % k) : ℤ) routine: positivity
 Leaves (↑m : ℤ) * (↑k : ℤ) ≤ n - (1 : ℤ) ∧ n - (1 : ℤ) < ((↑m : ℤ) + (1 : ℤ)) * (↑k : ℤ), with h5 : (0 : ℤ) ≤ (↑((n - (1 : ℤ)).natAbs % k) : ℤ).
 Lean, line 188
 have h5 : (0 : ℤ) ≤ (((n - 1).natAbs % k : ℕ) : ℤ) := by positivity
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 188 at cd7163d4891e ↗
9. s12.hm_ge2 have (2 : ℕ) ≤ m
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hm_ge2 : (2 : ℕ) ≤ m.
 Uses library Nat.le_div_iff_mul_le.
 Lean, line 190
 have hm_ge2 : 2 ≤ m := (Nat.le_div_iff_mul_le (by omega)).2 (by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 190 at cd7163d4891e ↗
10. s12.hm2 have (2 : ℝ) ≤ (↑m : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hm2 : (2 : ℝ) ≤ (↑m : ℝ).
 Lean, line 191
 have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast hm_ge2
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 191 at cd7163d4891e ↗
11. s12.hmk have (↑m : ℝ) * (↑k : ℝ) ≤ (↑n : ℝ) - (1 : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hmk : (↑m : ℝ) * (↑k : ℝ) ≤ (↑n : ℝ) - (1 : ℝ).
 Lean, line 192
 have hmk : (m : ℝ) * k ≤ n - 1 := by exact_mod_cast hm.1
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 192 at cd7163d4891e ↗
12. s12.hmk2 have (↑n : ℝ) - (1 : ℝ) < ((↑m : ℝ) + (1 : ℝ)) * (↑k : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hmk2 : (↑n : ℝ) - (1 : ℝ) < ((↑m : ℝ) + (1 : ℝ)) * (↑k : ℝ).
 Lean, line 193
 have hmk2 : (n : ℝ) - 1 < ((m : ℝ) + 1) * k := by exact_mod_cast hm.2
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 193 at cd7163d4891e ↗
13. s12.hm_lt have (↑m : ℝ) < (1 / 2 : ℝ) * (↑k : ℝ) ^ ((1 : ℝ) - θ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hm_lt : (↑m : ℝ) < (1 / 2 : ℝ) * (↑k : ℝ) ^ ((1 : ℝ) - θ).
 Uses library Not, mul_le_mul_of_nonneg_right.
 Lean, lines 194–200
 have hm_lt : (m : ℝ) < (1 / 2) * (k : ℝ) ^ (1 - θ) := by have e : (k : ℝ) ^ ((2 : ℝ) - θ) = (k : ℝ) ^ (1 - θ) * k := by rw [show (2 : ℝ) - θ = (1 - θ) + 1 by ring, Real.rpow_add hk0, Real.rpow_one] rw [e] at hn2 by_contra hc push Not at hc linarith [mul_le_mul_of_nonneg_right hc hk0.le]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 194–200 at cd7163d4891e ↗
 s12.hm_lt.e have (↑k : ℝ) ^ ((2 : ℝ) - θ) = (↑k : ℝ) ^ ((1 : ℝ) - θ) * (↑k : ℝ)
 Leaves (↑m : ℝ) < (1 / 2 : ℝ) * (↑k : ℝ) ^ ((1 : ℝ) - θ), with e : (↑k : ℝ) ^ ((2 : ℝ) - θ) = (↑k : ℝ) ^ ((1 : ℝ) - θ) * (↑k : ℝ).
 Uses library Real.rpow_add, Real.rpow_one.
 Lean, lines 195–196
 have e : (k : ℝ) ^ ((2 : ℝ) - θ) = (k : ℝ) ^ (1 - θ) * k := by rw [show (2 : ℝ) - θ = (1 - θ) + 1 by ring, Real.rpow_add hk0, Real.rpow_one]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 195–196 at cd7163d4891e ↗
14. s12.hkey have ((2 : ℝ) * (↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑k : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hkey : ((2 : ℝ) * (↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑k : ℝ).
 Uses library Real.rpow_add'.
 Lean, lines 201–204
 have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) := by have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) ^ (1 - θ) * (k : ℝ) ^ θ := by exact mul_lt_mul_of_pos_right (by linarith) hkθ convert hkey using 1 ; rw [ ← Real.rpow_add' ] <;> norm_num
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 201–204 at cd7163d4891e ↗
 s12.hkey.hkey have ((2 : ℝ) * (↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑k : ℝ) ^ ((1 : ℝ) - θ) * (↑k : ℝ) ^ θ
 Leaves ((2 : ℝ) * (↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑k : ℝ), with hkey : ((2 : ℝ) * (↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑k : ℝ) ^ ((1 : ℝ) - θ) * (↑k : ℝ) ^ θ.
 Uses library mul_lt_mul_of_pos_right.
 Lean, lines 202–203
 have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) ^ (1 - θ) * (k : ℝ) ^ θ := by exact mul_lt_mul_of_pos_right (by linarith) hkθ
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 202–203 at cd7163d4891e ↗
15. s12.hdiv have ((↑m : ℝ) - (1 : ℝ)) * ((↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ) = (↑m : ℝ) * (↑k : ℝ) ^ θ
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hdiv : ((↑m : ℝ) - (1 : ℝ)) * ((↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ) = (↑m : ℝ) * (↑k : ℝ) ^ θ.
 Lean, lines 205–207
 have hdiv : ((m : ℝ) - 1) * ((m : ℝ) / (m - 1) * (k : ℝ) ^ θ) = m * (k : ℝ) ^ θ := by have : (m : ℝ) - 1 ≠ 0 := by linarith field_simp
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 205–207 at cd7163d4891e ↗
 s12.hdiv.this have (↑m : ℝ) - (1 : ℝ) ≠ (0 : ℝ) routine: linarith
 Leaves ((↑m : ℝ) - (1 : ℝ)) * ((↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ) = (↑m : ℝ) * (↑k : ℝ) ^ θ, with this : (↑m : ℝ) - (1 : ℝ) ≠ (0 : ℝ).
 Lean, line 206
 have : (m : ℝ) - 1 ≠ 0 := by linarith
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 206 at cd7163d4891e ↗
16. s12.hdiv2 have (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) ≤ (2 : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hdiv2 : (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) ≤ (2 : ℝ).
 Uses library div_le_iff₀.
 Lean, lines 208–209
 have hdiv2 : (m : ℝ) / (m - 1) ≤ 2 := by rw [div_le_iff₀ (by linarith)]; linarith
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 208–209 at cd7163d4891e ↗
17. s12.s17 case
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with h_case : (↑n : ℝ) < (↑m : ℝ) * (↑k : ℝ) + (↑m : ℝ) * (↑k : ℝ) ^ θ.
 Uses library Exists.intro.
 Lean, lines 211–223
 · obtain ⟨p, hp_prime, hp1, hp2⟩ := hw k hkw (k + (m : ℝ) / (m - 1) * (k : ℝ) ^ θ) (le_add_of_nonneg_right (mul_nonneg (div_nonneg (by positivity) (by linarith)) hkθ.le)) (by linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le]) have hpos : (0 : ℝ) < (m : ℝ) - 1 := by linarith have hA := mul_lt_mul_of_pos_left hp1 hpos have hB := mul_lt_mul_of_pos_left hp2 hpos refine ⟨p, hp_prime, ?_, ?_, ?_⟩ · linarith [mul_nonneg (div_nonneg (by positivity : (0:ℝ) ≤ m) hpos.le) hkθ.le] · linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le] · apply dvd_Pprod_of_mem k n p (((m : ℤ) - 1) * p) · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hA, hdiv, h_case] · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hB, hdiv, hkey, hmk] · exact dvd_mul_left _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 211–223 at cd7163d4891e ↗
 s12.s17.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ + (↑k : ℝ) ^ θ
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with p : ℕ, hp_prime : Nat.Prime p, hp1 : (↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ < (↑p : ℝ), hp2 : (↑p : ℝ) < (↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ + (↑k : ℝ) ^ θ.
 Uses library le_add_of_nonneg_right, mul_nonneg, div_nonneg, mul_le_mul_of_nonneg_right.
 Lean, lines 211–213
 · obtain ⟨p, hp_prime, hp1, hp2⟩ := hw k hkw (k + (m : ℝ) / (m - 1) * (k : ℝ) ^ θ) (le_add_of_nonneg_right (mul_nonneg (div_nonneg (by positivity) (by linarith)) hkθ.le)) (by linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le])
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 211–213 at cd7163d4891e ↗
 s12.s17.hpos have (0 : ℝ) < (↑m : ℝ) - (1 : ℝ) routine: linarith
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hpos : (0 : ℝ) < (↑m : ℝ) - (1 : ℝ).
 Lean, line 214
 have hpos : (0 : ℝ) < (m : ℝ) - 1 := by linarith
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 214 at cd7163d4891e ↗
 s12.s17.hA have ((↑m : ℝ) - (1 : ℝ)) * ((↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ) < ((↑m : ℝ) - (1 : ℝ)) * (↑p : ℝ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hA : ((↑m : ℝ) - (1 : ℝ)) * ((↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ) < ((↑m : ℝ) - (1 : ℝ)) * (↑p : ℝ).
 Uses library mul_lt_mul_of_pos_left.
 Lean, line 215
 have hA := mul_lt_mul_of_pos_left hp1 hpos
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 215 at cd7163d4891e ↗
 s12.s17.hB have ((↑m : ℝ) - (1 : ℝ)) * (↑p : ℝ) < ((↑m : ℝ) - (1 : ℝ)) * ((↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ + (↑k : ℝ) ^ θ)
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hB : ((↑m : ℝ) - (1 : ℝ)) * (↑p : ℝ) < ((↑m : ℝ) - (1 : ℝ)) * ((↑k : ℝ) + (↑m : ℝ) / ((↑m : ℝ) - (1 : ℝ)) * (↑k : ℝ) ^ θ + (↑k : ℝ) ^ θ).
 Uses library mul_lt_mul_of_pos_left.
 Lean, line 216
 have hB := mul_lt_mul_of_pos_left hp2 hpos
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 216 at cd7163d4891e ↗
 s12.s17.s5 case routine: linarith
 Leaves (↑k : ℝ) < (↑p : ℝ).
 Uses library mul_nonneg, div_nonneg.
 Lean, line 218
 · linarith [mul_nonneg (div_nonneg (by positivity : (0:ℝ) ≤ m) hpos.le) hkθ.le]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 218 at cd7163d4891e ↗
 s12.s17.s6 case routine: linarith
 Leaves (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ.
 Uses library mul_le_mul_of_nonneg_right.
 Lean, line 219
 · linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 219 at cd7163d4891e ↗
 s12.s17.s7 case
 Leaves (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).
 Lean, lines 220–223
 · apply dvd_Pprod_of_mem k n p (((m : ℤ) - 1) * p) · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hA, hdiv, h_case] · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hB, hdiv, hkey, hmk] · exact dvd_mul_left _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 220–223 at cd7163d4891e ↗
 s12.s17.s7.s1 case
 Leaves n - (↑k : ℤ) < ((↑m : ℤ) - (1 : ℤ)) * (↑p : ℤ).
 Uses library Int.cast_lt.
 Lean, line 221
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hA, hdiv, h_case]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 221 at cd7163d4891e ↗
 s12.s17.s7.s2 case
 Leaves ((↑m : ℤ) - (1 : ℤ)) * (↑p : ℤ) < n.
 Uses library Int.cast_lt.
 Lean, line 222
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hB, hdiv, hkey, hmk]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 222 at cd7163d4891e ↗
 s12.s17.s7.s3 case
 Leaves (↑p : ℤ) ∣ ((↑m : ℤ) - (1 : ℤ)) * (↑p : ℤ).
 Uses library dvd_mul_left.
 Lean, line 223
 · exact dvd_mul_left _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 223 at cd7163d4891e ↗
18. s12.s18 case
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with h_case : ¬(↑n : ℝ) < (↑m : ℝ) * (↑k : ℝ) + (↑m : ℝ) * (↑k : ℝ) ^ θ.
 Uses library Not, Exists.intro.
 Lean, lines 224–235
 · push Not at h_case obtain ⟨p, hp_prime, hp1, hp2⟩ : ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ p < (k : ℝ) + (k : ℝ) ^ θ := hw k hkw k le_rfl (by linarith) have hpk : k + 1 ≤ p := by exact_mod_cast hp1 refine ⟨p, hp_prime, hp1, by linarith, ?_⟩ have hmp : (m : ℝ) * p < m * ((k : ℝ) + (k : ℝ) ^ θ) := mul_lt_mul_of_pos_left hp2 (by linarith) apply dvd_Pprod_of_mem k n p ((m : ℤ) * p) · have : (m : ℤ) * (k + 1) ≤ m * p := mul_le_mul_of_nonneg_left (by exact_mod_cast hpk) (by positivity) have hm1 : (1 : ℤ) ≤ m := by exact_mod_cast (show 1 ≤ m by omega) linarith [hm.2] · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hmp, h_case] · exact dvd_mul_left _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 224–235 at cd7163d4891e ↗
 s12.s18.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with p : ℕ, hp_prime : Nat.Prime p, hp1 : (↑k : ℝ) < (↑p : ℝ), hp2 : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ.
 Uses library le_rfl.
 Lean, lines 225–226
 obtain ⟨p, hp_prime, hp1, hp2⟩ : ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ p < (k : ℝ) + (k : ℝ) ^ θ := hw k hkw k le_rfl (by linarith)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 225–226 at cd7163d4891e ↗
 s12.s18.hpk have k + (1 : ℕ) ≤ p
 Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hpk : k + (1 : ℕ) ≤ p.
 Lean, line 227
 have hpk : k + 1 ≤ p := by exact_mod_cast hp1
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 227 at cd7163d4891e ↗
 s12.s18.hmp have (↑m : ℝ) * (↑p : ℝ) < (↑m : ℝ) * ((↑k : ℝ) + (↑k : ℝ) ^ θ)
 Leaves (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hmp : (↑m : ℝ) * (↑p : ℝ) < (↑m : ℝ) * ((↑k : ℝ) + (↑k : ℝ) ^ θ).
 Uses library mul_lt_mul_of_pos_left.
 Lean, line 229
 have hmp : (m : ℝ) * p < m * ((k : ℝ) + (k : ℝ) ^ θ) := mul_lt_mul_of_pos_left hp2 (by linarith)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 229 at cd7163d4891e ↗
 s12.s18.s4 case
 Leaves n - (↑k : ℤ) < (↑m : ℤ) * (↑p : ℤ).
 Lean, lines 231–233
 · have : (m : ℤ) * (k + 1) ≤ m * p := mul_le_mul_of_nonneg_left (by exact_mod_cast hpk) (by positivity) have hm1 : (1 : ℤ) ≤ m := by exact_mod_cast (show 1 ≤ m by omega) linarith [hm.2]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 231–233 at cd7163d4891e ↗
 s12.s18.s4.this have (↑m : ℤ) * ((↑k : ℤ) + (1 : ℤ)) ≤ (↑m : ℤ) * (↑p : ℤ)
 Leaves n - (↑k : ℤ) < (↑m : ℤ) * (↑p : ℤ), with this : (↑m : ℤ) * ((↑k : ℤ) + (1 : ℤ)) ≤ (↑m : ℤ) * (↑p : ℤ).
 Uses library mul_le_mul_of_nonneg_left.
 Lean, line 231
 · have : (m : ℤ) * (k + 1) ≤ m * p := mul_le_mul_of_nonneg_left (by exact_mod_cast hpk) (by positivity)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 231 at cd7163d4891e ↗
 s12.s18.s4.hm1 have (1 : ℤ) ≤ (↑m : ℤ)
 Leaves n - (↑k : ℤ) < (↑m : ℤ) * (↑p : ℤ), with hm1 : (1 : ℤ) ≤ (↑m : ℤ).
 Lean, line 232
 have hm1 : (1 : ℤ) ≤ m := by exact_mod_cast (show 1 ≤ m by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 232 at cd7163d4891e ↗
 s12.s18.s5 case
 Leaves (↑m : ℤ) * (↑p : ℤ) < n.
 Uses library Int.cast_lt.
 Lean, line 234
 · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hmp, h_case]
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 234 at cd7163d4891e ↗
 s12.s18.s6 case
 Leaves (↑p : ℤ) ∣ (↑m : ℤ) * (↑p : ℤ).
 Uses library dvd_mul_left.
 Lean, line 235
 · exact dvd_mul_left _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, line 235 at cd7163d4891e ↗
s13 case
Leaves (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ θ⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ θ}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - θ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ θ ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with hB : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ θ / Real.log (↑k : ℝ) ≤ (↑(pc (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ θ)) : ℝ).
Uses library Exists.intro.
Lean, lines 236–238
```
 · left
 rintro ⟨C, hC, k₀, hk⟩
 exact hB ⟨C, hC, k₀, fun k hk' => by rw [hpc]; exact hk k hk'⟩
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean, lines 236–238 at cd7163d4891e ↗

The proof in Lean (Proof.lean)

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

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

import Mathlib
import Nodes.«erdos-1094--h2--h2--h2--h1».Context

open scoped Nat

/-! Hole `h_small` 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_1094__h2__h2__h2__h1 : (¬∃ (C : ℝ),
      (0 : ℝ) < C ∧
        ∃ (k₀ : ℕ),
          ∀ (k : ℕ),
            k₀ ≤ k →
              C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
                (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                        (0 : ℤ) < p ∧
                          Nat.Prime p.natAbs ∧
                            (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
                  ℝ)) ∨
  ∃ (k₀ : ℕ),
    ∀ (k : ℕ),
      k₀ ≤ k →
        ∀ (n : ℤ),
          (2 : ℤ) * (↑k : ℤ) < n →
            (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) →
              ∃ (p : ℕ),
                Nat.Prime p ∧
                  (↑k : ℝ) < (↑p : ℝ) ∧
                    (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
                      (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
  generalize hθ : (21 / 40 : ℝ) = θ
  have hθ0 : (0 : ℝ) < θ := by rw [← hθ]; norm_num
  have hθ1 : θ < 1 := by rw [← hθ]; norm_num
  clear hθ
  obtain ⟨pc, hpc⟩ : ∃ pc : ℝ → ℝ → ℕ, ∀ a b : ℝ, pc a b = ((Finset.Ioo ⌊a⌋ ⌈b⌉).filter (fun p : ℤ => 0 < p ∧ (p.natAbs).Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < b)).card := ⟨_, fun _ _ => rfl⟩
  have primeCard_le_add : ∀ (a b c : ℝ), b ≤ c → (pc a c : ℝ) ≤ (pc a b : ℝ) + (c - b + 1) := by
    intro a b c hbc; rw [hpc, hpc]; clear hpc hθ0 hθ1
    -- Let S(t) := (Finset.Ioo ⌊a⌋ ⌈t⌉).filter (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ a < (p:ℝ) ∧ (p:ℝ) < t).
    set S := fun t : ℝ => Finset.filter (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < t) (Finset.Ioo ⌊a⌋ ⌈t⌉);
    -- Show `S(c) ⊆ S(b) ∪ Finset.Ico ⌈b⌉ ⌈c⌉`.
    have h_subset : S c ⊆ S b ∪ Finset.Ico ⌈b⌉ ⌈c⌉ := by
      intro p hp; by_cases h : ( p : ℝ ) < b <;> simp_all +decide ;
      · exact Or.inl <| Finset.mem_filter.mpr ⟨ Finset.mem_Ioo.mpr ⟨ Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.1, Int.lt_ceil.mpr h ⟩, Finset.mem_filter.mp hp |>.2.1, Finset.mem_filter.mp hp |>.2.2.1, Finset.mem_filter.mp hp |>.2.2.2.1, h ⟩;
      · exact Or.inr ⟨ Int.ceil_le.mpr h, Finset.mem_Ioo.mp ( Finset.mem_filter.mp hp |>.1 ) |>.2 ⟩;
    -- Thus by `Finset.card_le_card` and `Finset.card_union_le`, `S(c).card ≤ S(b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card`.
    have h_card : (S c).card ≤ (S b).card + (Finset.Ico ⌈b⌉ ⌈c⌉).card := by
      exact le_trans ( Finset.card_le_card h_subset ) ( Finset.card_union_le _ _ );
    have hI : ((Finset.Ico ⌈b⌉ ⌈c⌉).card : ℝ) ≤ c - b + 1 := by
      rw [Int.card_Ico]
      have h0 : (0 : ℤ) ≤ ⌈c⌉ - ⌈b⌉ := sub_nonneg.mpr (Int.ceil_mono hbc)
      have h1 : (((⌈c⌉ - ⌈b⌉).toNat : ℕ) : ℝ) = ((⌈c⌉ - ⌈b⌉ : ℤ) : ℝ) := by
        rw [← Int.cast_natCast, Int.toNat_of_nonneg h0]
      rw [h1]
      push_cast
      linarith [Int.ceil_lt_add_one c, Int.le_ceil b]
    refine le_trans (Nat.cast_le.mpr h_card) ?_
    push_cast
    linarith [hI]
  have exists_prime_of_primeCard_pos : ∀ (a b : ℝ), 0 < pc a b → ∃ p : ℕ, p.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < b := by
    intro a b h; rw [hpc] at h; clear hpc
    obtain ⟨ p, hp ⟩ := Finset.card_pos.mp h;
    cases p <;> aesop
  have tendsto_log_rpow_mul_rpow_neg : ∀ (b c : ℝ), 0 < c → Filter.Tendsto (fun x : ℝ => (Real.log x) ^ b * x ^ (-c)) Filter.atTop (nhds 0) := by
    intro b c hc
    -- Use the fact that `Real.log x ^ b` is little-o of `x ^ c` as `x` tends to infinity.
    have h_log : (fun x : ℝ => Real.log x ^ b) =o[Filter.atTop] (fun x : ℝ => x ^ c) :=
      isLittleO_log_rpow_rpow_atTop b hc
    convert h_log.tendsto_div_nhds_zero.congr' _ using 1;
    filter_upwards [ Filter.eventually_gt_atTop 0 ] with x hx using by rw [ div_eq_mul_inv, Real.rpow_neg hx.le ] ;
  have poly_log_lt : ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), 0 < C → ∀ᶠ k : ℕ in Filter.atTop, A * (k : ℝ) ^ α * (Real.log k) ^ β ≤ C * (k : ℝ) ^ tt / Real.log k := by
    intro A α β tt hα C hC
    -- Let's choose any $C > 0$ and derive a contradiction.
    have h_lim : Filter.Tendsto (fun k : ℕ => (A * (k : ℝ) ^ α * (Real.log k) ^ β) / ((k : ℝ) ^ tt / (Real.log k))) Filter.atTop (nhds 0) := by
      -- Simplify the expression inside the limit.
      suffices h_simp : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1) * (k : ℝ) ^ (α - tt)) Filter.atTop (nhds 0) by
        refine h_simp.congr' ?_;
        filter_upwards [ Filter.eventually_gt_atTop 1 ] with k hk ; rw [ Real.rpow_sub ( by positivity ) ] ; ring_nf;
        rw [ Real.rpow_add ( Real.log_pos ( Nat.one_lt_cast.mpr hk ) ), Real.rpow_one ] ; norm_num ; ring;
      have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_;
      · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring;
      · linarith;
    filter_upwards [ h_lim.eventually ( gt_mem_nhds hC ), Filter.eventually_gt_atTop 1 ] with k hk₁ hk₂;
    rw [ div_lt_iff₀ ( div_pos ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr hk₂.le ) _ ) ( Real.log_pos ( Nat.one_lt_cast.mpr hk₂ ) ) ) ] at hk₁ ; ring_nf at hk₁ ⊢ ; linarith
  have excess_le : ∀ (k N : ℕ), 1 ≤ k → (k : ℝ) ≤ (N : ℝ) → (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 → (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by
    intro k N hk hkN hNk
    -- Subexcess bound: `(N:ℝ)^θ - (k:ℝ)^θ ≤ ((N:ℝ) - k)^θ`
    have h_subex : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ ((N : ℝ) - k) ^ θ := by
      rw [ sub_le_iff_le_add' ];
      convert Real.rpow_add_le_add_rpow _ _ _ _ using 1 <;> norm_num;
      · exact_mod_cast hkN;
      · exact hθ0.le;
      · exact le_of_lt hθ1;
    refine le_trans h_subex ?_;
    refine' le_trans ( Real.rpow_le_rpow ( sub_nonneg.mpr hkN ) ( show ( N : ℝ ) - k ≤ 3 * ( k : ℝ ) ^ θ by linarith [ show ( k : ℝ ) ^ θ ≥ 1 by exact Real.one_le_rpow ( by norm_cast ) ( by exact hθ0.le ) ] ) ( hθ0.le ) ) _;
    rw [ Real.mul_rpow ( by positivity ) ( by positivity ), ← Real.rpow_mul ( by positivity ) ]
  have count_beats_excess : ∀ (C : ℝ), 0 < C → ∀ᶠ k : ℕ in Filter.atTop, ∀ N : ℕ, (k : ℝ) ≤ (N : ℝ) → (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 → (N : ℝ) ^ θ - (k : ℝ) ^ θ + 2 < C * (N : ℝ) ^ θ / Real.log N := by
    intro C hC; clear primeCard_le_add exists_prime_of_primeCard_pos tendsto_log_rpow_mul_rpow_neg hpc
    -- Step 1: produce a purely-k bound and then specialize to N.
    have step1 : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) + 3 ≤ (C / 2) * (k : ℝ) ^ θ / Real.log k := by
      -- Apply `poly_log_lt` to each term separately.
      have hA : ∀ᶠ k : ℕ in Filter.atTop, (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by
        have := poly_log_lt ( ( 3 : ℝ ) ^ θ ) ( θ * θ ) 0 θ ( by nlinarith [ show 0 < θ by exact hθ0, show θ < 1 by exact hθ1 ] ) ( C / 4 ) ( by positivity );
        aesop
      have hB : ∀ᶠ k : ℕ in Filter.atTop, 3 ≤ (C / 4) * (k : ℝ) ^ θ / Real.log k := by
        have := poly_log_lt ( 3 : ℝ ) 0 0 θ hθ0 ( C / 4 ) ( by positivity ) ; aesop;
      filter_upwards [ hA, hB ] with k hk₁ hk₂ using by ring_nf at hk₁ hk₂ ⊢; linarith;
    -- Step 2: Filter_upwards on [step1, eventually_ge_atTop 4] with k, hkA, hk4.
    filter_upwards [step1, Filter.eventually_ge_atTop 4] with k hkA hk4;
    intro N hkN hNk
    have hN_le_4k : (N : ℝ) ≤ 4 * (k : ℝ) := by
      linarith [ show ( k : ℝ ) ^ θ ≤ k by exact le_trans ( Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) <| show θ ≤ 1 by exact le_of_lt <| hθ1 ) <| by norm_num, show ( k : ℝ ) ≥ 4 by norm_cast ]
    have h_logN_le_2logk : Real.log (N : ℝ) ≤ 2 * Real.log (k : ℝ) := by
      erw [ ← Real.log_pow ] ; gcongr ; norm_cast at *;
      · linarith;
      · norm_cast at *; nlinarith;
    have h_logN_pos : 0 < Real.log (N : ℝ) := by
      exact Real.log_pos <| by norm_cast at *; linarith;
    have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ + 2 < (C / 2) * (k : ℝ) ^ θ / Real.log k := by
      have h_exp_bound : (N : ℝ) ^ θ - (k : ℝ) ^ θ ≤ (3 : ℝ) ^ θ * (k : ℝ) ^ (θ * θ) := by
        apply excess_le k N (by linarith) hkN hNk;
      linarith
    have h_rhs_bound : (C / 2) * (k : ℝ) ^ θ / Real.log k ≤ C * (N : ℝ) ^ θ / Real.log N := by
      rw [ div_le_div_iff₀ ] <;> try positivity;
      · have h_rhs_bound : (k : ℝ) ^ θ * Real.log N ≤ 2 * (N : ℝ) ^ θ * Real.log k := by
          have h_rhs_bound : (k : ℝ) ^ θ ≤ (N : ℝ) ^ θ := by
            exact Real.rpow_le_rpow ( by positivity ) hkN ( by exact hθ0.le );
          nlinarith [ Real.rpow_pos_of_pos ( by positivity : 0 < ( k : ℝ ) ) θ ];
        nlinarith;
      · exact Real.log_pos <| by norm_cast; linarith;
    linarith [h_exp_bound, h_rhs_bound]
  have dvd_Pprod_of_factor : ∀ (k : ℕ) (n : ℤ) (p : ℤ) (i : ℕ), i ∈ Finset.Icc 1 k → p ∣ (n - (i : ℤ)) → p ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
    intro k n p i hi hp
    exact hp.trans (Finset.dvd_prod_of_mem (fun i : ℕ => (n - (i : ℤ))) hi)
  have dvd_Pprod_of_mem : ∀ (k : ℕ) (n : ℤ) (p : ℤ) (t : ℤ), n - (k : ℤ) < t → t < n → p ∣ t → p ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
    intro k n p t h1 h2 hpt
    convert dvd_Pprod_of_factor k n p ( Int.toNat ( n - t ) ) ?_ ?_ using 1 <;> norm_num [ Int.toNat_of_nonneg ( sub_nonneg.mpr h2.le ) ];
    · omega;
    · assumption
  by_cases hB : ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → C * (k : ℝ) ^ θ / Real.log k ≤ (pc (k : ℝ) ((k : ℝ) + (k : ℝ) ^ θ) : ℝ)
  · right
    have exists_prime_in_window : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ a : ℝ, (k : ℝ) ≤ a → a ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ → ∃ p : ℕ, p.Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < a + (k : ℝ) ^ θ := by
      clear tendsto_log_rpow_mul_rpow_neg poly_log_lt excess_le dvd_Pprod_of_factor dvd_Pprod_of_mem hpc
      obtain ⟨ C, hC, k₀, hk₀ ⟩ := hB;
      -- Choose `k₀' := max (max k₀ k₁) 2`.
      obtain ⟨ k₁, hk₁ ⟩ := Filter.eventually_atTop.mp (count_beats_excess C hC)
      use max (max k₀ k₁) 2;
      intros k hk a ha₁ ha₂
      set N := ⌈a⌉₊ with hN
      have hN₁ : (k : ℝ) ≤ (N : ℝ) := by
        exact_mod_cast ha₁.trans <| Nat.le_ceil _
      have hN₂ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by
        exact le_trans ( Nat.ceil_lt_add_one ( by linarith ) |> le_of_lt ) ( by linarith )
      have hN₃ : (N : ℝ) < a + 1 := by
        exact Nat.ceil_lt_add_one ( by linarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith [ le_max_right ( max k₀ k₁ ) 2 ] ] )
      have hN₄ : (k : ℝ) ≤ N := by
        exact_mod_cast hN₁
      have hN₅ : (N : ℝ) ≤ (k : ℝ) + 2 * (k : ℝ) ^ θ + 1 := by
        convert hN₂ using 1;
      -- Apply `hk₀` to get `bhpN : C*(N:ℝ)^θ/Real.log N ≤ pc (N:ℝ) ((N:ℝ)+(N:ℝ)^θ)`.
      have h_bhpN : C * (N : ℝ) ^ θ / Real.log N ≤ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) := by
        exact hk₀ N ( by norm_cast at *; linarith [ Nat.le_max_left ( max k₀ k₁ ) 2, Nat.le_max_right ( max k₀ k₁ ) 2, Nat.le_max_left k₀ k₁, Nat.le_max_right k₀ k₁ ] );
      -- Apply `primeCard_le_add` to bound the prime count in `(N, a + k^θ)`.
      have h_primeCard_le_add : pc (N : ℝ) (a + (k : ℝ) ^ θ) ≥ pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) - ((N : ℝ) ^ θ - (k : ℝ) ^ θ + 2) := by
        have h_primeCard_le_add : pc (N : ℝ) ((N : ℝ) + (N : ℝ) ^ θ) ≤ pc (N : ℝ) (a + (k : ℝ) ^ θ) + ((N : ℝ) + (N : ℝ) ^ θ - (a + (k : ℝ) ^ θ) + 1) := by
          convert primeCard_le_add ( N : ℝ ) ( a + ( k : ℝ ) ^ θ ) ( N + ( N : ℝ ) ^ θ ) _ using 1;
          exact add_le_add ( Nat.le_ceil _ ) ( Real.rpow_le_rpow ( by linarith ) ( by linarith ) ( by exact hθ0.le ) );
        linarith;
      -- Therefore, `pc (N:ℝ) (a + k^θ) > 0`.
      have h_primeCard_pos : 0 < pc (N : ℝ) (a + (k : ℝ) ^ θ) := by
        exact_mod_cast ( by linarith [ hk₁ k ( by linarith [ le_max_left ( max k₀ k₁ ) 2, le_max_right ( max k₀ k₁ ) 2, le_max_left k₀ k₁, le_max_right k₀ k₁ ] ) N hN₄ hN₅ ] : ( 0 : ℝ ) < pc ( N : ℝ ) ( a + k ^ θ ) );
      exact exists_prime_of_primeCard_pos _ _ h_primeCard_pos |> fun ⟨ p, hp₁, hp₂, hp₃ ⟩ => ⟨ p, hp₁, by linarith [ Nat.le_ceil a, show ( p : ℝ ) ≥ N by exact_mod_cast hp₂.le ], hp₃ ⟩
    clear tendsto_log_rpow_mul_rpow_neg poly_log_lt excess_le count_beats_excess primeCard_le_add exists_prime_of_primeCard_pos dvd_Pprod_of_factor hB hpc
    obtain ⟨kw, hw⟩ := exists_prime_in_window
    clear pc
    use max kw 2
    intro k hk n hn1 hn2
    have hk2 : 2 ≤ k := le_trans (le_max_right _ _) hk
    have hkw : kw ≤ k := le_trans (le_max_left _ _) hk
    have hk0 : (0 : ℝ) < k := by exact_mod_cast (show 0 < k by omega)
    have hkθ : (0 : ℝ) < (k : ℝ) ^ θ := Real.rpow_pos_of_pos hk0 _
    have hN : (((n - 1).natAbs : ℕ) : ℤ) = n - 1 := Int.natAbs_of_nonneg (by omega)
    set m := (n - 1).natAbs / k with hmdef
    have hm : (m : ℤ) * k ≤ n - 1 ∧ n - 1 < ((m + 1) : ℤ) * k := by
      have h1 : k * m + (n - 1).natAbs % k = (n - 1).natAbs := Nat.div_add_mod _ _
      have h2 : (n - 1).natAbs % k < k := Nat.mod_lt _ (by omega)
      have h3 : (k : ℤ) * m + (((n - 1).natAbs % k : ℕ) : ℤ) = n - 1 := by rw [← hN]; exact_mod_cast h1
      have h4 : (((n - 1).natAbs % k : ℕ) : ℤ) < k := by exact_mod_cast h2
      have h5 : (0 : ℤ) ≤ (((n - 1).natAbs % k : ℕ) : ℤ) := by positivity
      constructor <;> linarith
    have hm_ge2 : 2 ≤ m := (Nat.le_div_iff_mul_le (by omega)).2 (by omega)
    have hm2 : (2 : ℝ) ≤ m := by exact_mod_cast hm_ge2
    have hmk : (m : ℝ) * k ≤ n - 1 := by exact_mod_cast hm.1
    have hmk2 : (n : ℝ) - 1 < ((m : ℝ) + 1) * k := by exact_mod_cast hm.2
    have hm_lt : (m : ℝ) < (1 / 2) * (k : ℝ) ^ (1 - θ) := by
      have e : (k : ℝ) ^ ((2 : ℝ) - θ) = (k : ℝ) ^ (1 - θ) * k := by
        rw [show (2 : ℝ) - θ = (1 - θ) + 1 by ring, Real.rpow_add hk0, Real.rpow_one]
      rw [e] at hn2
      by_contra hc
      push Not at hc
      linarith [mul_le_mul_of_nonneg_right hc hk0.le]
    have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) := by
      have hkey : (2 * (m : ℝ) - 1) * (k : ℝ) ^ θ < (k : ℝ) ^ (1 - θ) * (k : ℝ) ^ θ := by
        exact mul_lt_mul_of_pos_right (by linarith) hkθ
      convert hkey using 1 ; rw [ ← Real.rpow_add' ] <;> norm_num
    have hdiv : ((m : ℝ) - 1) * ((m : ℝ) / (m - 1) * (k : ℝ) ^ θ) = m * (k : ℝ) ^ θ := by
      have : (m : ℝ) - 1 ≠ 0 := by linarith
      field_simp
    have hdiv2 : (m : ℝ) / (m - 1) ≤ 2 := by
      rw [div_le_iff₀ (by linarith)]; linarith
    by_cases h_case : (n : ℝ) < (m : ℝ) * k + (m : ℝ) * (k : ℝ) ^ θ
    · obtain ⟨p, hp_prime, hp1, hp2⟩ := hw k hkw (k + (m : ℝ) / (m - 1) * (k : ℝ) ^ θ)
        (le_add_of_nonneg_right (mul_nonneg (div_nonneg (by positivity) (by linarith)) hkθ.le))
        (by linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le])
      have hpos : (0 : ℝ) < (m : ℝ) - 1 := by linarith
      have hA := mul_lt_mul_of_pos_left hp1 hpos
      have hB := mul_lt_mul_of_pos_left hp2 hpos
      refine ⟨p, hp_prime, ?_, ?_, ?_⟩
      · linarith [mul_nonneg (div_nonneg (by positivity : (0:ℝ) ≤ m) hpos.le) hkθ.le]
      · linarith [mul_le_mul_of_nonneg_right hdiv2 hkθ.le]
      · apply dvd_Pprod_of_mem k n p (((m : ℤ) - 1) * p)
        · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hA, hdiv, h_case]
        · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hB, hdiv, hkey, hmk]
        · exact dvd_mul_left _ _
    · push Not at h_case
      obtain ⟨p, hp_prime, hp1, hp2⟩ : ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ p < (k : ℝ) + (k : ℝ) ^ θ :=
        hw k hkw k le_rfl (by linarith)
      have hpk : k + 1 ≤ p := by exact_mod_cast hp1
      refine ⟨p, hp_prime, hp1, by linarith, ?_⟩
      have hmp : (m : ℝ) * p < m * ((k : ℝ) + (k : ℝ) ^ θ) := mul_lt_mul_of_pos_left hp2 (by linarith)
      apply dvd_Pprod_of_mem k n p ((m : ℤ) * p)
      · have : (m : ℤ) * (k + 1) ≤ m * p := mul_le_mul_of_nonneg_left (by exact_mod_cast hpk) (by positivity)
        have hm1 : (1 : ℤ) ≤ m := by exact_mod_cast (show 1 ≤ m by omega)
        linarith [hm.2]
      · rw [← @Int.cast_lt ℝ]; push_cast; linarith [hmp, h_case]
      · exact dvd_mul_left _ _
  · left
    rintro ⟨C, hC, k₀, hk⟩
    exact hB ⟨C, hC, k₀, fun k hk' => by rw [hpc]; exact hk k hk'⟩

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-1094--h2--h2--h2--h1».Context

open scoped Nat

/-! Hole `h_small` 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_1094__h2__h2__h2__h1 : (¬∃ (C : ℝ),
      (0 : ℝ) < C ∧
        ∃ (k₀ : ℕ),
          ∀ (k : ℕ),
            k₀ ≤ k →
              C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
                (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                        (0 : ℤ) < p ∧
                          Nat.Prime p.natAbs ∧
                            (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
                  ℝ)) ∨
  ∃ (k₀ : ℕ),
    ∀ (k : ℕ),
      k₀ ≤ k →
        ∀ (n : ℤ),
          (2 : ℤ) * (↑k : ℤ) < n →
            (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) →
              ∃ (p : ℕ),
                Nat.Prime p ∧
                  (↑k : ℝ) < (↑p : ℝ) ∧
                    (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
                      (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := 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/e8b9c5caada8….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Statement.lean. Origin: skeleton-hole.

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000524.json.

Submitter: t1014-p
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (intermediate)

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/000524.json, merge commit cd7163d4891e.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Witness.lean, sha256 1aa8a1c1b9f3.

import Mathlib

open scoped Nat

theorem witness : True := trivial

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 →