Open Proof Network

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

the thin strip with n/gcd(n,k) prime, gcd(n,k) ≥ 2

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

open

Hole h_div of erdos-1094--h2--h1--h4--h1 (split by 20261015T145300Z-t1015c-a06-partial.lean).

$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ 2\le\gcd(n,k)\ \Longrightarrow\ k\le K$

Only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{21/40})$ (the upper bound taken over the reals, with $21/40$ a real exponent) such that $k\lfloor n/k\rfloor$ divides $k!$, the least prime factor of $\binom{n}{k}$ exceeds $\lfloor n/k\rfloor$, and $n/\gcd(n,k)$ is prime with $\gcd(n,k)\ge 2$. Lean conventions: n / k is floor division, $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$, and Nat.minFac is the least prime factor (1 at 1, 2 at 0).

unverified · history

Lean
theorem erdos_1094__h2__h1__h4__h1__h2 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K := 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 is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from this hole by 20261018T192800Z-t1018-b-partial.lean (merged in 5b822c6c3b80, attestation 000757).

  • h_proper → erdos-1094--h2--h1--h4--h1--h2--h1 (open)

    $\displaystyle \exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$

Read the partial proof (Lean)
theorem erdos_1094__h2__h1__h4__h1__h2 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K := by
  -- approach: split on whether gcd(n,k) = k; that case is impossible (it forces n = k², k prime, and k² ∤ k!)
  -- licence: CC-BY-4.0
  -- label: proper common divisor case
  -- claim: $\exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$
  -- The case gcd(n,k) = k is closed in the assembly.
  -- When gcd(n,k) = k, k ∣ n, so n/k = q is prime and k·q = n ∣ k!, giving q ≤ k; with k² ≤ n, q = k,
  -- so k is prime and k² ∣ k!, i.e. k ∣ (k-1)!, impossible. Only proper divisors 2 ≤ gcd(n,k) < k remain.
  have h_proper : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K := sorry
  obtain ⟨K, hK⟩ := h_proper
  refine ⟨K, ?_⟩
  intro n k hk hkn hr hdiv hmin hp hg
  rcases lt_or_eq_of_le (Nat.le_of_dvd hk (Nat.gcd_dvd_right n k)) with hlt | heq
  · exact hK n k hk hkn hr hdiv hmin hp hg hlt
  · exfalso
    have hkd : k ∣ n := by
      have := Nat.gcd_dvd_left n k
      rwa [heq] at this
    rw [heq] at hp
    have hq1 : n / k ≤ k := (Nat.Prime.dvd_factorial hp).mp (dvd_trans (Dvd.intro_left k rfl) hdiv)
    have hq2 : k ≤ n / k := (Nat.le_div_iff_mul_le hk).mpr hkn
    have hqk : n / k = k := le_antisymm hq1 hq2
    rw [hqk] at hp hdiv
    have hk2 := hp.two_le
    obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
    rw [Nat.factorial_succ] at hdiv
    have h1 : j + 1 ∣ j.factorial := (Nat.mul_dvd_mul_iff_left (by omega)).mp hdiv
    have h2 := (Nat.Prime.dvd_factorial hp).mp h1
    omega

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.

What is known

Work on it

Work on this statement →

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

open scoped Nat

/-! Hole `h_div` 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__h1__h4__h1__h2 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K := by
  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 →

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

$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ 2\le\gcd(n,k)\ \Longrightarrow\ k\le K$

Only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{21/40})$ (the upper bound taken over the reals, with $21/40$ a real exponent) such that $k\lfloor n/k\rfloor$ divides $k!$, the least prime factor of $\binom{n}{k}$ exceeds $\lfloor n/k\rfloor$, and $n/\gcd(n,k)$ is prime with $\gcd(n,k)\ge 2$. Lean conventions: n / k is floor division, $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$, and Nat.minFac is the least prime factor (1 at 1, 2 at 0).

Rendered from gloss/7aa7e431a228….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/Statement.lean. Origin: compiler-derived.

Depends on (1), each in words

Depends on, each in words where someone has written them:

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000757.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/Witness.lean, sha256 f5d4fdda3170.
import Mathlib
import Nodes.«erdos-1094--h2--h1--h4--h1--h2».Context
open scoped Nat

/-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance
satisfying this statement's hypotheses; until then the node is blocked. -/

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 →

Attempts (2)

2 recorded. Routes refuted: none. Failure classes: route-dead-ends 1.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1018-b; merged in 5b822c6c3b80 under attestations/000757.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261018T192800Z-t1018-b-partial.lean, extracted by the gate at 32961c7678e9 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.

  1. h_proper hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K hole

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K, with h_proper : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K.

    Uses library Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. .

    Left open as a hole; its statement is erdos-1094--h2--h1--h4--h1--h2--h1 (open).

    Lean, lines 22–28
      have h_proper : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K := sorry

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, lines 22–28 at f0dfc93f9827 ↗

  2. s2 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K, with K : ℕ, hK : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K.

    Lean, line 29
      obtain ⟨K, hK⟩ := h_proper

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 29 at f0dfc93f9827 ↗

  3. s3 case

    Leaves k ≤ K, with hlt : n.gcd k < k.

    Lean, line 33
      · exact hK n k hk hkn hr hdiv hmin hp hg hlt

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 33 at f0dfc93f9827 ↗

  4. s4 case

    Leaves k ≤ K, with heq : n.gcd k = k.

    Uses library Nat.factorial_succ.

    Lean, lines 34–48
      · exfalso
    have hkd : k ∣ n := by
      have := Nat.gcd_dvd_left n k
      rwa [heq] at this
    rw [heq] at hp
    have hq1 : n / k ≤ k := (Nat.Prime.dvd_factorial hp).mp (dvd_trans (Dvd.intro_left k rfl) hdiv)
    have hq2 : k ≤ n / k := (Nat.le_div_iff_mul_le hk).mpr hkn
    have hqk : n / k = k := le_antisymm hq1 hq2
    rw [hqk] at hp hdiv
    have hk2 := hp.two_le
    obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
    rw [Nat.factorial_succ] at hdiv
    have h1 : j + 1 ∣ j.factorial := (Nat.mul_dvd_mul_iff_left (by omega)).mp hdiv
    have h2 := (Nat.Prime.dvd_factorial hp).mp h1
    omega

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, lines 34–48 at f0dfc93f9827 ↗

    1. s4.hkd have k ∣ n

      Leaves False, with hkd : k ∣ n.

      Lean, lines 35–37
          have hkd : k ∣ n := by
      have := Nat.gcd_dvd_left n k
      rwa [heq] at this

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, lines 35–37 at f0dfc93f9827 ↗

      1. s4.hkd.this have n.gcd k ∣ n

        Leaves k ∣ n, with this : n.gcd k ∣ n.

        Uses library Nat.gcd_dvd_left.

        Lean, line 36
              have := Nat.gcd_dvd_left n k

        targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 36 at f0dfc93f9827 ↗

    2. s4.hq1 have n / k ≤ k

      Leaves False, with hq1 : n / k ≤ k.

      Uses library Nat.Prime.dvd_factorial, dvd_trans, Dvd.intro_left, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, line 39
          have hq1 : n / k ≤ k := (Nat.Prime.dvd_factorial hp).mp (dvd_trans (Dvd.intro_left k rfl) hdiv)

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 39 at f0dfc93f9827 ↗

    3. s4.hq2 have k ≤ n / k

      Leaves False, with hq2 : k ≤ n / k.

      Uses library Nat.le_div_iff_mul_le.

      Lean, line 40
          have hq2 : k ≤ n / k := (Nat.le_div_iff_mul_le hk).mpr hkn

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 40 at f0dfc93f9827 ↗

    4. s4.hqk have n / k = k

      Leaves False, with hqk : n / k = k.

      Uses library le_antisymm.

      Lean, line 41
          have hqk : n / k = k := le_antisymm hq1 hq2

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 41 at f0dfc93f9827 ↗

    5. s4.hk2 have (2 : ℕ) ≤ k

      Leaves False, with hk2 : (2 : ℕ) ≤ k.

      Lean, line 43
          have hk2 := hp.two_le

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 43 at f0dfc93f9827 ↗

    6. s4.s6 obtain ∃ (j : ℕ), k = j + (1 : ℕ)

      Leaves False, with j : ℕ, hk : (0 : ℕ) < j + (1 : ℕ), hkn : (j + (1 : ℕ)) * (j + (1 : ℕ)) ≤ n, hr : (↑n : ℝ) < (↑(j + (1 : ℕ)) : ℝ) * ((↑(j + (1 : ℕ)) : ℝ) + (3 : ℝ) * (↑(j + (1 : ℕ)) : ℝ) ^ (21 / 40 : ℝ)), hdiv : (j + (1 : ℕ)) * (j + (1 : ℕ)) ∣ (j + (1 : ℕ))!, hmin : (n.choose (j + (1 : ℕ))).minFac > n / (j + (1 : ℕ)), hp : Nat.Prime (j + (1 : ℕ)), hg : (2 : ℕ) ≤ n.gcd (j + (1 : ℕ)), heq : n.gcd (j + (1 : ℕ)) = j + (1 : ℕ), hkd : j + (1 : ℕ) ∣ n, hq1 : n / (j + (1 : ℕ)) ≤ j + (1 : ℕ), hq2 : j + (1 : ℕ) ≤ n / (j + (1 : ℕ)), hqk : n / (j + (1 : ℕ)) = j + (1 : ℕ), hk2 : (2 : ℕ) ≤ j + (1 : ℕ).

      Uses library Exists.intro Existential introduction. .

      Lean, line 44
          obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 44 at f0dfc93f9827 ↗

    7. s4.h1 have j + (1 : ℕ) ∣ j !

      Leaves False, with h1 : j + (1 : ℕ) ∣ j !.

      Uses library Nat.mul_dvd_mul_iff_left.

      Lean, line 46
          have h1 : j + 1 ∣ j.factorial := (Nat.mul_dvd_mul_iff_left (by omega)).mp hdiv

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 46 at f0dfc93f9827 ↗

    8. s4.h2 have j + (1 : ℕ) ≤ j

      Leaves False, with h2 : j + (1 : ℕ) ≤ j.

      Uses library Nat.Prime.dvd_factorial.

      Lean, line 47
          have h2 := (Nat.Prime.dvd_factorial hp).mp h1

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean, line 47 at f0dfc93f9827 ↗

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

open scoped Nat

/-! Hole `h_div` 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__h1__h4__h1__h2 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K := by
  -- approach: split on whether gcd(n,k) = k; that case is impossible (it forces n = k², k prime, and k² ∤ k!)
  -- licence: CC-BY-4.0
  -- label: proper common divisor case
  -- claim: $\exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$
  -- The case gcd(n,k) = k is closed in the assembly.
  -- When gcd(n,k) = k, k ∣ n, so n/k = q is prime and k·q = n ∣ k!, giving q ≤ k; with k² ≤ n, q = k,
  -- so k is prime and k² ∣ k!, i.e. k ∣ (k-1)!, impossible. Only proper divisors 2 ≤ gcd(n,k) < k remain.
  have h_proper : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                (2 : ℕ) ≤ n.gcd k → n.gcd k < k → k ≤ K := sorry
  obtain ⟨K, hK⟩ := h_proper
  refine ⟨K, ?_⟩
  intro n k hk hkn hr hdiv hmin hp hg
  rcases lt_or_eq_of_le (Nat.le_of_dvd hk (Nat.gcd_dvd_right n k)) with hlt | heq
  · exact hK n k hk hkn hr hdiv hmin hp hg hlt
  · exfalso
    have hkd : k ∣ n := by
      have := Nat.gcd_dvd_left n k
      rwa [heq] at this
    rw [heq] at hp
    have hq1 : n / k ≤ k := (Nat.Prime.dvd_factorial hp).mp (dvd_trans (Dvd.intro_left k rfl) hdiv)
    have hq2 : k ≤ n / k := (Nat.le_div_iff_mul_le hk).mpr hkn
    have hqk : n / k = k := le_antisymm hq1 hq2
    rw [hqk] at hp hdiv
    have hk2 := hp.two_le
    obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
    rw [Nat.factorial_succ] at hdiv
    have h1 : j + 1 ∣ j.factorial := (Nat.mul_dvd_mul_iff_left (by omega)).mp hdiv
    have h2 := (Nat.Prime.dvd_factorial hp).mp h1
    omega
How to read this page

No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).

How to read a statement’s page →