FormalConjectures.ErdosProblems.«400»

/-
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 400

Reference: erdosproblems.com/400

open Nat Filter Finsetopen scoped Asymptotics Topologynamespace Erdos400

For any $k\geq 2$ let $g_k(n)$ denote the maximum value of $(a_1+\cdots+a_k)-n$ where $a_1,\ldots,a_k$ are integers such that $a_1!\cdots a_k! \mid n!$.

noncomputable def g (k n : ℕ) : ℕ :=
  sSup { ((∑ i, a i) - n) | (a : Fin k → ℕ) (_ : (∏ i, (a i) !) ∣ n !) }

Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$?

@[category research open, AMS 11]
theorem erdos_400.parts.i :
    answer(sorry) ↔ ∀ᵉ (k ≥ 2), ∃ c : ℝ,
      (fun x : ℕ ↦ (∑ n ∈ Icc 1 x, (g k n : ℝ))) ~[atTop]
      (fun x : ℕ ↦ c * x * Real.log x) := by⊢ True ↔ ∀ k ≥ 2, ∃ c, (fun x ↦ ∑ n ∈ Icc 1 x, ↑(g k n)) ~[atTop] fun x ↦ c * ↑x * Real.log ↑x
  sorryAll goals completed! 🐙

Is it true that there is a constant $c_k$ such that for almost all $n < x$ we have $g_k(n)=c_k\log x+o(\log x)$?

@[category research open, AMS 11]
theorem erdos_400.parts.ii :
    answer(sorry) ↔ ∀ᵉ (k ≥ 2), ∃ c : ℝ, ∀ ε > 0,
      Tendsto (fun x : ℕ ↦
        (((Icc 1 x).filter (fun n ↦
          |(g k n : ℝ) - c * Real.log x| ≤ ε * Real.log x)).card : ℝ) / x)
        atTop (𝓝 1) := by⊢ True ↔
  ∀ k ≥ 2,
    ∃ c,
      ∀ ε > 0, Tendsto (fun x ↦ ↑(#({n ∈ Icc 1 x | |↑(g k n) - c * Real.log ↑x| ≤ ε * Real.log ↑x})) / ↑x) atTop (𝓝 1)
  sorryAll goals completed! 🐙

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

@[category research solved, AMS 11]
theorem erdos_400.variants.upper_bound (k : ℕ) (hk : k ≥ 2) :
    (fun n : ℕ ↦ (g k n : ℝ)) ≪ (fun n : ℕ ↦ Real.log (n : ℝ)) := byk:ℕhk:k ≥ 2⊢ (fun n ↦ ↑(g k n)) =O[atTop] fun n ↦ Real.log ↑n
  sorryAll goals completed! 🐙

For $k \ge 2$, $g_k(n) > 0$. We show this by choosing $a = (n, 1, 0, \ldots, 0)$.


@[category test, AMS 11]
theorem erdos_400.variants.g_pos (k n : ℕ) (h: k ≥ 2) : 0 < g k n := byk:ℕn:ℕh:k ≥ 2⊢ 0 < g k n
  obtain ⟨k', rfl⟩ : ∃ k', k = k' + 2 := ⟨k - 2, byk:ℕn:ℕh:k ≥ 2⊢ k = k - 2 + 2n:ℕk':ℕh:k' + 2 ≥ 2⊢ 0 < g (k' + 2) n omegaAll goals completed! 🐙n:ℕk':ℕh:k' + 2 ≥ 2⊢ 0 < g (k' + 2) n⟩n:ℕk':ℕh:k' + 2 ≥ 2⊢ 0 < g (k' + 2) n
  simp only [g]n:ℕk':ℕh:k' + 2 ≥ 2⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  -- Witness: a(0) = n, a(1) = 1, a(i) = 0 for i ≥ 2
  set a : Fin (k' + 2) → ℕ := fun i =>
    if (i : ℕ) = 0 then n else if (i : ℕ) = 1 then 1 else 0 with ha_defn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  have h_prod : ∏ i : Fin (k' + 2), (a i)! = n ! := byk:ℕn:ℕh:k ≥ 2⊢ 0 < g k nn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    rw [Fin.prod_univ_succn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ (a 0)! * ∏ i, (a i.succ)! = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ (a 0)! * ∏ i, (a i.succ)! = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ (a 0)! * ∏ i, (a i.succ)! = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}; simp [ha_def]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ n ! * ∏ x, (if x = 0 then 1 else 0)! = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    rw [Fin.prod_univ_succn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ n ! * ((if 0 = 0 then 1 else 0)! * ∏ i, (if i.succ = 0 then 1 else 0)!) = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ n ! * ((if 0 = 0 then 1 else 0)! * ∏ i, (if i.succ = 0 then 1 else 0)!) = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0⊢ n ! * ((if 0 = 0 then 1 else 0)! * ∏ i, (if i.succ = 0 then 1 else 0)!) = n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}; simpn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  have h_sum : ∑ i : Fin (k' + 2), a i = n + 1 := byk:ℕn:ℕh:k ≥ 2⊢ 0 < g k nn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    rw [Fin.sum_univ_succn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ a 0 + ∑ i, a i.succ = n + 1n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ a 0 + ∑ i, a i.succ = n + 1n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !⊢ a 0 + ∑ i, a i.succ = n + 1n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}; simp [ha_def]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  -- 1 is in the set
  have hmem : 1 ∈ {(∑ i, b i) - n | (b : Fin (k' + 2) → ℕ) (_ : ∏ i, (b i)! ∣ n !)} :=
    ⟨a, h_prod ▸ dvd_refl n !, byn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1⊢ ∑ i, a i - n = 1n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x} omegaAll goals completed! 🐙n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}⟩n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  -- The set is bounded above by (k'+2) * n!
  have hbdd : BddAbove {(∑ i, b i) - n | (b : Fin (k' + 2) → ℕ) (_ : ∏ i, (b i)! ∣ n !)} := byk:ℕn:ℕh:k ≥ 2⊢ 0 < g k nn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    refine ⟨(k' + 2) * n !, ?_⟩n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ (k' + 2) * n ! ∈ upperBounds {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    rintro x ⟨b, hb, rfl⟩n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ ∑ i, b i - n ≤ (k' + 2) * n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
    calc (∑ i, b i) - n
        ≤ ∑ i, b i := Nat.sub_le _ _
      _ ≤ ∑ i : Fin (k' + 2), (b i)! :=
          Finset.sum_le_sum fun i _ => Nat.self_le_factorial _
      _ ≤ Finset.univ.card • n ! := byn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ ∑ i, (b i)! ≤ #univ • n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
          apply Finset.sum_le_card_nsmuln:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ ∀ x ∈ univ, (b x)! ≤ n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}; intro i _n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !i:Fin (k' + 2)a✝:i ∈ univ⊢ (b i)! ≤ n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
          exact le_trans (Finset.single_le_prod' (fun j _ =>
            Nat.one_le_iff_ne_zero.mpr (Nat.factorial_ne_zero _))
            (Finset.mem_univ i)) (Nat.le_of_dvd (Nat.factorial_pos n) hb)All goals completed! 🐙n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
      _ = (k' + 2) * n ! := byn:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ #univ • n ! = (k' + 2) * n !n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x} simp [smul_eq_mul]n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}n:ℕk':ℕh:k' + 2 ≥ 2a:Fin (k' + 2) → ℕ := fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0ha_def:a = fun i ↦ if ↑i = 0 then n else if ↑i = 1 then 1 else 0h_prod:∏ i, (a i)! = n !h_sum:∑ i, a i = n + 1hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}hbdd:BddAbove {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x}⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
  exact Nat.lt_of_lt_of_le Nat.one_pos (le_csSup hbdd hmem)All goals completed! 🐙

end Erdos400