/-
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 FormalConjecturesUtilErdős Problem 400
open Nat Filter Finsetopen scoped Asymptotics Topology
namespace 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) := ⊢ True ↔ ∀ k ≥ 2, ∃ c, (fun x => ∑ n ∈ Icc 1 x, ↑(g k n)) ~[atTop] fun x => c * ↑x * Real.log ↑x
All 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) := ⊢ 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)
All 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 : ℝ)) := k:ℕhk:k ≥ 2⊢ (fun n => ↑(g k n)) =O[atTop] fun n => Real.log ↑n
All 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 := k:ℕn:ℕh:k ≥ 2⊢ 0 < g k n
obtain ⟨k', rfl⟩ : ∃ k', k = k' + 2 := ⟨k - 2, k:ℕn:ℕh:k ≥ 2⊢ k = k - 2 + 2 All goals completed! 🐙⟩
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
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 := rfl⊢ 0 < sSup {x | ∃ a, ∃ (_ : ∏ i, (a i)! ∣ n !), ∑ i, a i - n = x}
have h_prod : ∏ i : Fin (k' + 2), (a i)! = n ! := k:ℕn:ℕh:k ≥ 2⊢ 0 < g k 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 := rfl⊢ (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 := rfl⊢ 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 0 := rfl⊢ n ! * ((if 0 = 0 then 1 else 0)! * ∏ i, (if i.succ = 0 then 1 else 0)!) = n !; All goals completed! 🐙
have h_sum : ∑ i : Fin (k' + 2), a i = n + 1 := k:ℕn:ℕh:k ≥ 2⊢ 0 < g k 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 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))⊢ a 0 + ∑ i, a i.succ = n + 1; All goals completed! 🐙
-- 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 !, 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 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))⊢ ∑ i, a i - n = 1 All goals completed! 🐙⟩
-- The set is bounded above by (k'+2) * n!
have hbdd : BddAbove {(∑ i, b i) - n | (b : Fin (k' + 2) → ℕ) (_ : ∏ i, (b i)! ∣ n !)} := k:ℕn:ℕh:k ≥ 2⊢ 0 < g k 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 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))⊢ (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 0 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ ∑ i, b i - n ≤ (k' + 2) * n !
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 ! := 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 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))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 0 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ ∀ x ∈ univ, (b x)! ≤ n !; 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 0 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !i:Fin (k' + 2)a✝:i ∈ univ⊢ (b i)! ≤ n !
All goals completed! 🐙
_ = (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 0 := rflh_prod:∏ i, (a i)! = n ! :=
Eq.mpr (id (congrArg (fun _a => _a = n !) (Fin.prod_univ_succ fun i => (a i)!)))
(Eq.mpr
(id
(congrArg (fun x => x = n !)
(congr
(congrArg (fun x => HMul.hMul x !)
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(prod_congr (Eq.refl univ) fun x a_1 =>
congrArg factorial
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1) fun a =>
Eq.refl 0)))))))
(Eq.mpr (id (congrArg (fun _a => n ! * _a = n !) (Fin.prod_univ_succ fun x => (if x = 0 then 1 else 0)!)))
(of_eq_true
(Eq.trans
(congrArg (fun x => x = n !)
(Eq.trans
(congrArg (HMul.hMul n !)
(Eq.trans
(congr (congrArg (fun x => HMul.hMul x !) (ite_cond_eq_true 1 0 (eq_self 0)))
(Eq.trans
(prod_congr (Eq.refl univ) fun x a =>
congrArg factorial (ite_cond_eq_false 1 0 (Fin.succ_ne_zero._simp_1 x)))
prod_const_one))
(mul_one 1)))
(mul_one n !)))
(eq_self n !)))))h_sum:∑ i, a i = n + 1 :=
Eq.mpr (id (congrArg (fun _a => _a = n + 1) (Fin.sum_univ_succ a)))
(of_eq_true
(Eq.trans
(Eq.trans
(congrArg (fun x => x = n + 1)
(congr
(congrArg HAdd.hAdd
(Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
0)
(ite_cond_eq_true n (if ↑0 = 1 then 1 else 0) (eq_self 0))))
(Eq.trans
(Eq.trans
(sum_congr (Eq.refl univ) fun x a_1 =>
Eq.trans
(congrFun
(Eq.trans ha_def
(funext fun i =>
ite_congr Fin.val_eq_zero_iff._simp_1 (fun a => Eq.refl n) fun a =>
Eq.refl (if ↑i = 1 then 1 else 0)))
x.succ)
(Eq.trans (ite_cond_eq_false n (if ↑x.succ = 1 then 1 else 0) (Fin.succ_ne_zero._simp_1 x))
(ite_congr (Eq.trans add_eq_right._simp_1 Fin.val_eq_zero_iff._simp_1) (fun a => Eq.refl 1)
fun a => Eq.refl 0)))
(sum_ite_eq' univ 0 fun x => 1))
(ite_cond_eq_true 1 0 (mem_univ._simp_1 0)))))
add_left_cancel_iff._simp_1)
(eq_self 1)))hmem:1 ∈ {x | ∃ b, ∃ (_ : ∏ i, (b i)! ∣ n !), ∑ i, b i - n = x} :=
Exists.intro a
(Exists.intro (h_prod ▸ Eq.symm h_prod ▸ dvd_refl n !)
(Decidable.byContradiction fun a => g_pos._proof_2 n k' h_sum a))b:Fin (k' + 2) → ℕhb:∏ i, (b i)! ∣ n !⊢ #univ • n ! = (k' + 2) * n ! All goals completed! 🐙
All goals completed! 🐙
end Erdos400