1. FormalConjectures
  2. ErdosProblems
  3. «18»
/- 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 18

Reference:

    erdosproblems.com/18

    [ErGr80] Erdős, P. and Graham, R. L. (1980). Old and New Problems and Results in Combinatorial Number Theory. Monographies de L'Enseignement Mathématique, 28. Université de Genève. (See the sections on Egyptian fractions or practical numbers).

    [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.

open Filter Asymptotics Real namespace Erdos18

For a practical number $n$, $h(n)$ is the maximum over all $1 ≤ m ≤ n$ of the minimum number of divisors of $n$ needed to represent $m$ as a sum of distinct divisors.

noncomputable def practicalH (n : ℕ) : ℕ := Finset.sup (Finset.Icc 1 n) fun m => sInf {k | ∃ D : Finset ℕ, D ⊆ n.divisors ∧ D.card = k ∧ m ∈ subsetSums D}

$h(1) = 1$: we need the single divisor {1} to represent 1.

@[category test, AMS 11] theorem practicalH_one : practicalH 1 = 1 := ⊢ practicalH 1 = 1 All goals completed! 🐙

$h(2) = 1$: divisors are {1, 2}, each of m=1,2 needs only 1 divisor.

@[category test, AMS 11] theorem practicalH_two : practicalH 2 = 1 := ⊢ practicalH 2 = 1 ⊢ max (sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D}) (sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D}) = 1 have h1 : sInf {k | ∃ D : Finset ℕ, D ⊆ {1, 2} ∧ D.card = k ∧ 1 ∈ subsetSums D} = 1 := le_antisymm (Nat.sInf_le ⟨{1}, ⊢ {1} ⊆ {1, 2} All goals completed! 🐙, rfl, {1}, rfl.subset, ⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩) (le_csInf ⟨1, {1}, ⊢ {1} ⊆ {1, 2} All goals completed! 🐙, rfl, {1}, rfl.subset, ⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩ fun k ⟨D, _, hD, B, hB, hm⟩ => hD ▸ Finset.one_le_card.mpr ((Finset.nonempty_iff_ne_empty.mpr fun h => k:ℕx✝:k ∈ {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D}D:Finset ℕleft✝:D ⊆ {1, 2}hD:D.card = kB:Finset ℕhB:↑B ⊆ ↑Dhm:1 = ∑ i ∈ B, ih:B = ∅⊢ False All goals completed! 🐙).mono hB)) have h2 : sInf {k | ∃ D : Finset ℕ, D ⊆ {1, 2} ∧ D.card = k ∧ 2 ∈ subsetSums D} = 1 := le_antisymm (Nat.sInf_le ⟨{2}, h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1 := le_antisymm (Nat.sInf_le (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) (le_csInf (Exists.intro 1 (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) fun k x => match x with | Exists.intro D ⟨left, ⟨hD, Exists.intro B ⟨hB, hm⟩⟩⟩ => hD ▸ Finset.one_le_card.mpr (Finset.Nonempty.mono hB (Finset.nonempty_iff_ne_empty.mpr fun h => False.elim (Eq.mp (Eq.trans (congrArg (Eq 1) (Finset.sum_congr h fun x a => Eq.refl x)) one_ne_zero._simp_1) hm))))⊢ {2} ⊆ {1, 2} All goals completed! 🐙, rfl, {2}, rfl.subset, h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1 := le_antisymm (Nat.sInf_le (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) (le_csInf (Exists.intro 1 (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) fun k x => match x with | Exists.intro D ⟨left, ⟨hD, Exists.intro B ⟨hB, hm⟩⟩⟩ => hD ▸ Finset.one_le_card.mpr (Finset.Nonempty.mono hB (Finset.nonempty_iff_ne_empty.mpr fun h => False.elim (Eq.mp (Eq.trans (congrArg (Eq 1) (Finset.sum_congr h fun x a => Eq.refl x)) one_ne_zero._simp_1) hm))))⊢ 2 = ∑ i ∈ {2}, i All goals completed! 🐙⟩) (le_csInf ⟨1, {2}, h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1 := le_antisymm (Nat.sInf_le (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) (le_csInf (Exists.intro 1 (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) fun k x => match x with | Exists.intro D ⟨left, ⟨hD, Exists.intro B ⟨hB, hm⟩⟩⟩ => hD ▸ Finset.one_le_card.mpr (Finset.Nonempty.mono hB (Finset.nonempty_iff_ne_empty.mpr fun h => False.elim (Eq.mp (Eq.trans (congrArg (Eq 1) (Finset.sum_congr h fun x a => Eq.refl x)) one_ne_zero._simp_1) hm))))⊢ {2} ⊆ {1, 2} All goals completed! 🐙, rfl, {2}, rfl.subset, h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1 := le_antisymm (Nat.sInf_le (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) (le_csInf (Exists.intro 1 (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) fun k x => match x with | Exists.intro D ⟨left, ⟨hD, Exists.intro B ⟨hB, hm⟩⟩⟩ => hD ▸ Finset.one_le_card.mpr (Finset.Nonempty.mono hB (Finset.nonempty_iff_ne_empty.mpr fun h => False.elim (Eq.mp (Eq.trans (congrArg (Eq 1) (Finset.sum_congr h fun x a => Eq.refl x)) one_ne_zero._simp_1) hm))))⊢ 2 = ∑ i ∈ {2}, i All goals completed! 🐙⟩ fun k ⟨D, _, hD, B, hB, hm⟩ => hD ▸ Finset.one_le_card.mpr ((Finset.nonempty_iff_ne_empty.mpr fun h => h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1 := le_antisymm (Nat.sInf_le (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) (le_csInf (Exists.intro 1 (Exists.intro {1} ⟨of_eq_true (Eq.trans Finset.singleton_subset_iff._simp_1 (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self 1)) (Eq.trans Finset.mem_singleton._simp_1 (OfNat.one_ne_ofNat._simp_1 2))) (or_false True)))), ⟨rfl, Exists.intro {1} ⟨Eq.subset rfl, of_eq_true (Eq.trans (congrArg (Eq 1) (Finset.sum_singleton (fun x => x) 1)) (eq_self 1))⟩⟩⟩)) fun k x => match x with | Exists.intro D ⟨left, ⟨hD, Exists.intro B ⟨hB, hm⟩⟩⟩ => hD ▸ Finset.one_le_card.mpr (Finset.Nonempty.mono hB (Finset.nonempty_iff_ne_empty.mpr fun h => False.elim (Eq.mp (Eq.trans (congrArg (Eq 1) (Finset.sum_congr h fun x a => Eq.refl x)) one_ne_zero._simp_1) hm))))k:ℕx✝:k ∈ {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D}D:Finset ℕleft✝:D ⊆ {1, 2}hD:D.card = kB:Finset ℕhB:↑B ⊆ ↑Dhm:2 = ∑ i ∈ B, ih:B = ∅⊢ False All goals completed! 🐙).mono hB)) All goals completed! 🐙

$h(6) = 2$: divisors are {1, 2, 3, 6}. The hardest m to represent is m=4 or m=5, each requiring 2 divisors: 4=1+3, 5=2+3.

@[category test, AMS 11] theorem practicalH_six : practicalH 6 = 2 := ⊢ practicalH 6 = 2 have hdiv : Nat.divisors 6 = ({1, 2, 3, 6} : Finset ℕ) := ⊢ practicalH 6 = 2 All goals completed! 🐙 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))⊢ practicalH 6 ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))⊢ 2 ≤ practicalH 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))⊢ practicalH 6 ≤ 2 -- practicalH 6 ≤ 2 : each m in [1,6] is a sum of at most two divisors of 6. hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ Finset.Icc 1 6, sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ b ∈ subsetSums ↑D} ≤ 2 intro m hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm:m ∈ Finset.Icc 1 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm:1 ≤ m ∧ m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ mhm2:m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 2hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 2 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{1, 2}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2}.card = 2 All goals completed! 🐙, {1}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ ↑{1} ⊆ ↑{1, 2} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{1, 2}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2}.card = 2 All goals completed! 🐙, {2}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ ↑{2} ⊆ ↑{1, 2} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ 2 = ∑ i ∈ {2}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{1, 2}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2}.card = 2 All goals completed! 🐙, {1, 2}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ ↑{1, 2} ⊆ ↑{1, 2} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ 3 = ∑ i ∈ {1, 2}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{1, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3}.card = 2 All goals completed! 🐙, {1, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ ↑{1, 3} ⊆ ↑{1, 3} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ 4 = ∑ i ∈ {1, 3}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{2, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3}.card = 2 All goals completed! 🐙, {2, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ ↑{2, 3} ⊆ ↑{2, 3} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ 5 = ∑ i ∈ {2, 3}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 2 exact Nat.sInf_le ⟨{1, 6}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6}.card = 2 All goals completed! 🐙, {6}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ ↑{6} ⊆ ↑{1, 6} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ 6 = ∑ i ∈ {6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))⊢ 2 ≤ practicalH 6 -- 2 ≤ practicalH 6, witnessed by m = 4 (which needs two divisors: 4 = 1 + 3). have h4 : (4 : ℕ) ∈ Finset.Icc 1 6 := ⊢ practicalH 6 = 2 All goals completed! 🐙 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ 2 ≤ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D} hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}.Nonemptyhdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}, 2 ≤ b hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}.Nonempty exact ⟨2, {1, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 3} ⊆ Nat.divisors 6 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 3} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 3}.card = 2 All goals completed! 🐙, {1, 3}, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ ↑{1, 3} ⊆ ↑{1, 3} All goals completed! 🐙, hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ 4 = ∑ i ∈ {1, 3}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}, 2 ≤ b hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, i⊢ 2 ≤ k hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihk:¬2 ≤ k⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihk:k < 2⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 2⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 2⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 2⊢ False -- D.card = 0 : D = ∅, so B = ∅ and the sum is 0 ≠ 4. hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 2⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑∅⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ False All goals completed! 🐙 hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 2⊢ False -- D.card = 1 : D = {d} with d ∣ 6, so the sum is 0 or d, neither equal to 4. hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 2⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}⊢ False have hd : d ∈ Nat.divisors 6 := hDsub (hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}⊢ d ∈ {d} All goals completed! 🐙) hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {1}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {2}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {3}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {1}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {2}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {3}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = ∅⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = {6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6h:B = ∅⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6h:B = {1}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6h:B = ∅⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6h:B = {2}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6h:B = ∅⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6h:B = {3}⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = ∅⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = {6}⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {6}, i⊢ False hdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {1}, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {2}, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {3}, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 6 = {1, 2, 3, 6} := of_decide_eq_true (id (Eq.refl true))h4:4 ∈ Finset.Icc 1 6 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {6}, i⊢ False All goals completed! 🐙

$h(12) = 3$: divisors are {1, 2, 3, 4, 6, 12}. The hardest m is m=11, requiring 3 divisors: 11=1+4+6.

@[category test, AMS 11] theorem practicalH_twelve : practicalH 12 = 3 := ⊢ practicalH 12 = 3 have hdiv : Nat.divisors 12 = ({1, 2, 3, 4, 6, 12} : Finset ℕ) := ⊢ practicalH 12 = 3 All goals completed! 🐙 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))⊢ practicalH 12 ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))⊢ 3 ≤ practicalH 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))⊢ practicalH 12 ≤ 3 -- practicalH 12 ≤ 3 : each m in [1,12] is a sum of at most three divisors of 12. hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ Finset.Icc 1 12, sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ b ∈ subsetSums ↑D} ≤ 3 intro m hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm:m ∈ Finset.Icc 1 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm:1 ≤ m ∧ m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ mhm2:m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 7 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 8 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 9 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 10 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D} ≤ 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 12 ∈ subsetSums ↑D} ≤ 3 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 2, 3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3}.card = 3 All goals completed! 🐙, {1}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ ↑{1} ⊆ ↑{1, 2, 3} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 2, 3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3}.card = 3 All goals completed! 🐙, {2}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ ↑{2} ⊆ ↑{1, 2, 3} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ 2 = ∑ i ∈ {2}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 2, 3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3}.card = 3 All goals completed! 🐙, {3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ ↑{3} ⊆ ↑{1, 2, 3} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ 3 = ∑ i ∈ {3}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6}.card = 3 All goals completed! 🐙, {4}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ ↑{4} ⊆ ↑{1, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ 4 = ∑ i ∈ {4}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6}.card = 3 All goals completed! 🐙, {1, 4}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ ↑{1, 4} ⊆ ↑{1, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ 5 = ∑ i ∈ {1, 4}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 2, 3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3}.card = 3 All goals completed! 🐙, {1, 2, 3}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ ↑{1, 2, 3} ⊆ ↑{1, 2, 3} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ 6 = ∑ i ∈ {1, 2, 3}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 7 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6}.card = 3 All goals completed! 🐙, {1, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ ↑{1, 6} ⊆ ↑{1, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ 7 = ∑ i ∈ {1, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 8 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{2, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6}.card = 3 All goals completed! 🐙, {2, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ ↑{2, 6} ⊆ ↑{2, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ 8 = ∑ i ∈ {2, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 9 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{3, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6}.card = 3 All goals completed! 🐙, {3, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ ↑{3, 6} ⊆ ↑{3, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ 9 = ∑ i ∈ {3, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 10 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{4, 6, 12}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12}.card = 3 All goals completed! 🐙, {4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ ↑{4, 6} ⊆ ↑{4, 6, 12} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ 10 = ∑ i ∈ {4, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6}.card = 3 All goals completed! 🐙, {1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ ↑{1, 4, 6} ⊆ ↑{1, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ 11 = ∑ i ∈ {1, 4, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 12 ∈ subsetSums ↑D} ≤ 3 exact Nat.sInf_le ⟨{2, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6}.card = 3 All goals completed! 🐙, {2, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ ↑{2, 4, 6} ⊆ ↑{2, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ 12 = ∑ i ∈ {2, 4, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))⊢ 3 ≤ practicalH 12 -- 3 ≤ practicalH 12, witnessed by m = 11 (needs three divisors: 11 = 1 + 4 + 6). have h11 : (11 : ℕ) ∈ Finset.Icc 1 12 := ⊢ practicalH 12 = 3 All goals completed! 🐙 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ 3 ≤ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D} hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}.Nonemptyhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}, 3 ≤ b hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}.Nonempty exact ⟨3, {1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 4, 6} ⊆ Nat.divisors 12 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ {1, 4, 6}.card = 3 All goals completed! 🐙, {1, 4, 6}, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ ↑{1, 4, 6} ⊆ ↑{1, 4, 6} All goals completed! 🐙, hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ 11 = ∑ i ∈ {1, 4, 6}, i All goals completed! 🐙⟩ hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}, 3 ≤ b hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, i⊢ 3 ≤ k hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihk:¬3 ≤ k⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihk:k < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 3⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 3⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 2hk:2 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑∅⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ False All goals completed! 🐙 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}⊢ False have hd : d ∈ Nat.divisors 12 := hDsub (hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}⊢ d ∈ {d} All goals completed! 🐙) hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 4, 6, 12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 4, 6, 12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {1}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {2}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {3}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {4}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {6}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {1}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {2}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {3}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {4}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {6}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = {12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12h:B = {1}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12h:B = {2}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12h:B = {3}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12h:B = {4}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12h:B = {6}⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = ∅⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = {12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {12}, i⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {1}, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {2}, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {3}, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {4}, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {6}, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falsehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {12}, i⊢ False All goals completed! 🐙 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 2hk:2 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:∃ x y, x ≠ y ∧ D = {x, y}hk:2 < 3⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}⊢ False have ha : a ∈ Nat.divisors 12 := hDsub (hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}⊢ a ∈ {a, b} All goals completed! 🐙) have hb : b ∈ Nat.divisors 12 := hDsub (hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}ha:a ∈ Nat.divisors 12 := hDsub (of_eq_true (Eq.trans Finset.mem_insert._simp_1 (Eq.trans (congr (congrArg Or (eq_self a)) Finset.mem_singleton._simp_1) (true_or (a = b)))))⊢ b ∈ {a, b} All goals completed! 🐙) hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}ha:a ∈ {1, 2, 3, 4, 6, 12}hb:b ∈ {1, 2, 3, 4, 6, 12}⊢ False hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}ha:a ∈ {1, 2, 3, 4, 6, 12}hb:b ∈ {1, 2, 3, 4, 6, 12}hBp:B ⊆ {a, b} := Finset.coe_subset.mp hBsub⊢ False have key : ∀ S ∈ ({a, b} : Finset ℕ).powerset, S.sum (fun x => x) ≠ 11 := ⊢ practicalH 12 = 3 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:1 ≠ bhDsub:{1, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, b}hBp:B ⊆ {1, b}⊢ ∀ S ∈ {1, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:2 ≠ bhDsub:{2, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, b}hBp:B ⊆ {2, b}⊢ ∀ S ∈ {2, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:3 ≠ bhDsub:{3, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, b}hBp:B ⊆ {3, b}⊢ ∀ S ∈ {3, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:4 ≠ bhDsub:{4, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, b}hBp:B ⊆ {4, b}⊢ ∀ S ∈ {4, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:6 ≠ bhDsub:{6, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, b}hBp:B ⊆ {6, b}⊢ ∀ S ∈ {6, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:12 ≠ bhDsub:{12, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, b}hBp:B ⊆ {12, b}⊢ ∀ S ∈ {12, b}.powerset, ∑ x ∈ S, x ≠ 11 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:1 ≠ bhDsub:{1, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, b}hBp:B ⊆ {1, b}⊢ ∀ S ∈ {1, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:2 ≠ bhDsub:{2, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, b}hBp:B ⊆ {2, b}⊢ ∀ S ∈ {2, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:3 ≠ bhDsub:{3, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, b}hBp:B ⊆ {3, b}⊢ ∀ S ∈ {3, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:4 ≠ bhDsub:{4, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, b}hBp:B ⊆ {4, b}⊢ ∀ S ∈ {4, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:6 ≠ bhDsub:{6, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, b}hBp:B ⊆ {6, b}⊢ ∀ S ∈ {6, b}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3b:ℕhb:b ∈ {1, 2, 3, 4, 6, 12}hab:12 ≠ bhDsub:{12, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, b}hBp:B ⊆ {12, b}⊢ ∀ S ∈ {12, b}.powerset, ∑ x ∈ S, x ≠ 11 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 1hDsub:{12, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 1}hBp:B ⊆ {12, 1}⊢ ∀ S ∈ {12, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 2hDsub:{12, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 2}hBp:B ⊆ {12, 2}⊢ ∀ S ∈ {12, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 3hDsub:{12, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 3}hBp:B ⊆ {12, 3}⊢ ∀ S ∈ {12, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 4hDsub:{12, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 4}hBp:B ⊆ {12, 4}⊢ ∀ S ∈ {12, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 6hDsub:{12, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 6}hBp:B ⊆ {12, 6}⊢ ∀ S ∈ {12, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 12hDsub:{12, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 12}hBp:B ⊆ {12, 12}⊢ ∀ S ∈ {12, 12}.powerset, ∑ x ∈ S, x ≠ 11 hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 1hDsub:{1, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 1}hBp:B ⊆ {1, 1}⊢ ∀ S ∈ {1, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 2hDsub:{1, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 2}hBp:B ⊆ {1, 2}⊢ ∀ S ∈ {1, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 3hDsub:{1, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 3}hBp:B ⊆ {1, 3}⊢ ∀ S ∈ {1, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 4hDsub:{1, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 4}hBp:B ⊆ {1, 4}⊢ ∀ S ∈ {1, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 6hDsub:{1, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 6}hBp:B ⊆ {1, 6}⊢ ∀ S ∈ {1, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:1 ≠ 12hDsub:{1, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{1, 12}hBp:B ⊆ {1, 12}⊢ ∀ S ∈ {1, 12}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 1hDsub:{2, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 1}hBp:B ⊆ {2, 1}⊢ ∀ S ∈ {2, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 2hDsub:{2, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 2}hBp:B ⊆ {2, 2}⊢ ∀ S ∈ {2, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 3hDsub:{2, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 3}hBp:B ⊆ {2, 3}⊢ ∀ S ∈ {2, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 4hDsub:{2, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 4}hBp:B ⊆ {2, 4}⊢ ∀ S ∈ {2, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 6hDsub:{2, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 6}hBp:B ⊆ {2, 6}⊢ ∀ S ∈ {2, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:2 ≠ 12hDsub:{2, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{2, 12}hBp:B ⊆ {2, 12}⊢ ∀ S ∈ {2, 12}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 1hDsub:{3, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 1}hBp:B ⊆ {3, 1}⊢ ∀ S ∈ {3, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 2hDsub:{3, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 2}hBp:B ⊆ {3, 2}⊢ ∀ S ∈ {3, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 3hDsub:{3, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 3}hBp:B ⊆ {3, 3}⊢ ∀ S ∈ {3, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 4hDsub:{3, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 4}hBp:B ⊆ {3, 4}⊢ ∀ S ∈ {3, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 6hDsub:{3, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 6}hBp:B ⊆ {3, 6}⊢ ∀ S ∈ {3, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:3 ≠ 12hDsub:{3, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{3, 12}hBp:B ⊆ {3, 12}⊢ ∀ S ∈ {3, 12}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 1hDsub:{4, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 1}hBp:B ⊆ {4, 1}⊢ ∀ S ∈ {4, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 2hDsub:{4, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 2}hBp:B ⊆ {4, 2}⊢ ∀ S ∈ {4, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 3hDsub:{4, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 3}hBp:B ⊆ {4, 3}⊢ ∀ S ∈ {4, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 4hDsub:{4, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 4}hBp:B ⊆ {4, 4}⊢ ∀ S ∈ {4, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 6hDsub:{4, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 6}hBp:B ⊆ {4, 6}⊢ ∀ S ∈ {4, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:4 ≠ 12hDsub:{4, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{4, 12}hBp:B ⊆ {4, 12}⊢ ∀ S ∈ {4, 12}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 1hDsub:{6, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 1}hBp:B ⊆ {6, 1}⊢ ∀ S ∈ {6, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 2hDsub:{6, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 2}hBp:B ⊆ {6, 2}⊢ ∀ S ∈ {6, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 3hDsub:{6, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 3}hBp:B ⊆ {6, 3}⊢ ∀ S ∈ {6, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 4hDsub:{6, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 4}hBp:B ⊆ {6, 4}⊢ ∀ S ∈ {6, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 6hDsub:{6, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 6}hBp:B ⊆ {6, 6}⊢ ∀ S ∈ {6, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:6 ≠ 12hDsub:{6, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{6, 12}hBp:B ⊆ {6, 12}⊢ ∀ S ∈ {6, 12}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 1hDsub:{12, 1} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 1}hBp:B ⊆ {12, 1}⊢ ∀ S ∈ {12, 1}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 2hDsub:{12, 2} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 2}hBp:B ⊆ {12, 2}⊢ ∀ S ∈ {12, 2}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 3hDsub:{12, 3} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 3}hBp:B ⊆ {12, 3}⊢ ∀ S ∈ {12, 3}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 4hDsub:{12, 4} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 4}hBp:B ⊆ {12, 4}⊢ ∀ S ∈ {12, 4}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 6hDsub:{12, 6} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 6}hBp:B ⊆ {12, 6}⊢ ∀ S ∈ {12, 6}.powerset, ∑ x ∈ S, x ≠ 11hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12} := of_decide_eq_true (id (Eq.refl true))h11:11 ∈ Finset.Icc 1 12 := of_decide_eq_true (id (Eq.refl true))k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3hab:12 ≠ 12hDsub:{12, 12} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{12, 12}hBp:B ⊆ {12, 12}⊢ ∀ S ∈ {12, 12}.powerset, ∑ x ∈ S, x ≠ 11 All goals completed! 🐙 All goals completed! 🐙

For any practical number $n$, $h(n) ≤ number of divisors of $n$.

@[category test, AMS 11] theorem practicalH_le_divisors (n : ℕ) (hn : Nat.IsPractical n) : practicalH n ≤ n.divisors.card := n:ℕhn:n.IsPractical⊢ practicalH n ≤ n.divisors.card n:ℕhn:n.IsPractical⊢ ∀ (b : ℕ), 1 ≤ b ∧ b ≤ n → sInf {k | ∃ D ⊆ n.divisors, D.card = k ∧ b ∈ subsetSums ↑D} ≤ n.divisors.card All goals completed! 🐙

$h(n!)$ is well-defined since $n!$ is practical for $n ≥ 1$.

@[category textbook, AMS 11] theorem factorial_isPractical (n : ℕ) : Nat.IsPractical n.factorial := n:ℕ⊢ n.factorial.IsPractical induction n with ⊢ (Nat.factorial 0).IsPractical intro m m:ℕhm:m ≤ Nat.factorial 0⊢ m ∈ subsetSums ↑(Nat.factorial 0).divisors; m:ℕhm:m ≤ 1⊢ m ∈ subsetSums ↑(Nat.factorial 0).divisors; m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.factorial 0).divisorsm:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.factorial 0).divisors m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.factorial 0).divisors exact ⟨∅, m:ℕhm:0 ≤ 1⊢ ↑∅ ⊆ ↑(Nat.factorial 0).divisors All goals completed! 🐙, m:ℕhm:0 ≤ 1⊢ 0 = ∑ i ∈ ∅, i All goals completed! 🐙⟩ m:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.factorial 0).divisors exact ⟨{1}, m:ℕhm:1 ≤ 1⊢ ↑{1} ⊆ ↑(Nat.factorial 0).divisors All goals completed! 🐙, m:ℕhm:1 ≤ 1⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩ n:ℕih:n.factorial.IsPractical⊢ (n + 1).factorial.IsPractical intro m n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:¬m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors exact subsetSums_mono (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ ↑n.factorial.divisors ⊆ ↑(n + 1).factorial.divisors All goals completed! 🐙) (ih m hle) n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:¬m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors; n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors; n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors obtain ⟨B, hB_sub, hB_sum⟩ := ih q (Nat.div_le_of_le_mul (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)⊢ m ≤ (n + 1) * n.factorial All goals completed! 🐙)) have hdvd : ∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d * (n + 1) ∈ (n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d * (n + 1) ∣ (n + 1).factorial n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1) * n.factorial exact mul_dvd_mul_left _ (Nat.dvd_of_mem_divisors (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d ∈ n.factorial.divisors All goals completed! 🐙)) have hB'_sum : (B.image (· * (n + 1))).sum id = (n + 1) * q := n:ℕ⊢ n.factorial.IsPractical n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩⊢ ∑ x ∈ B, id (x * (n + 1)) = (n + 1) * q All goals completed! 🐙 n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:r = 0⊢ (Finset.image (fun x => x * (n + 1)) B).sum id ∈ subsetSums ↑(n + 1).factorial.divisors exact ⟨_, fun x hx => n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:r = 0x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B)⊢ x ∈ ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:r = 0d:ℕhd:d ∈ Bhx:d * (n + 1) ∈ ↑(Finset.image (fun x => x * (n + 1)) B)⊢ d * (n + 1) ∈ ↑(n + 1).factorial.divisors; All goals completed! 🐙, rfl⟩ n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors have h_disj : Disjoint (B.image (· * (n + 1))) {r} := n:ℕ⊢ n.factorial.IsPractical n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0⊢ ¬∃ a ∈ B, a * (n + 1) = r; n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = r⊢ False have : 0 < d := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = r⊢ d ∈ n.factorial.divisors All goals completed! 🐙)) (Nat.factorial_pos n) n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = rthis✝:0 < d := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n)this:n + 1 ≤ d * (n + 1) := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this✝⊢ False All goals completed! 🐙 n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)⊢ (Finset.image (fun x => x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors exact ⟨_, fun x hx => n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})⊢ x ∈ ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ Finset.image (fun x => x * (n + 1)) B⊢ x ∈ ↑(n + 1).factorial.divisorsn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ x ∈ ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ Finset.image (fun x => x * (n + 1)) B⊢ x ∈ ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)d:ℕhd:d ∈ Bhx:d * (n + 1) ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:d * (n + 1) ∈ Finset.image (fun x => x * (n + 1)) B⊢ d * (n + 1) ∈ ↑(n + 1).factorial.divisors; All goals completed! 🐙 n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ x ∈ ↑(n + 1).factorial.divisors n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ r ∈ ↑(n + 1).factorial.divisors; exact Nat.mem_divisors.mpr ⟨(Nat.dvd_factorial (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ 0 < r All goals completed! 🐙) (n:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)r:ℕ := m % (n + 1)h_div:m = (n + 1) * q + r := Eq.symm (Nat.div_add_mod m (n + 1))h_r_lt:r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => Nat.mem_divisors.mpr ⟨Eq.mpr (id (congrArg (fun _a => _a ∣ (n + 1).factorial) (mul_comm d (n + 1)))) (Eq.mpr (id (congrArg (fun _a => (n + 1) * d ∣ _a) (Nat.factorial_succ n))) (mul_dvd_mul_left (n + 1) (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))))), Nat.factorial_ne_zero (n + 1)⟩hB'_sum:(Finset.image (fun x => x * (n + 1)) B).sum id = (n + 1) * q := Eq.mpr (id (congrArg (fun _a => _a = (n + 1) * q) (Finset.sum_image fun a x b x_1 h => mul_right_cancel₀ (fun a_1 => factorial_isPractical._proof_1 n m B a b a_1) h))) (of_eq_true (Eq.trans (congr (congrArg Eq (Finset.sum_congr (Eq.refl B) fun x a => Eq.refl (x * (n + 1)))) (Eq.trans (Eq.trans (congrArg (HMul.hMul (n + 1)) hB_sum) (Finset.mul_sum B (fun i => i) (n + 1))) (Finset.sum_congr (Eq.refl B) fun x a => mul_comm (n + 1) x))) (eq_self (∑ x ∈ B, x * (n + 1)))))hr:¬r = 0h_disj:Disjoint (Finset.image (fun x => x * (n + 1)) B) {r} := Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.disjoint_singleton_right))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext Finset.mem_image))) fun a => Exists.casesOn a fun d h => And.casesOn h fun hd hdr => have this := Nat.pos_of_dvd_of_pos (Nat.dvd_of_mem_divisors (cast Finset.mem_coe._simp_1 (hB_sub hd))) (Nat.factorial_pos n); have this := le_mul_of_one_le_left (Nat.zero_le (n + 1)) this; factorial_isPractical._proof_3 n m h_r_lt B d hdr this)x:ℕhx:x ∈ ↑(Finset.image (fun x => x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ r ≤ n All goals completed! 🐙)).trans (Nat.factorial_dvd_factorial n.le_succ), Nat.factorial_ne_zero _⟩, rfl⟩

Conjecture 1. Are there infinitely many practical numbers $m$ such that $h(m) < (\log \log m)^{O(1)}$?

More precisely: does there exist a constant $C > 0$ such that for infinitely many practical numbers $m$, we have $h(m) < (\log \log m)^C$?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_18a : answer(sorry) ↔ ∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧ (practicalH m : ℝ) < (log (log m)) ^ C := ⊢ True ↔ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in atTop, m.IsPractical ∧ ↑(practicalH m) < log (log ↑m) ^ C All goals completed! 🐙

Conjecture 2. Is it true that $h(n!) < n^{o(1)}$? That is, for all $\varepsilon > 0$, is $h(n!) < n^\varepsilon$ for sufficiently large $n$?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_18b : answer(sorry) ↔ ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (n : ℝ) ^ ε := ⊢ True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑(practicalH n.factorial) < ↑n ^ ε All goals completed! 🐙

Conjecture 3. Or perhaps even $h(n!) < (\log n)^{O(1)}$?

Erdős offered $250 for a proof or disproof.

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_18c : answer(sorry) ↔ ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (log n) ^ C := ⊢ True ↔ ∃ C, 0 < C ∧ ∀ᶠ (n : ℕ) in atTop, ↑(practicalH n.factorial) < log ↑n ^ C All goals completed! 🐙

Erdős's Theorem. Erdős proved that $h(n!) < n$ for all $n \ge 1$.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_18_upper_bound : ∀ᶠ n : ℕ in atTop, practicalH (Nat.factorial n) < n := ⊢ ∀ᶠ (n : ℕ) in atTop, practicalH n.factorial < n All goals completed! 🐙

Vose's Theorem. Vose proved the existence of infinitely many practical numbers $m$ such that $h(m) \ll (\log m)^{1/2}$. This gives a positive answer to a weaker form of Conjecture 1.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_18_vose : ∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧ (practicalH m : ℝ) < C * (log m) ^ (1 / 2 : ℝ) := ⊢ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in atTop, m.IsPractical ∧ ↑(practicalH m) < C * log ↑m ^ (1 / 2) All goals completed! 🐙 end Erdos18