∀ (N k : ℕ),
  N.smoothNumbersUpTo k ⊆
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)