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 Filter

open scoped Topology Classical Asymptotics


namespace 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 }

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

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

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'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 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 declaration uses 'sorry'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 declaration uses 'sorry'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 n
      ext khk:ℕ⊢ k ∈ {k | 0 < k ∧ 0 ∣ φ k} ↔ k ∈ ∅
      simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_and]hk:ℕ⊢ 0 < k → ¬0 ∣ φ k
      intro hkhk:ℕhk:0 < k⊢ ¬0 ∣ φ k
      rw [zero_dvd_iff]hk:ℕhk:0 < k⊢ ¬φ k = 0
      have := Nat.totient_pos.mpr hkhk:ℕhk:0 < kthis:0 < φ k := totient_pos.mpr hk⊢ ¬φ k = 0
      omegaAll goals completed! 🐙
    rw [hempty, Nat.sInf_empty]inlhempty:{k | 0 < k ∧ 0 ∣ φ k} = ∅ := 
  Set.ext fun k =>
    Eq.mpr
      (id
        (Eq.trans (Eq.trans (congrArg (Iff (0 < k ∧ 0 ∣ φ k)) (mn_leq_pn._simp_1 k)) (iff_false (0 < k ∧ 0 ∣ φ k)))
          mn_leq_pn._simp_2))
      fun hk =>
      Eq.mpr (id (congrArg (fun _a => ¬_a) (propext zero_dvd_iff)))
        (have this := totient_pos.mpr hk;
        fun a => mn_leq_pn._proof_2 k this a)⊢ 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 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]}.Nonempty
      exact ⟨q, hq, hmod⟩All goals completed! 🐙
    obtain ⟨hp, hmod⟩ := Nat.sInf_mem hneinrn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty := 
  Exists.casesOn (forall_exists_prime_gt_and_modEq 0 hn (coprime_one_left n)) fun q h =>
    And.casesOn h fun left right => And.casesOn right fun hq hmod => Exists.intro q ⟨hq, hmod⟩hp: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_leinr.hmn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty := 
  Exists.casesOn (forall_exists_prime_gt_and_modEq 0 hn (coprime_one_left n)) fun q h =>
    And.casesOn h fun left right => And.casesOn right fun hq hmod => Exists.intro q ⟨hq, hmod⟩hp: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, ?_⟩inr.hmn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty := 
  Exists.casesOn (forall_exists_prime_gt_and_modEq 0 hn (coprime_one_left n)) fun q h =>
    And.casesOn h fun left right => And.casesOn right fun hq hmod => Exists.intro q ⟨hq, hmod⟩hp: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 hp]inr.hmn:ℕhn:n ≠ 0hne:{k | Nat.Prime k ∧ k ≡ 1 [MOD n]}.Nonempty := 
  Exists.casesOn (forall_exists_prime_gt_and_modEq 0 hn (coprime_one_left n)) fun q h =>
    And.casesOn h fun left right => And.casesOn right fun hq hmod => Exists.intro q ⟨hq, hmod⟩hp: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 bhia:ℕb:ℕ⊢ (fun j => 2 ^ (2 * j + 3)) a = (fun j => 2 ^ (2 * j + 3)) b → 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}.Infinite
      unfold mj:ℕk:ℕ := 2 * j + 3⊢ sInf {k_1 | 0 < k_1 ∧ 2 ^ k ∣ φ k_1} ≤ 2 ^ (k + 1)
      refine Nat.sInf_le ⟨byj:ℕk:ℕ := 2 * j + 3⊢ 0 < 2 ^ (k + 1) positivityAll goals completed! 🐙, ?_⟩
      rw [Nat.totient_prime_pow Nat.prime_two (by omega)]j:ℕk:ℕ := 2 * j + 3⊢ 2 ^ k ∣ 2 ^ (k + 1 - 1) * (2 - 1)
      norm_numAll goals completed! 🐙
    have hp : 2 ^ (k + 1) + 1 ≤ p (2 ^ k) := by⊢ {n | m n < p n}.Infinite
      unfold pj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)⊢ 2 ^ (k + 1) + 1 ≤ sInf {k_1 | Nat.Prime k_1 ∧ k_1 ≡ 1 [MOD 2 ^ k]}
      let q := sInf {x | x.Prime ∧ x ≡ 1 [MOD 2 ^ k]}j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)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]}
      change 2 ^ (k + 1) + 1 ≤ qj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}⊢ 2 ^ (k + 1) + 1 ≤ q
      have hne : {x | x.Prime ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := by⊢ {n | m n < p n}.Infinite
        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) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}⊢ 2 ≠ 0 decideAll goals completed! 🐙)) (Nat.coprime_one_left (2 ^ k))
        exact ⟨r, hr, hmod⟩All goals completed! 🐙
      obtain ⟨hprime, hmod⟩ : q.Prime ∧ q ≡ 1 [MOD 2 ^ k] := Nat.sInf_mem hnej:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ (k + 1) + 1 ≤ q
      rw [Nat.pow_succ]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]⊢ 2 ^ k * 2 + 1 ≤ q
      by_contra hboundj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ q⊢ False
      have hxle : q ≤ 2 ^ k * 2 := by⊢ {n | m n < p n}.Infinite omegaAll goals completed! 🐙
      have hlower : 2 ^ k + 1 ≤ q := by⊢ {n | m n < p n}.Infinite
        simpa [add_comm] using hmod.symm.add_le_of_lt hprime.one_ltAll goals completed! 🐙
      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) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))⊢ q < 2 ^ k + 1 + 2 ^ k omegaAll goals completed! 🐙)
      have hxeq : q = 2 ^ k + 1 := by⊢ {n | m n < p n}.Infinite omegaAll goals completed! 🐙
      have hkodd : Odd k := ⟨j + 1, byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper a⊢ k = 2 * (j + 1) + 1 dsimp [k]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper a⊢ 2 * j + 3 = 2 * (j + 1) + 1; omegaAll goals completed! 🐙⟩
      have hxeqthree : q = 3 := (hprime.dvd_iff_eq (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))⊢ 3 ≠ 1 decideAll goals completed! 🐙)).mp (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))⊢ 3 ∣ q
        rw [hxeq]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))⊢ 3 ∣ 2 ^ k + 1
        simpa using hkodd.nat_add_dvd_pow_add_pow 2 1All goals completed! 🐙)
      have heighteen : 8 ≤ 2 ^ k := by⊢ {n | m n < p n}.Infinite
        change 2 ^ 3 ≤ 2 ^ kj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))hxeqthree:q = 3 := 
  (Prime.dvd_iff_eq hprime (of_decide_eq_true (id (Eq.refl true)))).mp
    (Eq.mpr (id (congrArg (fun _a => 3 ∣ _a) hxeq))
      (Eq.mp (congrArg (fun x => 3 ∣ 2 ^ k + x) (one_pow k)) (Odd.nat_add_dvd_pow_add_pow 2 1 hkodd)))⊢ 2 ^ 3 ≤ 2 ^ k
        exact Nat.pow_le_pow_right (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))hxeqthree:q = 3 := 
  (Prime.dvd_iff_eq hprime (of_decide_eq_true (id (Eq.refl true)))).mp
    (Eq.mpr (id (congrArg (fun _a => 3 ∣ _a) hxeq))
      (Eq.mp (congrArg (fun x => 3 ∣ 2 ^ k + x) (one_pow k)) (Odd.nat_add_dvd_pow_add_pow 2 1 hkodd)))⊢ 2 > 0 decideAll goals completed! 🐙) (byj:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))hxeqthree:q = 3 := 
  (Prime.dvd_iff_eq hprime (of_decide_eq_true (id (Eq.refl true)))).mp
    (Eq.mpr (id (congrArg (fun _a => 3 ∣ _a) hxeq))
      (Eq.mp (congrArg (fun x => 3 ∣ 2 ^ k + x) (one_pow k)) (Odd.nat_add_dvd_pow_add_pow 2 1 hkodd)))⊢ 3 ≤ k dsimp [k]j:ℕk:ℕ := 2 * j + 3hm:m (2 ^ k) ≤ 2 ^ (k + 1) := 
  id
    (Nat.sInf_le
      ⟨pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (ble 1 2)))
          (k + 1),
        Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ k ∣ _a)
              (totient_prime_pow prime_two (Decidable.byContradiction fun a => infinitely_many_n._proof_2 j a))))
          (of_eq_true
            (Eq.trans
              (Eq.trans
                (congrArg (Dvd.dvd (2 ^ k))
                  (Eq.trans
                    (congr (congrArg (fun x => HMul.hMul (2 ^ x)) (add_tsub_cancel_right k 1))
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natSub (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1))
                        (Eq.refl 1)))
                    (mul_one (2 ^ k))))
                (dvd_refl._simp_1 (2 ^ k)))
              (eq_true True.intro)))⟩)q:ℕ := sInf {x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}hne:{x | Nat.Prime x ∧ x ≡ 1 [MOD 2 ^ k]}.Nonempty := 
  Exists.casesOn
    (forall_exists_prime_gt_and_modEq 0 (pow_ne_zero k (of_decide_eq_true (id (Eq.refl true))))
      (coprime_one_left (2 ^ k)))
    fun r h => And.casesOn h fun left right => And.casesOn right fun hr hmod => Exists.intro r ⟨hr, hmod⟩hprime:Nat.Prime qhmod:q ≡ 1 [MOD 2 ^ k]hbound:¬2 ^ k * 2 + 1 ≤ qhxle:q ≤ 2 ^ k * 2 := Decidable.byContradiction fun a => infinitely_many_n._proof_3 j hbound ahlower:2 ^ k + 1 ≤ q := 
  Eq.mpr (id (congrArg (fun x => x ≤ q) (add_comm (2 ^ k) 1)))
    (ModEq.add_le_of_lt (ModEq.symm hmod) (Prime.one_lt hprime))hupper:q ≤ 2 ^ k + 1 := 
  ModEq.le_of_lt_add (ModEq.trans hmod (ModEq.symm add_modEq_left))
    (Decidable.byContradiction fun a => infinitely_many_n._proof_4 j hbound a)hxeq:q = 2 ^ k + 1 := Decidable.byContradiction fun a => infinitely_many_n._proof_5 j hlower hupper ahkodd:Odd k := Exists.intro (j + 1) (id (Decidable.byContradiction fun a => infinitely_many_n._proof_6 j a))hxeqthree:q = 3 := 
  (Prime.dvd_iff_eq hprime (of_decide_eq_true (id (Eq.refl true)))).mp
    (Eq.mpr (id (congrArg (fun _a => 3 ∣ _a) hxeq))
      (Eq.mp (congrArg (fun x => 3 ∣ 2 ^ k + x) (one_pow k)) (Odd.nat_add_dvd_pow_add_pow 2 1 hkodd)))⊢ 3 ≤ 2 * j + 3; omegaAll goals completed! 🐙)
      omegaAll goals completed! 🐙
    omegaAll goals completed! 🐙

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 declaration uses 'sorry'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 A N) / ↑N) atTop (𝓝 1) ∧ Tendsto (fun n => ↑(m n) / ↑n) (atTop ⊓ 𝓟 A) atTop
  sorryAll goals completed! 🐙


end Erdos456