case zero
n : ℕ
c : CompositionAsSet n
i : ℕ
h✝ : i < Finset.card c.boundaries
h : Nat.zero < Finset.card c.boundaries
⊢ sum (take Nat.zero (blocks c)) = ↑(↑(boundary c) { val := Nat.zero, isLt := h })

case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < Finset.card c.boundaries
⊢ sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
induction' i with i IH
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
have A : i < c.blocks.length := by
  rw [c.card_boundaries_eq_succ_length] at h
  simp [blocks, Nat.lt_of_succ_lt_succ h]
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length, Nat.sub_le])
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) + nthLe (blocks c) i A = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ sum (take (Nat.succ i) (blocks c)) = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
rw [sum_take_succ _ _ A, IH B]
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) +
      (↑(↑(boundary c)
            { val := i + 1, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } + 1 < Finset.card c.boundaries) }) -
        ↑(↑(boundary c)
            { val := i, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } < Finset.card c.boundaries) })) =
    ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) + nthLe (blocks c) i A = ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
simp only [blocks, blocksFun, nthLe_ofFn']
case succ.h
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) ≤
    ↑(↑(boundary c)
        { val := i + 1, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } + 1 < Finset.card c.boundaries) })
case succ
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) +
      (↑(↑(boundary c)
            { val := i + 1, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } + 1 < Finset.card c.boundaries) }) -
        ↑(↑(boundary c)
            { val := i, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } < Finset.card c.boundaries) })) =
    ↑(↑(boundary c) { val := Nat.succ i, isLt := h })
apply add_tsub_cancel_of_le
no goals
case succ.h
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
B : i < Finset.card c.boundaries
⊢ ↑(↑(boundary c) { val := i, isLt := B }) ≤
    ↑(↑(boundary c)
        { val := i + 1, isLt := (_ : ↑{ val := i, isLt := (_ : i < length c) } + 1 < Finset.card c.boundaries) })
simp
no goals
case zero
n : ℕ
c : CompositionAsSet n
i : ℕ
h✝ : i < Finset.card c.boundaries
h : Nat.zero < Finset.card c.boundaries
⊢ sum (take Nat.zero (blocks c)) = ↑(↑(boundary c) { val := Nat.zero, isLt := h })
simp
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < length c + 1
⊢ i < List.length (blocks c)
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
⊢ i < List.length (blocks c)
rw [c.card_boundaries_eq_succ_length] at h
no goals
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < length c + 1
⊢ i < List.length (blocks c)
simp [blocks, Nat.lt_of_succ_lt_succ h]
no goals
n : ℕ
c : CompositionAsSet n
i✝ : ℕ
h✝ : i✝ < Finset.card c.boundaries
i : ℕ
IH : ∀ (h : i < Finset.card c.boundaries), sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
h : Nat.succ i < Finset.card c.boundaries
A : i < List.length (blocks c)
⊢ List.length (blocks c) ≤ Finset.card c.boundaries
simp [blocks, length, Nat.sub_le]