FormalConjectures.ErdosProblems.«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 Realnamespace 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 := by⊢ practicalH 1 = 1
  norm_num [subsetSums, practicalH]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 := by⊢ practicalH 2 = 1
  simp only [practicalH, (by decide : Finset.Icc 1 2 = ({1, 2} : Finset ℕ)),
    (by decide : Nat.divisors 2 = ({1, 2} : Finset ℕ)), Finset.sup_insert, Finset.sup_singleton]⊢ 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}, by⊢ {1} ⊆ {1, 2}h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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, rfl, {1}, rfl.subset, by⊢ 1 = ∑ i ∈ {1}, ih1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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⟩)
      (le_csInf ⟨1, {1}, by⊢ {1} ⊆ {1, 2}h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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, rfl, {1}, rfl.subset, by⊢ 1 = ∑ i ∈ {1}, ih1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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⟩ fun k ⟨D, _, hD, B, hB, hm⟩ =>
        hD ▸ Finset.one_le_card.mpr ((Finset.nonempty_iff_ne_empty.mpr fun h => byk:ℕ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 = ∅⊢ Falseh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 simp [h] at hmAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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).mono hB))h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 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 h2 : sInf {k | ∃ D : Finset ℕ, D ⊆ {1, 2} ∧ D.card = k ∧ 2 ∈ subsetSums D} = 1 :=
    le_antisymm (Nat.sInf_le ⟨{2}, byh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1⊢ {2} ⊆ {1, 2}h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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, rfl, {2}, rfl.subset, byh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1⊢ 2 = ∑ i ∈ {2}, ih1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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⟩)
      (le_csInf ⟨1, {2}, byh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1⊢ {2} ⊆ {1, 2}h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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, rfl, {2}, rfl.subset, byh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1⊢ 2 = ∑ i ∈ {2}, ih1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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 simpAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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⟩ fun k ⟨D, _, hD, B, hB, hm⟩ =>
        hD ▸ Finset.one_le_card.mpr ((Finset.nonempty_iff_ne_empty.mpr fun h => byh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1k:ℕ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 = ∅⊢ Falseh1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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 simp [h] at hmAll goals completed! 🐙h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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).mono hB))h1:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 1 ∈ subsetSums ↑D} = 1h2:sInf {k | ∃ D ⊆ {1, 2}, D.card = k ∧ 2 ∈ subsetSums ↑D} = 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
  simp [h1, h2]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 := by⊢ practicalH 6 = 2
  have hdiv : Nat.divisors 6 = ({1, 2, 3, 6} : Finset ℕ) := by decidehdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ practicalH 6 = 2hdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ practicalH 6 = 2
  apply le_antisymmahdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ practicalH 6 ≤ 2ahdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ 2 ≤ practicalH 6
  ·ahdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ practicalH 6 ≤ 2 -- practicalH 6 ≤ 2 : each m in [1,6] is a sum of at most two divisors of 6.
    apply Finset.sup_leahdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ ∀ b ∈ Finset.Icc 1 6, sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ b ∈ subsetSums ↑D} ≤ 2
    intro m hmahdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm:m ∈ Finset.Icc 1 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2
    rw [Finset.mem_Iccahdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm:1 ≤ m ∧ m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2ahdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm:1 ≤ m ∧ m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2] at hmahdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm:1 ≤ m ∧ m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2
    obtain ⟨hm1, hm2⟩ := hmahdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ mhm2:m ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 2
    interval_cases ma.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 2a.«2»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 2a.«3»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 2a.«4»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 2a.«5»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 2a.«6»hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 2
    ·a.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ {1, 2}.card = 2 decideAll goals completed! 🐙, {1}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ ↑{1} ⊆ ↑{1, 2} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 1hm2:1 ≤ 6⊢ 1 = ∑ i ∈ {1}, i decideAll goals completed! 🐙⟩
    ·a.«2»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ {1, 2}.card = 2 decideAll goals completed! 🐙, {2}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ ↑{2} ⊆ ↑{1, 2} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 2hm2:2 ≤ 6⊢ 2 = ∑ i ∈ {2}, i decideAll goals completed! 🐙⟩
    ·a.«3»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ {1, 2}.card = 2 decideAll goals completed! 🐙, {1, 2}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ ↑{1, 2} ⊆ ↑{1, 2} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 3hm2:3 ≤ 6⊢ 3 = ∑ i ∈ {1, 2}, i decideAll goals completed! 🐙⟩
    ·a.«4»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ {1, 3}.card = 2 decideAll goals completed! 🐙, {1, 3}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ ↑{1, 3} ⊆ ↑{1, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 4hm2:4 ≤ 6⊢ 4 = ∑ i ∈ {1, 3}, i decideAll goals completed! 🐙⟩
    ·a.«5»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ {2, 3}.card = 2 decideAll goals completed! 🐙, {2, 3}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ ↑{2, 3} ⊆ ↑{2, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 5hm2:5 ≤ 6⊢ 5 = ∑ i ∈ {2, 3}, i decideAll goals completed! 🐙⟩
    ·a.«6»hdiv:Nat.divisors 6 = {1, 2, 3, 6}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}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ {1, 6}.card = 2 decideAll goals completed! 🐙, {6}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ ↑{6} ⊆ ↑{1, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}m:ℕhm1:1 ≤ 6hm2:6 ≤ 6⊢ 6 = ∑ i ∈ {6}, i decideAll goals completed! 🐙⟩
  ·ahdiv:Nat.divisors 6 = {1, 2, 3, 6}⊢ 2 ≤ practicalH 6 -- 2 ≤ practicalH 6, witnessed by m = 4 (which needs two divisors: 4 = 1 + 3).
    have h4 : (4 : ℕ) ∈ Finset.Icc 1 6 := by⊢ practicalH 6 = 2ahdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ 2 ≤ practicalH 6 decideahdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ 2 ≤ practicalH 6ahdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ 2 ≤ practicalH 6
    refine le_trans ?_ (Finset.le_sup h4)ahdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ 2 ≤ sInf {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}
    apply le_csInfa.h₁hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}.Nonemptyh₂hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}, 2 ≤ b
    ·a.h₁hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}.Nonempty exact ⟨2, {1, 3}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {1, 3} ⊆ Nat.divisors 6 rw [hdivhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {1, 3} ⊆ {1, 2, 3, 6}hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {1, 3} ⊆ {1, 2, 3, 6}]hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {1, 3} ⊆ {1, 2, 3, 6}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ {1, 3}.card = 2 decideAll goals completed! 🐙, {1, 3}, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ ↑{1, 3} ⊆ ↑{1, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ 4 = ∑ i ∈ {1, 3}, i decideAll goals completed! 🐙⟩
    ·h₂hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 6, D.card = k ∧ 4 ∈ subsetSums ↑D}, 2 ≤ b rintro k ⟨D, hDsub, hDcard, B, hBsub, hBsum⟩h₂hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, i⊢ 2 ≤ k
      by_contra! hkh₂hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihk:k < 2⊢ False
      interval_cases kh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 2⊢ Falseh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 2⊢ False
      ·h₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕ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.
        rw [Finset.card_eq_zeroh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 2⊢ Falseh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 2⊢ False] at hDcardh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 2⊢ False
        subst hDcardh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑∅⊢ False
        rw [Finset.coe_empty,h₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:↑B ⊆ ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ False Set.subset_empty_iff,h₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:↑B = ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ False Finset.coe_eq_emptyh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ False] at hBsubh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsub:B = ∅⊢ False
        subst hBsubh₂.«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:0 < 2hDsub:∅ ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ False
        simp at hBsumAll goals completed! 🐙
      ·h₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕ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.
        rw [Finset.card_eq_oneh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 2⊢ Falseh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 2⊢ False] at hDcardh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 6B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:4 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 2⊢ False
        obtain ⟨d, rfl⟩ := hDcardh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}⊢ False
        have hd : d ∈ Nat.divisors 6 := hDsub (byhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}⊢ d ∈ {d}h₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 6⊢ False simpAll goals completed! 🐙h₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 6⊢ False)h₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 6⊢ False
        rw [hdivh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 6}⊢ Falseh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 6}⊢ False] at hdh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 6}⊢ False
        rw [Finset.coe_subset,h₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B ⊆ {d}hd:d ∈ {1, 2, 3, 6}⊢ Falseh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 6}⊢ False Finset.subset_singleton_iffh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 6}⊢ Falseh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 6}⊢ False] at hBsubh₂.«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2d:ℕhDsub:{d} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {d}hd:d ∈ {1, 2, 3, 6}⊢ False
        fin_cases hdh₂.«1».«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {1}⊢ Falseh₂.«1».«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {2}⊢ Falseh₂.«1».«2»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {3}⊢ Falseh₂.«1».«3»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {6}⊢ False <;>h₂.«1».«0»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {1}⊢ Falseh₂.«1».«1»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {2}⊢ Falseh₂.«1».«2»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {3}⊢ Falseh₂.«1».«3»hdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsub:B = ∅ ∨ B = {6}⊢ False
          rcases hBsub with h | hh₂.«1».«3».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = ∅⊢ Falseh₂.«1».«3».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = {6}⊢ False <;>h₂.«1».«0».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6h:B = ∅⊢ Falseh₂.«1».«0».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{1} ⊆ Nat.divisors 6h:B = {1}⊢ Falseh₂.«1».«1».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6h:B = ∅⊢ Falseh₂.«1».«1».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{2} ⊆ Nat.divisors 6h:B = {2}⊢ Falseh₂.«1».«2».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6h:B = ∅⊢ Falseh₂.«1».«2».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{3} ⊆ Nat.divisors 6h:B = {3}⊢ Falseh₂.«1».«3».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = ∅⊢ Falseh₂.«1».«3».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕB:Finset ℕhBsum:4 = ∑ i ∈ B, ihk:1 < 2hDsub:{6} ⊆ Nat.divisors 6h:B = {6}⊢ False subst hh₂.«1».«3».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {6}, i⊢ False <;>h₂.«1».«0».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«0».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{1} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {1}, i⊢ Falseh₂.«1».«1».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«1».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{2} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {2}, i⊢ Falseh₂.«1».«2».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«2».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{3} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {3}, i⊢ Falseh₂.«1».«3».inlhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«3».inrhdiv:Nat.divisors 6 = {1, 2, 3, 6}h4:4 ∈ Finset.Icc 1 6k:ℕhk:1 < 2hDsub:{6} ⊆ Nat.divisors 6hBsum:4 = ∑ i ∈ {6}, i⊢ False simp at hBsumAll 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 := by⊢ practicalH 12 = 3
  have hdiv : Nat.divisors 12 = ({1, 2, 3, 4, 6, 12} : Finset ℕ) := by decidehdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ practicalH 12 = 3hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ practicalH 12 = 3
  apply le_antisymmahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ practicalH 12 ≤ 3ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ 3 ≤ practicalH 12
  ·ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ practicalH 12 ≤ 3 -- practicalH 12 ≤ 3 : each m in [1,12] is a sum of at most three divisors of 12.
    apply Finset.sup_leahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ ∀ b ∈ Finset.Icc 1 12, sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ b ∈ subsetSums ↑D} ≤ 3
    intro m hmahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm:m ∈ Finset.Icc 1 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3
    rw [Finset.mem_Iccahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm:1 ≤ m ∧ m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm:1 ≤ m ∧ m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3] at hmahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm:1 ≤ m ∧ m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3
    obtain ⟨hm1, hm2⟩ := hmahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ mhm2:m ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ m ∈ subsetSums ↑D} ≤ 3
    interval_cases ma.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 1 ∈ subsetSums ↑D} ≤ 3a.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 2 ∈ subsetSums ↑D} ≤ 3a.«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 3 ∈ subsetSums ↑D} ≤ 3a.«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 4 ∈ subsetSums ↑D} ≤ 3a.«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 5 ∈ subsetSums ↑D} ≤ 3a.«6»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 6 ∈ subsetSums ↑D} ≤ 3a.«7»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 7 ∈ subsetSums ↑D} ≤ 3a.«8»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 8 ∈ subsetSums ↑D} ≤ 3a.«9»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 9 ∈ subsetSums ↑D} ≤ 3a.«10»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 10 ∈ subsetSums ↑D} ≤ 3a.«11»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D} ≤ 3a.«12»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 12 ∈ subsetSums ↑D} ≤ 3
    ·a.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ {1, 2, 3}.card = 3 decideAll goals completed! 🐙, {1}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ ↑{1} ⊆ ↑{1, 2, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 1hm2:1 ≤ 12⊢ 1 = ∑ i ∈ {1}, i decideAll goals completed! 🐙⟩
    ·a.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ {1, 2, 3}.card = 3 decideAll goals completed! 🐙, {2}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ ↑{2} ⊆ ↑{1, 2, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 2hm2:2 ≤ 12⊢ 2 = ∑ i ∈ {2}, i decideAll goals completed! 🐙⟩
    ·a.«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ {1, 2, 3}.card = 3 decideAll goals completed! 🐙, {3}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ ↑{3} ⊆ ↑{1, 2, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 3hm2:3 ≤ 12⊢ 3 = ∑ i ∈ {3}, i decideAll goals completed! 🐙⟩
    ·a.«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ {1, 4, 6}.card = 3 decideAll goals completed! 🐙, {4}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ ↑{4} ⊆ ↑{1, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 4hm2:4 ≤ 12⊢ 4 = ∑ i ∈ {4}, i decideAll goals completed! 🐙⟩
    ·a.«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ {1, 4, 6}.card = 3 decideAll goals completed! 🐙, {1, 4}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ ↑{1, 4} ⊆ ↑{1, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 5hm2:5 ≤ 12⊢ 5 = ∑ i ∈ {1, 4}, i decideAll goals completed! 🐙⟩
    ·a.«6»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ {1, 2, 3}.card = 3 decideAll goals completed! 🐙, {1, 2, 3}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ ↑{1, 2, 3} ⊆ ↑{1, 2, 3} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 6hm2:6 ≤ 12⊢ 6 = ∑ i ∈ {1, 2, 3}, i decideAll goals completed! 🐙⟩
    ·a.«7»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ {1, 4, 6}.card = 3 decideAll goals completed! 🐙, {1, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ ↑{1, 6} ⊆ ↑{1, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 7hm2:7 ≤ 12⊢ 7 = ∑ i ∈ {1, 6}, i decideAll goals completed! 🐙⟩
    ·a.«8»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ {2, 4, 6}.card = 3 decideAll goals completed! 🐙, {2, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ ↑{2, 6} ⊆ ↑{2, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 8hm2:8 ≤ 12⊢ 8 = ∑ i ∈ {2, 6}, i decideAll goals completed! 🐙⟩
    ·a.«9»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ {3, 4, 6}.card = 3 decideAll goals completed! 🐙, {3, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ ↑{3, 6} ⊆ ↑{3, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 9hm2:9 ≤ 12⊢ 9 = ∑ i ∈ {3, 6}, i decideAll goals completed! 🐙⟩
    ·a.«10»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ {4, 6, 12}.card = 3 decideAll goals completed! 🐙, {4, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ ↑{4, 6} ⊆ ↑{4, 6, 12} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 10hm2:10 ≤ 12⊢ 10 = ∑ i ∈ {4, 6}, i decideAll goals completed! 🐙⟩
    ·a.«11»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ {1, 4, 6}.card = 3 decideAll goals completed! 🐙, {1, 4, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ ↑{1, 4, 6} ⊆ ↑{1, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 11hm2:11 ≤ 12⊢ 11 = ∑ i ∈ {1, 4, 6}, i decideAll goals completed! 🐙⟩
    ·a.«12»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}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}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ {2, 4, 6}.card = 3 decideAll goals completed! 🐙, {2, 4, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ ↑{2, 4, 6} ⊆ ↑{2, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}m:ℕhm1:1 ≤ 12hm2:12 ≤ 12⊢ 12 = ∑ i ∈ {2, 4, 6}, i decideAll goals completed! 🐙⟩
  ·ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}⊢ 3 ≤ practicalH 12 -- 3 ≤ practicalH 12, witnessed by m = 11 (needs three divisors: 11 = 1 + 4 + 6).
    have h11 : (11 : ℕ) ∈ Finset.Icc 1 12 := by⊢ practicalH 12 = 3ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ 3 ≤ practicalH 12 decideahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ 3 ≤ practicalH 12ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ 3 ≤ practicalH 12
    refine le_trans ?_ (Finset.le_sup h11)ahdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ 3 ≤ sInf {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}
    apply le_csInfa.h₁hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}.Nonemptyh₂hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}, 3 ≤ b
    ·a.h₁hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}.Nonempty exact ⟨3, {1, 4, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {1, 4, 6} ⊆ Nat.divisors 12 rw [hdivhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}]hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {1, 4, 6} ⊆ {1, 2, 3, 4, 6, 12}; decideAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ {1, 4, 6}.card = 3 decideAll goals completed! 🐙, {1, 4, 6}, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ ↑{1, 4, 6} ⊆ ↑{1, 4, 6} simpAll goals completed! 🐙, byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ 11 = ∑ i ∈ {1, 4, 6}, i decideAll goals completed! 🐙⟩
    ·h₂hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12⊢ ∀ b ∈ {k | ∃ D ⊆ Nat.divisors 12, D.card = k ∧ 11 ∈ subsetSums ↑D}, 3 ≤ b rintro k ⟨D, hDsub, hDcard, B, hBsub, hBsum⟩h₂hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, i⊢ 3 ≤ k
      by_contra! hkh₂hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12hDcard:D.card = kB:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihk:k < 3⊢ False
      interval_cases kh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 3⊢ Falseh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 3⊢ Falseh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 2hk:2 < 3⊢ False
      ·h₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 0hk:0 < 3⊢ False rw [Finset.card_eq_zeroh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 3⊢ Falseh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 3⊢ False] at hDcardh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D = ∅hk:0 < 3⊢ False
        subst hDcardh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑∅⊢ False
        rw [Finset.coe_empty,h₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:↑B ⊆ ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ False Set.subset_empty_iff,h₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:↑B = ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ False Finset.coe_eq_emptyh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ Falseh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ False] at hBsubh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsub:B = ∅⊢ False
        subst hBsubh₂.«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:0 < 3hDsub:∅ ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ False
        simp at hBsumAll goals completed! 🐙
      ·h₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 1hk:1 < 3⊢ False rw [Finset.card_eq_oneh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 3⊢ Falseh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 3⊢ False] at hDcardh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:∃ a, D = {a}hk:1 < 3⊢ False
        obtain ⟨d, rfl⟩ := hDcardh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}⊢ False
        have hd : d ∈ Nat.divisors 12 := hDsub (byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}⊢ d ∈ {d}h₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 12⊢ False simpAll goals completed! 🐙h₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 12⊢ False)h₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}hd:d ∈ Nat.divisors 12⊢ False
        rw [hdivh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{d}hd:d ∈ {1, 2, 3, 4, 6, 12}⊢ Falseh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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] at hdh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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
        rw [Finset.coe_subset,h₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3d:ℕhDsub:{d} ⊆ Nat.divisors 12hBsub:B ⊆ {d}hd:d ∈ {1, 2, 3, 4, 6, 12}⊢ Falseh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 Finset.subset_singleton_iffh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}⊢ Falseh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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] at hBsubh₂.«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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
        fin_cases hdh₂.«1».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {1}⊢ Falseh₂.«1».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {2}⊢ Falseh₂.«1».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {3}⊢ Falseh₂.«1».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {4}⊢ Falseh₂.«1».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {6}⊢ Falseh₂.«1».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {12}⊢ False <;>h₂.«1».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {1}⊢ Falseh₂.«1».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {2}⊢ Falseh₂.«1».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {3}⊢ Falseh₂.«1».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {4}⊢ Falseh₂.«1».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {6}⊢ Falseh₂.«1».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsub:B = ∅ ∨ B = {12}⊢ False rcases hBsub with h | hh₂.«1».«5».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«5».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = {12}⊢ False <;>h₂.«1».«0».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«0».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{1} ⊆ Nat.divisors 12h:B = {1}⊢ Falseh₂.«1».«1».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«1».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{2} ⊆ Nat.divisors 12h:B = {2}⊢ Falseh₂.«1».«2».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«2».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{3} ⊆ Nat.divisors 12h:B = {3}⊢ Falseh₂.«1».«3».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«3».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{4} ⊆ Nat.divisors 12h:B = {4}⊢ Falseh₂.«1».«4».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«4».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{6} ⊆ Nat.divisors 12h:B = {6}⊢ Falseh₂.«1».«5».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = ∅⊢ Falseh₂.«1».«5».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:1 < 3hDsub:{12} ⊆ Nat.divisors 12h:B = {12}⊢ False subst hh₂.«1».«5».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {12}, i⊢ False <;>h₂.«1».«0».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«0».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{1} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {1}, i⊢ Falseh₂.«1».«1».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«1».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{2} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {2}, i⊢ Falseh₂.«1».«2».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«2».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{3} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {3}, i⊢ Falseh₂.«1».«3».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«3».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{4} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {4}, i⊢ Falseh₂.«1».«4».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«4».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{6} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {6}, i⊢ Falseh₂.«1».«5».inlhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ ∅, i⊢ Falseh₂.«1».«5».inrhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕhk:1 < 3hDsub:{12} ⊆ Nat.divisors 12hBsum:11 = ∑ i ∈ {12}, i⊢ False simp at hBsumAll goals completed! 🐙
      ·h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕD:Finset ℕhDsub:D ⊆ Nat.divisors 12B:Finset ℕhBsub:↑B ⊆ ↑DhBsum:11 = ∑ i ∈ B, ihDcard:D.card = 2hk:2 < 3⊢ False rw [Finset.card_eq_twoh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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⊢ Falseh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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] at hDcardh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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
        obtain ⟨a, b, hab, rfl⟩ := hDcardh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 (byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕB:Finset ℕhBsum:11 = ∑ i ∈ B, ihk:2 < 3a:ℕb:ℕhab:a ≠ bhDsub:{a, b} ⊆ Nat.divisors 12hBsub:↑B ⊆ ↑{a, b}⊢ a ∈ {a, b}h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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⊢ False simpAll goals completed! 🐙h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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⊢ False)h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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⊢ False
        have hb : b ∈ Nat.divisors 12 := hDsub (byhdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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⊢ b ∈ {a, b}h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 12hb:b ∈ Nat.divisors 12⊢ False simpAll goals completed! 🐙h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 12hb:b ∈ Nat.divisors 12⊢ False)h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 12hb:b ∈ Nat.divisors 12⊢ False
        rw [hdivh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}⊢ Falseh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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] at ha hbh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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
        have hBp : B ⊆ ({a, b} : Finset ℕ) := Finset.coe_subset.mp hBsubh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}⊢ False
        have key : ∀ S ∈ ({a, b} : Finset ℕ).powerset, S.sum (fun x => x) ≠ 11 := by⊢ practicalH 12 = 3h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False
          fin_cases ha«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False <;>«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False fin_cases hb«5».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False <;>«0».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«0».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«0».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«0».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«0».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«0».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«1».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«2».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«3».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«4».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«0»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«1»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«3»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«4»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11«5».«5»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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 ≠ 11h₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False decideh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ Falseh₂.«2»hdiv:Nat.divisors 12 = {1, 2, 3, 4, 6, 12}h11:11 ∈ Finset.Icc 1 12k:ℕ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}key:∀ S ∈ {a, b}.powerset, ∑ x ∈ S, x ≠ 11⊢ False
        exact key B (Finset.mem_powerset.mpr hBp) hBsum.symmAll 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 := byn:ℕhn:n.IsPractical⊢ practicalH n ≤ n.divisors.card
  simp only [practicalH, Finset.sup_le_iff, Finset.mem_Icc]n:ℕhn:n.IsPractical⊢ ∀ (b : ℕ), 1 ≤ b ∧ b ≤ n → sInf {k | ∃ D ⊆ n.divisors, D.card = k ∧ b ∈ subsetSums ↑D} ≤ n.divisors.card
  exact fun m ⟨_, hm⟩ => Nat.sInf_le ⟨n.divisors, Finset.Subset.refl _, rfl, hn m hm⟩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 := byn:ℕ⊢ n.factorial.IsPractical
    induction n with
  | zero =>zero⊢ (Nat.factorial 0).IsPractical
    intro m hmzerom:ℕhm:m ≤ Nat.factorial 0⊢ m ∈ subsetSums ↑(Nat.factorial 0).divisors; simp at hmzerom:ℕhm:m ≤ 1⊢ m ∈ subsetSums ↑(Nat.factorial 0).divisors; interval_cases mzero.«0»m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.factorial 0).divisorszero.«1»m:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.factorial 0).divisors
    ·zero.«0»m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.factorial 0).divisors exact ⟨∅, bym:ℕhm:0 ≤ 1⊢ ↑∅ ⊆ ↑(Nat.factorial 0).divisors simpAll goals completed! 🐙, bym:ℕhm:0 ≤ 1⊢ 0 = ∑ i ∈ ∅, i simpAll goals completed! 🐙⟩
    ·zero.«1»m:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.factorial 0).divisors exact ⟨{1}, bym:ℕhm:1 ≤ 1⊢ ↑{1} ⊆ ↑(Nat.factorial 0).divisors simpAll goals completed! 🐙, bym:ℕhm:1 ≤ 1⊢ 1 = ∑ i ∈ {1}, i simpAll goals completed! 🐙⟩
  | succ n ih =>succn:ℕih:n.factorial.IsPractical⊢ (n + 1).factorial.IsPractical
    intro m hmsuccn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
    by_cases hle : m ≤ n.factorialposn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsnegn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:¬m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
    ·posn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors exact subsetSums_mono (byn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:m ≤ n.factorial⊢ ↑n.factorial.divisors ⊆ ↑(n + 1).factorial.divisors exact_mod_cast (Nat.divisors_subset_of_dvd
        (Nat.factorial_ne_zero _) (Nat.factorial_dvd_factorial n.le_succ))All goals completed! 🐙) (ih m hle)
    ·negn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:¬m ≤ n.factorial⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors push Not at hlenegn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1).factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors; rw [Nat.factorial_succnegn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsnegn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors] at hmnegn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < m⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      set q := m / (n + 1)negn:ℕih:n.factorial.IsPracticalm:ℕhm:m ≤ (n + 1) * n.factorialhle:n.factorial < mq:ℕ := m / (n + 1)⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors; set r := m % (n + 1)negn:ℕ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
      have h_div : m = (n + 1) * q + r := (Nat.div_add_mod m (n + 1)).symmnegn:ℕ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⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      have h_r_lt : r < n + 1 := Nat.mod_lt m (Nat.succ_pos n)negn:ℕ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 + rh_r_lt:r < n + 1⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      obtain ⟨B, hB_sub, hB_sum⟩ := ih q (Nat.div_le_of_le_mul (byn:ℕ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 + rh_r_lt:r < n + 1⊢ m ≤ (n + 1) * n.factorialnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, i⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors linarithAll goals completed! 🐙negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, i⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors))negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, i⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      have hdvd : ∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors := fun d hd => byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d * (n + 1) ∈ (n + 1).factorial.divisorsnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        refine Nat.mem_divisors.mpr ⟨?_, Nat.factorial_ne_zero _⟩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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d * (n + 1) ∣ (n + 1).factorialnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        rw [mul_comm,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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1).factorialn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1) * n.factorialnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors Nat.factorial_succn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1) * n.factorialn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1) * n.factorialnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ (n + 1) * d ∣ (n + 1) * n.factorialnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        exact mul_dvd_mul_left _ (Nat.dvd_of_mem_divisors (byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, id:ℕhd:d ∈ B⊢ d ∈ n.factorial.divisorsnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors exact_mod_cast hB_sub hdAll goals completed! 🐙negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors))negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      have hB'_sum : (B.image (· * (n + 1))).sum id = (n + 1) * q := byn:ℕ⊢ n.factorial.IsPracticalnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        rw [Finset.sum_image (fun a _ b _ h => mul_right_cancel₀ (byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorsa:ℕx✝¹:a ∈ ↑Bb:ℕx✝:b ∈ ↑Bh:a * (n + 1) = b * (n + 1)⊢ n + 1 ≠ 0n:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ ∑ x ∈ B, id (x * (n + 1)) = (n + 1) * qnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors omegaAll 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ ∑ x ∈ B, id (x * (n + 1)) = (n + 1) * qnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors) h)]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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisors⊢ ∑ x ∈ B, id (x * (n + 1)) = (n + 1) * qnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        simp [Finset.mul_sum, mul_comm, hB_sum]negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * q⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      by_cases hr : r = 0posn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
      ·posn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors rw [show m = (B.image (· * (n + 1))).sum id from byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m = (Finset.image (fun x ↦ x * (n + 1)) B).sum idposn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ (Finset.image (fun x ↦ x * (n + 1)) B).sum id ∈ subsetSums ↑(n + 1).factorial.divisors rw [hB'_sumn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m = (n + 1) * qn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m = (n + 1) * qposn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ (Finset.image (fun x ↦ x * (n + 1)) B).sum id ∈ 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ m = (n + 1) * qposn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ (Finset.image (fun x ↦ x * (n + 1)) B).sum id ∈ subsetSums ↑(n + 1).factorial.divisors; omegaAll goals completed! 🐙posn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ (Finset.image (fun x ↦ x * (n + 1)) B).sum id ∈ subsetSums ↑(n + 1).factorial.divisors]posn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0⊢ (Finset.image (fun x ↦ x * (n + 1)) B).sum id ∈ subsetSums ↑(n + 1).factorial.divisors
        exact ⟨_, fun x hx => byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B)⊢ x ∈ ↑(n + 1).factorial.divisors
          obtain ⟨d, hd, rfl⟩ := Finset.mem_image.mp hxn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:r = 0d:ℕhd:d ∈ Bhx:d * (n + 1) ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B)⊢ d * (n + 1) ∈ ↑(n + 1).factorial.divisors; exact hdvd d hdAll goals completed! 🐙, rfl⟩
      ·negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors have h_disj : Disjoint (B.image (· * (n + 1))) {r} := byn:ℕ⊢ n.factorial.IsPracticalnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
          rw [Finset.disjoint_singleton_right,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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ r ∉ Finset.image (fun x ↦ x * (n + 1)) Bn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ ¬∃ a ∈ B, a * (n + 1) = rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors Finset.mem_imagen:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ ¬∃ a ∈ B, a * (n + 1) = rn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ ¬∃ a ∈ B, a * (n + 1) = rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0⊢ ¬∃ a ∈ B, a * (n + 1) = rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors; rintro ⟨d, hd, hdr⟩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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = r⊢ Falsenegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
          have : 0 < d := Nat.pos_of_dvd_of_pos
            (Nat.dvd_of_mem_divisors (byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = r⊢ d ∈ n.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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = rthis:0 < d⊢ Falsenegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors exact_mod_cast hB_sub hdAll 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = rthis:0 < d⊢ Falsenegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors)) (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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = rthis:0 < d⊢ Falsenegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
          have := le_mul_of_one_le_left (Nat.zero_le (n + 1)) thisn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0d:ℕhd:d ∈ Bhdr:d * (n + 1) = rthis✝:0 < dthis:n + 1 ≤ d * (n + 1)⊢ Falsenegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
          omeganegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisorsnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m ∈ subsetSums ↑(n + 1).factorial.divisors
        rw [show m = (B.image (· * (n + 1)) ∪ {r}).sum id from byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum idnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors
          rw [Finset.sum_union h_disj,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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = ∑ x ∈ Finset.image (fun x ↦ x * (n + 1)) B, id x + ∑ x ∈ {r}, id xn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors Finset.sum_singleton,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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = ∑ x ∈ Finset.image (fun x ↦ x * (n + 1)) B, id x + id rn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors hB'_sum,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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + id rn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors id_eqn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ 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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ m = (n + 1) * q + rnegn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors; exact h_divAll goals completed! 🐙negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors]negn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}⊢ (Finset.image (fun x ↦ x * (n + 1)) B ∪ {r}).sum id ∈ subsetSums ↑(n + 1).factorial.divisors
        exact ⟨_, fun x hx => byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})⊢ x ∈ ↑(n + 1).factorial.divisors
          rcases Finset.mem_union.mp hx with h | hinln:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}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.divisorsinrn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ x ∈ ↑(n + 1).factorial.divisors
          ·inln:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}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 obtain ⟨d, hd, rfl⟩ := Finset.mem_image.mp hinln:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}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; exact hdvd d hdAll goals completed! 🐙
          ·inrn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ x ∈ ↑(n + 1).factorial.divisors rw [Finset.mem_singleton.mp hinrn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ r ∈ ↑(n + 1).factorial.divisorsinrn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ r ∈ ↑(n + 1).factorial.divisors]inrn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}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 (byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ 0 < r omegaAll goals completed! 🐙) (byn:ℕ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 + rh_r_lt:r < n + 1B:Finset ℕhB_sub:↑B ⊆ ↑n.factorial.divisorshB_sum:q = ∑ i ∈ B, ihdvd:∀ d ∈ B, d * (n + 1) ∈ (n + 1).factorial.divisorshB'_sum:(Finset.image (fun x ↦ x * (n + 1)) B).sum id = (n + 1) * qhr:¬r = 0h_disj:Disjoint (Finset.image (fun x ↦ x * (n + 1)) B) {r}x:ℕhx:x ∈ ↑(Finset.image (fun x ↦ x * (n + 1)) B ∪ {r})h:x ∈ {r}⊢ r ≤ n omegaAll 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 erdos_18a : answer(sorry) ↔
    ∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧
      (practicalH m : ℝ) < (log (log m)) ^ C := by⊢ True ↔ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in atTop, m.IsPractical ∧ ↑(practicalH m) < log (log ↑m) ^ C
  sorryAll 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 erdos_18b : answer(sorry) ↔
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (n : ℝ) ^ ε := by⊢ True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑(practicalH n.factorial) < ↑n ^ ε
  sorryAll 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 erdos_18c : answer(sorry) ↔
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (log n) ^ C := by⊢ True ↔ ∃ C, 0 < C ∧ ∀ᶠ (n : ℕ) in atTop, ↑(practicalH n.factorial) < log ↑n ^ C
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 11]
theorem erdos_18_upper_bound :
    ∀ᶠ n : ℕ in atTop, practicalH (Nat.factorial n) < n := by⊢ ∀ᶠ (n : ℕ) in atTop, practicalH n.factorial < n
  sorryAll 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 erdos_18_vose :
    ∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧
      (practicalH m : ℝ) < C * (log m) ^ (1 / 2 : ℝ) := by⊢ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in atTop, m.IsPractical ∧ ↑(practicalH m) < C * log ↑m ^ (1 / 2)
  sorryAll goals completed! 🐙

end Erdos18