FormalConjectures.ErdosProblems.«456»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 456

References:

erdosproblems.com/456

[Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73--82.

open Nat Filteropen scoped Topology Asymptoticsnamespace Erdos456

Let $p_n$ be the smallest prime $\equiv 1\pmod{n}$.

noncomputable def p (n : ℕ) : ℕ :=
  sInf { k | k.Prime ∧ k ≡ 1 [MOD n] }

Let $m_n$ be the smallest integer such that $n\mid \phi(m_n)$.

noncomputable def m (n : ℕ) : ℕ :=
  sInf { k | 0 < k ∧ n ∣ totient k }

open scoped Classical in

Is it true that $m_n<p_n$ for almost all $n$?

@[category research open, AMS 11]
theorem erdos_456.parts.i :
    answer(sorry) ↔
      Tendsto (fun N ↦ (count (fun n ↦ m n < p n) N : ℝ) / (N : ℝ)) atTop (𝓝 1) := by⊢ True ↔ Tendsto (fun N ↦ ↑(count (fun n ↦ m n < p n) N) / ↑N) atTop (𝓝 1)
  sorryAll goals completed! 🐙

open scoped Classical in

Does $p_n/m_n \to \infty$ for almost all $n$?

@[category research open, AMS 11]
theorem erdos_456.parts.ii :
    answer(sorry) ↔
      ∃ A : Set ℕ, Tendsto (fun N ↦ (count (· ∈ A) N : ℝ) / (N : ℝ)) atTop (𝓝 1) ∧
        Tendsto (fun n ↦ (p n : ℝ) / (m n : ℝ)) (atTop ⊓ 𝓟 A) atTop := by⊢ True ↔
  ∃ A,
    Tendsto (fun N ↦ ↑(count (fun x ↦ x ∈ A) N) / ↑N) atTop (𝓝 1) ∧
      Tendsto (fun n ↦ ↑(p n) / ↑(m n)) (atTop ⊓ 𝓟 A) atTop
  sorryAll goals completed! 🐙

Are there infinitely many primes $p$ such that $p-1$ is the only $n$ for which $m_n=p$?

@[category research open, AMS 11]
theorem erdos_456.parts.iii :
    answer(sorry) ↔
      { q | q.Prime ∧ ∀ n, m n = q ↔ n = q - 1 }.Infinite := by⊢ True ↔ {q | Nat.Prime q ∧ ∀ (n : ℕ), m n = q ↔ n = q - 1}.Infinite
  sorryAll goals completed! 🐙

Linnik's theorem implies that $p_n\leq n^{O(1)}$.

@[category research solved, AMS 11]
theorem erdos_456.variants.linniks_theorem :
    ∃ L : ℝ, (fun n ↦ (p n : ℝ)) =O[atTop] (fun n ↦ (n : ℝ) ^ L) := by⊢ ∃ L, (fun n ↦ ↑(p n)) =O[atTop] fun n ↦ ↑n ^ L
  sorryAll goals completed! 🐙

It is trivial that $m_n \leq p_n$ always.


@[category textbook, AMS 11]
theorem erdos_456.variants.mn_leq_pn (n : ℕ) :
    m n ≤ p n := byn:ℕ⊢ m n ≤ p n
  unfold m pn:ℕ⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
  rcases eq_or_ne n 0 with hn | hninln:ℕhn:n = 0⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}inrn:ℕhn:n ≠ 0⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
  ·inln:ℕhn:n = 0⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} subst hninl⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
    have hempty : {k | 0 < k ∧ (0 : ℕ) ∣ totient k} = (∅ : Set ℕ) := byn:ℕ⊢ m n ≤ p ninlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      ext kk:ℕ⊢ k ∈ {k | 0 < k ∧ 0 ∣ φ k} ↔ k ∈ ∅inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_and]k:ℕ⊢ 0 < k → ¬0 ∣ φ kinlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      intro hkk:ℕhk:0 < k⊢ ¬0 ∣ φ kinlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      rw [zero_dvd_iffk:ℕhk:0 < k⊢ ¬φ k = 0k:ℕhk:0 < k⊢ ¬φ k = 0inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}]k:ℕhk:0 < k⊢ ¬φ k = 0inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      have := Nat.totient_pos.mpr hkk:ℕhk:0 < kthis:0 < φ k⊢ ¬φ k = 0inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
      omegainlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf {k | 0 < k ∧ 0 ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
    rw [hempty,inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ sInf ∅ ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ 0 ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]} Nat.sInf_emptyinlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ 0 ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ 0 ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}]inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅⊢ 0 ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD 0]}
    exact Nat.zero_le _All goals completed! 🐙
  ·inrn:ℕhn:n ≠ 0⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} have hne : {k | k.Prime ∧ k ≡ 1 [MOD n]}.Nonempty := byn:ℕ⊢ m n ≤ p ninrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
      obtain ⟨q, _, hq, hmod⟩ :=
        Nat.forall_exists_prime_gt_and_modEq 0 hn (Nat.coprime_one_left n)n:ℕhn:n ≠ 0q:ℕleft✝:q > 0hq:Nat.Prime qhmod:q ≡ 1 [MOD n]⊢ {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyinrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
      exact ⟨q, hq, hmod⟩inrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}inrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
    obtain ⟨hp, hmod⟩ := Nat.sInf_mem hneinrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ sInf {k | 0 < k ∧ n ∣ φ k} ≤ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]}
    apply Nat.sInf_leinrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ∈ {k | 0 < k ∧ n ∣ φ k}
    refine ⟨hp.pos, ?_⟩inrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ n ∣ φ (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})
    rw [Nat.totient_prime hpinrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ n ∣ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} - 1inrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ n ∣ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} - 1]inrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonemptyhp:Nat.Prime (sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]})hmod:sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} ≡ 1 [MOD n]⊢ n ∣ sInf {k | Nat.Prime k ∧ k ≡ 1 [MOD n]} - 1
    exact (Nat.modEq_iff_dvd' hp.pos).mp hmod.symmAll goals completed! 🐙

Erdős [Er79e] writes it is 'easy to show' that for infinitely many $n$ we have $m_n < p_n$.


@[category research solved, AMS 11]
theorem erdos_456.variants.infinitely_many_n :
    { n | m n < p n }.Infinite := by⊢ {n | m n < p n}.Infinite
  apply Set.infinite_of_injective_forall_mem (f := fun j : ℕ ↦ 2 ^ (2 * j + 3))hi⊢ Function.Injective fun j ↦ 2 ^ (2 * j + 3)hf⊢ ∀ (x : ℕ), 2 ^ (2 * x + 3) ∈ {n | m n < p n}
  ·hi⊢ Function.Injective fun j ↦ 2 ^ (2 * j + 3) intro a b habhia:ℕb:ℕhab:(fun j ↦ 2 ^ (2 * j + 3)) a = (fun j ↦ 2 ^ (2 * j + 3)) b⊢ a = b
    apply Nat.pow_right_injective (bya:ℕb:ℕhab:(fun j ↦ 2 ^ (2 * j + 3)) a = (fun j ↦ 2 ^ (2 * j + 3)) b⊢ 2 ≤ 2 decideAll goals completed! 🐙) at hab
    omegaAll goals completed! 🐙
  ·hf⊢ ∀ (x : ℕ), 2 ^ (2 * x + 3) ∈ {n | m n < p n} intro jhfj:ℕ⊢ 2 ^ (2 * j + 3) ∈ {n | m n < p n}
    let k := 2 * j + 3hfj:ℕk:ℕ := 2 * j + 3⊢ 2 ^ (2 * j + 3) ∈ {n | m n < p n}
    -- Witness n = 2^k for odd k ≥ 3; then m(n) ≤ 2n, while 3 ∣ n + 1 forces p(n) > 2n.
    change m (2 ^ k) < p (2 ^ k)hfj:ℕk:ℕ := 2 * j + 3⊢ m (2 ^ k) < p (2 ^ k)
    have hm : m (2 ^ k) ≤ 2 ^ (k + 1) := by⊢ {n | m n < p n}.Infinitehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k)
      unfold mj:ℕk:ℕ := 2 * j + 3⊢ sInf {k_1 | 0 < k_1 ∧ 2 ^ k ∣ φ k_1} ≤ 2 ^ (k + 1)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k)
      refine Nat.sInf_le ⟨byj:ℕk:ℕ := 2 * j + 3⊢ 0 < 2 ^ (k + 1)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k) positivityAll goals completed! 🐙hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k), ?_⟩
      rw [Nat.totient_prime_pow Nat.prime_two (byj:ℕk:ℕ := 2 * j + 3⊢ 0 < k + 1j:ℕk:ℕ := 2 * j + 3⊢ 2 ^ k ∣ 2 ^ (k + 1 - 1) * (2 - 1)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k) omegaAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3⊢ 2 ^ k ∣ 2 ^ (k + 1 - 1) * (2 - 1)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k))]j:ℕk:ℕ := 2 * j + 3⊢ 2 ^ k ∣ 2 ^ (k + 1 - 1) * (2 - 1)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k)
      norm_numhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ m (2 ^ k) < p (2 ^ k)
    have hp : 2 ^ (k + 1) + 1 ≤ p (2 ^ k) := by⊢ {n | m n < p n}.Infinitehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      unfold pj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)⊢ 2 ^ (k + 1) + 1 ≤ sInf {k_1 | Nat.Prime k_1 ∧ k_1 ≡ 1 [MOD 2 ^ k]}hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      let q := sInf {x | x.Prime ∧ x ≡ 1 [MOD 2 ^ k]}j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}⊢ 2 ^ (k + 1) + 1 ≤ sInf {k_1 | Nat.Prime k_1 ∧ k_1 ≡ 1 [MOD 2 ^ k]}hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      change 2 ^ (k + 1) + 1 ≤ qj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hne : {x | x.Prime ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := by⊢ {n | m n < p n}.Infinitej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        obtain ⟨r, _, hr, hmod⟩ := Nat.forall_exists_prime_gt_and_modEq 0
          (pow_ne_zero k (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}⊢ 2 ≠ 0j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}r:ℕleft✝:r > 0hr:Nat.Prime rhmod:r ≡ 1 [MOD 2 ^ k]⊢ {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) decideAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}r:ℕleft✝:r > 0hr:Nat.Prime rhmod:r ≡ 1 [MOD 2 ^ k]⊢ {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k))) (Nat.coprime_one_left (2 ^ k))j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}r:ℕleft✝:r > 0hr:Nat.Prime rhmod:r ≡ 1 [MOD 2 ^ k]⊢ {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        exact ⟨r, hr, hmod⟩j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      obtain ⟨hprime, hmod⟩ : q.Prime ∧ q ≡ 1 [MOD 2 ^ k] := Nat.sInf_mem hnej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ (k + 1) + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      rw [Nat.pow_succj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ k * 2 + 1 ≤ qj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ k * 2 + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ k * 2 + 1 ≤ qhfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      by_contra hboundj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ q⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hxle : q ≤ 2 ^ k * 2 := by⊢ {n | m n < p n}.Infinitej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) omegaj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hlower : 2 ^ k + 1 ≤ q := by⊢ {n | m n < p n}.Infinitej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ q⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        simpa [add_comm] using hmod.symm.add_le_of_lt hprime.one_ltj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ q⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ q⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hupper : q ≤ 2 ^ k + 1 :=
        (hmod.trans Nat.add_modEq_left.symm).le_of_lt_add (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ q⊢ q < 2 ^ k + 1 + 2 ^ kj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) omegaAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k))j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hxeq : q = 2 ^ k + 1 := by⊢ {n | m n < p n}.Infinitej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) omegaj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hkodd : Odd k := ⟨j + 1, byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1⊢ k = 2 * (j + 1) + 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) dsimp [k]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1⊢ 2 * j + 3 = 2 * (j + 1) + 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k); omegaAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)⟩j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have hxeqthree : q = 3 := (hprime.dvd_iff_eq (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ 3 ≠ 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) decideAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k))).mp (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ 3 ∣ qj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        rw [hxeqj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ 3 ∣ 2 ^ k + 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ 3 ∣ 2 ^ k + 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd k⊢ 3 ∣ 2 ^ k + 1j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        simpa using hkodd.nat_add_dvd_pow_add_pow 2 1All goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k))j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      have heighteen : 8 ≤ 2 ^ k := by⊢ {n | m n < p n}.Infinitej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        change 2 ^ 3 ≤ 2 ^ kj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ 2 ^ 3 ≤ 2 ^ kj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
        exact Nat.pow_le_pow_right (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ 2 > 0j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) decideAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)) (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ 3 ≤ kj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k) dsimp [k]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3⊢ 3 ≤ 2 * j + 3j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k); omegaAll goals completed! 🐙j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k))j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonemptyhprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2hlower:2 ^ k + 1 ≤ qhupper:q ≤ 2 ^ k + 1hxeq:q = 2 ^ k + 1hkodd:Odd khxeqthree:q = 3heighteen:8 ≤ 2 ^ k⊢ Falsehfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
      omegahfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)hfj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1)hp:2 ^ (k + 1) + 1 ≤ p (2 ^ k)⊢ m (2 ^ k) < p (2 ^ k)
    omegaAll goals completed! 🐙

open scoped Classical in

Erdős [Er79e] writes it is 'easy to show' that $m_n/n \to \infty$ for almost all $n$.

@[category research solved, AMS 11]
theorem erdos_456.variants.m_div_n :
    ∃ A : Set ℕ, Tendsto (fun N ↦ (count (· ∈ A) N : ℝ) / N) atTop (𝓝 1) ∧
      Tendsto (fun n ↦ (m n : ℝ) / (n : ℝ)) (atTop ⊓ 𝓟 A) atTop := by⊢ ∃ A, Tendsto (fun N ↦ ↑(count (fun x ↦ x ∈ A) N) / ↑N) atTop (𝓝 1) ∧ Tendsto (fun n ↦ ↑(m n) / ↑n) (atTop ⊓ 𝓟 A) atTop
  sorryAll goals completed! 🐙

end Erdos456