-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem Composition.toCompositionAsSet_blocks (c : Composition n) :
    c.toCompositionAsSet.blocks = c.blocks

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks = c.blocks

Tactic:
have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ d.blocks = c.blocks

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ i < c.length + 1

Tactic:
rwa [c.card_boundaries_eq_succ_length] at i_lt'

Result:
no goals

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have i_lt' : i < c.boundaries.card := i_lt

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ ∀ i ≤ d.blocks.length, (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
intro i hi

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
let d := c.toCompositionAsSet

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ c.toCompositionAsSet.blocks = c.blocks

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ d.blocks = c.blocks

Tactic:
suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from
  eq_of_sum_take_eq length_eq H

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ ∀ i ≤ d.blocks.length, (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have i_lt : i < d.boundaries.card := by
  simpa [CompositionAsSet.blocks, length_ofFn,
    d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
change d.blocks = c.blocks

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks = c.blocks

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks.length = c.blocks.length

Tactic:
simp [d, blocks_length]

Result:
no goals

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have A :
  d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
    c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
  rfl

Result:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
⊢ i < d.boundaries.card

Tactic:
simpa [CompositionAsSet.blocks, length_ofFn,
  d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi

Result:
no goals

Proof state:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
  c.orderEmbOfFin_boundaries]

Result:
no goals