-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem blocks_partial_sum {i : ℕ} (h : i < c.boundaries.card) :
    (c.blocks.take i).sum = c.boundary ⟨i, h⟩

Proof state:
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < c.boundaries.card
⊢ (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)

Tactic:
induction i with
| zero => simp
| succ i IH =>
  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]
  have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length, Nat.sub_le])
  rw [sum_take_succ _ _ A, IH B]
  simp [blocks, blocksFun, get_ofFn]

Result:
no goals

Proof state:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
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]

Result:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Proof state:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.length + 1
⊢ i < c.blocks.length

Tactic:
simp [blocks, Nat.lt_of_succ_lt_succ h]

Result:
no goals

Proof state:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
⊢ i < c.blocks.length

Tactic:
rw [c.card_boundaries_eq_succ_length] at h

Result:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.length + 1
⊢ i < c.blocks.length

Proof state:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ c.blocks.length ≤ c.boundaries.card

Tactic:
simp [blocks, length, Nat.sub_le]

Result:
no goals

Proof state:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
rw [sum_take_succ _ _ A, IH B]

Result:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ ↑(c.boundary ⟨i, B⟩) + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)

Proof state:
case zero
n : ℕ
c : CompositionAsSet n
h : 0 < c.boundaries.card
⊢ (take 0 c.blocks).sum = ↑(c.boundary ⟨0, h⟩)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length, Nat.sub_le])

Result:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Proof state:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ ↑(c.boundary ⟨i, B⟩) + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
simp [blocks, blocksFun, get_ofFn]

Result:
no goals