n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks (toCompositionAsSet c) = c.blocks
n : ℕ
c : Composition n
⊢ CompositionAsSet.blocks (toCompositionAsSet c) = c.blocks
let d := c.toCompositionAsSet
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks d = c.blocks
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks (toCompositionAsSet c) = c.blocks
change d.blocks = c.blocks
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ CompositionAsSet.blocks d = c.blocks
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks d = c.blocks
have length_eq : d.blocks.length = c.blocks.length := by
  convert c.toCompositionAsSet_length
  simp [CompositionAsSet.blocks]
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
H :
  ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
⊢ CompositionAsSet.blocks d = c.blocks

case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ CompositionAsSet.blocks d = c.blocks
suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
H :
  ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
⊢ CompositionAsSet.blocks d = c.blocks

case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
exact eq_of_sum_take_eq length_eq H
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
⊢ ∀ (i : ℕ),
    i ≤ List.length (CompositionAsSet.blocks d) → sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
intro i hi
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
have i_lt : i < d.boundaries.card := by
  simpa [CompositionAsSet.blocks, length_ofFn, Nat.succ_eq_add_one,
    d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
have i_lt' : i < c.boundaries.card := i_lt
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
A :
  ↑(Finset.orderEmbOfFin d.boundaries (_ : Finset.card d.boundaries = Finset.card d.boundaries))
      { val := i, isLt := i_lt } =
    ↑(Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1)) { val := i, isLt := i_lt'' }
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
have A :
  d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
    c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
  rfl
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
A :
  ↑(Finset.orderEmbOfFin d.boundaries (_ : Finset.card d.boundaries = Finset.card d.boundaries))
      { val := i, isLt := i_lt } =
    ↑(Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1)) { val := i, isLt := i_lt'' }
B : sizeUpTo c i = ↑(↑(boundary c) { val := i, isLt := i_lt'' })
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
A :
  ↑(Finset.orderEmbOfFin d.boundaries (_ : Finset.card d.boundaries = Finset.card d.boundaries))
      { val := i, isLt := i_lt } =
    ↑(Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1)) { val := i, isLt := i_lt'' }
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
no goals
case H
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
i_lt'' : i < length c + 1
A :
  ↑(Finset.orderEmbOfFin d.boundaries (_ : Finset.card d.boundaries = Finset.card d.boundaries))
      { val := i, isLt := i_lt } =
    ↑(Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1)) { val := i, isLt := i_lt'' }
B : sizeUpTo c i = ↑(↑(boundary c) { val := i, isLt := i_lt'' })
⊢ sum (take i (CompositionAsSet.blocks d)) = sum (take i c.blocks)
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
  c.orderEmbOfFin_boundaries]
case h.e'_2
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ List.length (CompositionAsSet.blocks d) = CompositionAsSet.length (toCompositionAsSet c)
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ List.length (CompositionAsSet.blocks d) = List.length c.blocks
convert c.toCompositionAsSet_length
no goals
case h.e'_2
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ List.length (CompositionAsSet.blocks d) = CompositionAsSet.length (toCompositionAsSet c)
simp [CompositionAsSet.blocks]
no goals
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
⊢ i < Finset.card d.boundaries
simpa [CompositionAsSet.blocks, length_ofFn, Nat.succ_eq_add_one,
  d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
no goals
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
length_eq : List.length (CompositionAsSet.blocks d) = List.length c.blocks
i : ℕ
hi : i ≤ List.length (CompositionAsSet.blocks d)
i_lt : i < Finset.card d.boundaries
i_lt' : i < Finset.card (boundaries c)
⊢ i < length c + 1
rwa [c.card_boundaries_eq_succ_length] at i_lt'