numbers expressible as a sum

Stream: Is there code for X?

[Maja Kądziołka]

Do we have a lemma that by summing subsets of Finset.range n, you can obtain any intermediate number? Something like

import Mathlib

example (n : ℕ) : (Finset.range n).powerset.image (Finset.sum · id)
  = Finset.range ((Finset.range n |>.sum id) + 1)  := sorry

[Maja Kądziołka]

I managed to prove this, where would be a good place in Mathlib to put it?

example (n : ℕ) : (Finset.range n).powerset.image (∑ i ∈ ·, i)
    = Finset.range (∑ i ∈ Finset.range n, i + 1) := by
  induction n with
  | zero => simp
  | succ n ih => calc
    (Finset.range (n + 1)).powerset.image (∑ i ∈ ·, i)
    = (Finset.range n).powerset.image (∑ i ∈ ·, i) ∪
      (Finset.range n).powerset.image (∑ i ∈ insert n ·, i) := by
        simp [Finset.range_add_one, Finset.powerset_insert,
          Finset.image_union, Finset.image_image]; congr
    _ = Finset.range (∑ i ∈ Finset.range n, i + 1) ∪
      (Finset.range n).powerset.image (∑ i ∈ insert n ·, i) := by rw [ih]
    _ = Finset.range (∑ i ∈ Finset.range n, i + 1) ∪
      (Finset.range n).powerset.image (n + ∑ i ∈ ·, i) := by
        congr 1; apply Finset.image_congr; intro x hx
        rw [Finset.mem_coe, Finset.mem_powerset] at hx
        simp
        rw [Finset.sum_insert]
        intro h
        simpa using Finset.mem_of_subset hx h
    _ = Finset.range (∑ i ∈ Finset.range n, i + 1) ∪
      ((Finset.range n).powerset.image (∑ i ∈ ·, i)).image (n + ·) := by
        simp [Finset.image_image]; congr
    _ = Finset.range (∑ i ∈ Finset.range n, i + 1) ∪
      (Finset.range (∑ i ∈ Finset.range n, i + 1)).image (n + ·) := by rw [ih]
    _ = Finset.range (n + (∑ i ∈ Finset.range n, i + 1)) := by
      rw [Finset.range_eq_Ico, Finset.image_add_left_Ico, add_zero]
      have h : n ≤ (∑ i ∈ Finset.Ico 0 n, i + 1) := by
        cases n with
        | zero => simp
        | succ n => calc
          n + 1 ≤ n + ∑ i ∈ Finset.Ico 0 n, i + 1 := by simp
          _ = ∑ i ∈ Finset.Ico 0 (n + 1), i + 1 := by
            simp [Finset.range_add_one]
      rw [Finset.Ico_union_Ico' h <| Nat.zero_le _]
      simp
    _ = Finset.range (∑ i ∈ Finset.range (n + 1), i + 1) := by
      simp [@Finset.range_add_one n]; congr 1