[GOAL]
n : ℕ
c : Composition n
⊢ ∑ i : Fin (length c), blocksFun c i = n
[PROOFSTEP]
conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
[GOAL]
n : ℕ
c : Composition n
⊢ length c ≤ n
[PROOFSTEP]
conv_rhs => rw [← c.blocks_sum]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum]
[GOAL]
n : ℕ
c : Composition n
| n
[PROOFSTEP]
rw [← c.blocks_sum]
[GOAL]
n : ℕ
c : Composition n
⊢ length c ≤ sum c.blocks
[PROOFSTEP]
exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi
[GOAL]
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < length c
[PROOFSTEP]
apply length_pos_of_sum_pos
[GOAL]
case h
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < sum c.blocks
[PROOFSTEP]
convert h
[GOAL]
case h.e'_4
n : ℕ
c : Composition n
h : 0 < n
⊢ sum c.blocks = n
[PROOFSTEP]
exact c.blocks_sum
[GOAL]
n : ℕ
c : Composition n
⊢ sizeUpTo c 0 = 0
[PROOFSTEP]
simp [sizeUpTo]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ sizeUpTo c i = n
[PROOFSTEP]
dsimp [sizeUpTo]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ sum (take i c.blocks) = n
[PROOFSTEP]
convert c.blocks_sum
[GOAL]
case h.e'_2.h.e'_4
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ take i c.blocks = c.blocks
[PROOFSTEP]
exact take_all_of_le h
[GOAL]
n : ℕ
c : Composition n
i : ℕ
⊢ sizeUpTo c i ≤ n
[PROOFSTEP]
conv_rhs => rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
| n
[PROOFSTEP]
rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
⊢ sizeUpTo c i ≤ sum (take i c.blocks) + sum (drop i c.blocks)
[PROOFSTEP]
exact Nat.le_add_right _ _
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c (i + 1) = sizeUpTo c i + nthLe c.blocks i h
[PROOFSTEP]
simp only [sizeUpTo]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sum (take (i + 1) c.blocks) = sum (take i c.blocks) + nthLe c.blocks i h
[PROOFSTEP]
rw [sum_take_succ _ _ h]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c i < sizeUpTo c (i + 1)
[PROOFSTEP]
rw [c.sizeUpTo_succ h]
[GOAL]
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c i < sizeUpTo c i + nthLe c.blocks i h
[PROOFSTEP]
simp
[GOAL]
n : ℕ
c : Composition n
⊢ ↑(boundary c) 0 = 0
[PROOFSTEP]
simp [boundary, Fin.ext_iff]
[GOAL]
n : ℕ
c : Composition n
⊢ ↑(boundary c) (Fin.last (length c)) = Fin.last n
[PROOFSTEP]
simp [boundary, Fin.ext_iff]
[GOAL]
n : ℕ
c : Composition n
⊢ Finset.card (boundaries c) = length c + 1
[PROOFSTEP]
simp [boundaries]
[GOAL]
n : ℕ
c : Composition n
⊢ 0 ∈ boundaries c
[PROOFSTEP]
simp only [boundaries, Finset.mem_univ, exists_prop_of_true, Finset.mem_map]
[GOAL]
n : ℕ
c : Composition n
⊢ ∃ a, True ∧ ↑(boundary c).toEmbedding a = 0
[PROOFSTEP]
exact ⟨0, And.intro True.intro rfl⟩
[GOAL]
n : ℕ
c : Composition n
⊢ Fin.last n ∈ boundaries c
[PROOFSTEP]
simp only [boundaries, Finset.mem_univ, exists_prop_of_true, Finset.mem_map]
[GOAL]
n : ℕ
c : Composition n
⊢ ∃ a, True ∧ ↑(boundary c).toEmbedding a = Fin.last n
[PROOFSTEP]
exact ⟨Fin.last c.length, And.intro True.intro c.boundary_last⟩
[GOAL]
n : ℕ
c : Composition n
⊢ Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1) = boundary c
[PROOFSTEP]
refine' (Finset.orderEmbOfFin_unique' _ _).symm
[GOAL]
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (length c + 1)), ↑(boundary c) x ∈ boundaries c
[PROOFSTEP]
exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
[PROOFSTEP]
have n_pos : 0 < n := lt_of_le_of_lt (zero_le j) h
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
[PROOFSTEP]
have : 0 < c.blocks.sum := by rwa [← c.blocks_sum] at n_pos 
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
⊢ 0 < sum c.blocks
[PROOFSTEP]
rwa [← c.blocks_sum] at n_pos 
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
[PROOFSTEP]
have length_pos : 0 < c.blocks.length := length_pos_of_sum_pos (blocks c) this
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ ∃ i, j < sizeUpTo c (Nat.succ i) ∧ i < length c
[PROOFSTEP]
refine' ⟨c.length.pred, _, Nat.pred_lt (ne_of_gt length_pos)⟩
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
[PROOFSTEP]
have : c.length.pred.succ = c.length := Nat.succ_pred_eq_of_pos length_pos
[GOAL]
n : ℕ
c : Composition n
j : ℕ
h : j < n
n_pos : 0 < n
this✝ : 0 < sum c.blocks
length_pos : 0 < List.length c.blocks
this : Nat.succ (Nat.pred (length c)) = length c
⊢ j < sizeUpTo c (Nat.succ (Nat.pred (length c)))
[PROOFSTEP]
simp [this, h]
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ sizeUpTo c ↑(index c j) ≤ ↑j
[PROOFSTEP]
by_contra H
[GOAL]
n : ℕ
c : Composition n
j : Fin n
H : ¬sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
[PROOFSTEP]
set i := c.index j
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ¬sizeUpTo c ↑i ≤ ↑j
⊢ False
[PROOFSTEP]
push_neg at H 
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
⊢ False
[PROOFSTEP]
have i_pos : (0 : ℕ) < i := by
  by_contra' i_pos
  revert H
  simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
⊢ 0 < ↑i
[PROOFSTEP]
by_contra' i_pos
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : ↑(index c j) ≤ 0
⊢ False
[PROOFSTEP]
revert H
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
i_pos : ↑(index c j) ≤ 0
⊢ ↑j < sizeUpTo c ↑(index c j) → False
[PROOFSTEP]
simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
⊢ False
[PROOFSTEP]
let i₁ := (i : ℕ).pred
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
⊢ False
[PROOFSTEP]
have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
⊢ False
[PROOFSTEP]
have i₁_succ : i₁.succ = i := Nat.succ_pred_eq_of_pos i_pos
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
⊢ False
[PROOFSTEP]
have := Nat.find_min (c.index_exists j.2) i₁_lt_i
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : ¬(↑j < sizeUpTo c (Nat.succ i₁) ∧ i₁ < length c)
⊢ False
[PROOFSTEP]
simp [lt_trans i₁_lt_i (c.index j).2, i₁_succ] at this 
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c) := index c j
H : ↑j < sizeUpTo c ↑(index c j)
i_pos : 0 < ↑i
i₁ : ℕ := Nat.pred ↑i
i₁_lt_i : i₁ < ↑i
i₁_succ : Nat.succ i₁ = ↑i
this : sizeUpTo c ↑(index c j) ≤ ↑j
⊢ False
[PROOFSTEP]
exact Nat.lt_le_antisymm H this
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j - sizeUpTo c ↑(index c j) < blocksFun c (index c j)
[PROOFSTEP]
rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < sizeUpTo c (↑(index c j) + 1)
[PROOFSTEP]
exact lt_sizeUpTo_index_succ _ _
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ sizeUpTo c ↑(index c j) ≤ ↑j
[PROOFSTEP]
exact sizeUpTo_index_le _ _
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ ↑(embedding c (index c j)) (invEmbedding c j) = j
[PROOFSTEP]
rw [Fin.ext_iff]
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ ↑(↑(embedding c (index c j)) (invEmbedding c j)) = ↑j
[PROOFSTEP]
apply add_tsub_cancel_of_le (c.sizeUpTo_index_le j)
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) ↔ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
rcases Set.mem_range.2 h with ⟨k, hk⟩
[GOAL]
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : (fun y => ↑(embedding c i) y) k = j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
rw [Fin.ext_iff] at hk 
[GOAL]
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : ↑((fun y => ↑(embedding c i) y) k) = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
dsimp at hk 
[GOAL]
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
rw [← hk]
[GOAL]
case mp.intro
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : j ∈ Set.range ↑(embedding c i)
k : Fin (blocksFun c i)
hk : sizeUpTo c ↑i + ↑k = ↑j
⊢ sizeUpTo c ↑i ≤ sizeUpTo c ↑i + ↑k ∧ sizeUpTo c ↑i + ↑k < sizeUpTo c (Nat.succ ↑i)
[PROOFSTEP]
simp [sizeUpTo_succ', k.is_lt]
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i) → j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
apply Set.mem_range.2
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ∃ y, ↑(embedding c i) y = j
[PROOFSTEP]
refine' ⟨⟨j - c.sizeUpTo i, _⟩, _⟩
[GOAL]
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j - sizeUpTo c ↑i < blocksFun c i
[PROOFSTEP]
rw [tsub_lt_iff_left, ← sizeUpTo_succ']
[GOAL]
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑j < sizeUpTo c (↑i + 1)
[PROOFSTEP]
exact h.2
[GOAL]
case mpr.refine'_1
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ sizeUpTo c ↑i ≤ ↑j
[PROOFSTEP]
exact h.1
[GOAL]
case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := (_ : ↑j - sizeUpTo c ↑i < blocksFun c i) } = j
[PROOFSTEP]
rw [Fin.ext_iff]
[GOAL]
case mpr.refine'_2
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : sizeUpTo c ↑i ≤ ↑j ∧ ↑j < sizeUpTo c (Nat.succ ↑i)
⊢ ↑(↑(embedding c i) { val := ↑j - sizeUpTo c ↑i, isLt := (_ : ↑j - sizeUpTo c ↑i < blocksFun c i) }) = ↑j
[PROOFSTEP]
exact add_tsub_cancel_of_le h.1
[GOAL]
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
[PROOFSTEP]
classical
wlog h' : i₁ < i₂
exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm
by_contra d
obtain ⟨x, hx₁, hx₂⟩ : ∃ x : Fin n, x ∈ Set.range (c.embedding i₁) ∧ x ∈ Set.range (c.embedding i₂) :=
  Set.not_disjoint_iff.1 d
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
apply lt_irrefl (x : ℕ)
calc
  (x : ℕ) < c.sizeUpTo (i₁ : ℕ).succ := (c.mem_range_embedding_iff.1 hx₁).2
  _ ≤ c.sizeUpTo (i₂ : ℕ) := (monotone_sum_take _ A)
  _ ≤ x := (c.mem_range_embedding_iff.1 hx₂).1
[GOAL]
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
[PROOFSTEP]
wlog h' : i₁ < i₂
[GOAL]
case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin (length c)},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
[PROOFSTEP]
exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
[PROOFSTEP]
by_contra d
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
⊢ False
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ : ∃ x : Fin n, x ∈ Set.range (c.embedding i₁) ∧ x ∈ Set.range (c.embedding i₂) :=
  Set.not_disjoint_iff.1 d
[GOAL]
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
⊢ False
[PROOFSTEP]
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'
[GOAL]
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ False
[PROOFSTEP]
apply lt_irrefl (x : ℕ)
[GOAL]
case intro.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin (length c)
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ↑(embedding c i₁)) (Set.range ↑(embedding c i₂))
x : Fin n
hx₁ : x ∈ Set.range ↑(embedding c i₁)
hx₂ : x ∈ Set.range ↑(embedding c i₂)
A : Nat.succ ↑i₁ ≤ ↑i₂
⊢ ↑x < ↑x
[PROOFSTEP]
calc
  (x : ℕ) < c.sizeUpTo (i₁ : ℕ).succ := (c.mem_range_embedding_iff.1 hx₁).2
  _ ≤ c.sizeUpTo (i₂ : ℕ) := (monotone_sum_take _ A)
  _ ≤ x := (c.mem_range_embedding_iff.1 hx₂).1
[GOAL]
n : ℕ
c : Composition n
j : Fin n
⊢ j ∈ Set.range ↑(embedding c (index c j))
[PROOFSTEP]
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
  Set.mem_range_self
    _
      -- porting note: previously `rwa` closed
[GOAL]
n : ℕ
c : Composition n
j : Fin n
this : ↑(embedding c (index c j)) (invEmbedding c j) ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
[PROOFSTEP]
rw [c.embedding_comp_inv j] at this 
[GOAL]
n : ℕ
c : Composition n
j : Fin n
this : j ∈ Set.range ↑(embedding c (index c j))
⊢ j ∈ Set.range ↑(embedding c (index c j))
[PROOFSTEP]
assumption
[GOAL]
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) ↔ i = index c j
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ j ∈ Set.range ↑(embedding c i) → i = index c j
[PROOFSTEP]
rw [← not_imp_not]
[GOAL]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ ¬i = index c j → ¬j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : ¬i = index c j
⊢ ¬j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
⊢ i = index c j → j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin (length c)
h : i = index c j
⊢ j ∈ Set.range ↑(embedding c (index c j))
[PROOFSTEP]
exact c.mem_range_embedding j
[GOAL]
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ index c (↑(embedding c i) j) = i
[PROOFSTEP]
symm
[GOAL]
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ i = index c (↑(embedding c i) j)
[PROOFSTEP]
rw [← mem_range_embedding_iff']
[GOAL]
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ ↑(embedding c i) j ∈ Set.range ↑(embedding c i)
[PROOFSTEP]
apply Set.mem_range_self
[GOAL]
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ ↑(invEmbedding c (↑(embedding c i) j)) = ↑j
[PROOFSTEP]
simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]
[GOAL]
n : ℕ
c : Composition n
x : (i : Fin (length c)) × Fin (blocksFun c i)
⊢ (fun j => { fst := index c j, snd := invEmbedding c j }) ((fun x => ↑(embedding c x.fst) x.snd) x) = x
[PROOFSTEP]
rcases x with ⟨i, y⟩
[GOAL]
case mk
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ (fun j => { fst := index c j, snd := invEmbedding c j })
      ((fun x => ↑(embedding c x.fst) x.snd) { fst := i, snd := y }) =
    { fst := i, snd := y }
[PROOFSTEP]
dsimp
[GOAL]
case mk
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ { fst := index c (↑(embedding c i) y), snd := invEmbedding c (↑(embedding c i) y) } = { fst := i, snd := y }
[PROOFSTEP]
congr
[GOAL]
case mk.h.e_3.h
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ index c (↑(embedding c i) y) = i
[PROOFSTEP]
exact c.index_embedding _ _
[GOAL]
case mk.h.e_4
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ HEq (invEmbedding c (↑(embedding c i) y)) y
[PROOFSTEP]
rw [Fin.heq_ext_iff]
[GOAL]
case mk.h.e_4
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ ↑(invEmbedding c (↑(embedding c i) y)) = ↑y
[PROOFSTEP]
exact c.invEmbedding_comp _ _
[GOAL]
case mk.h.e_4.h
n : ℕ
c : Composition n
i : Fin (length c)
y : Fin (blocksFun c i)
⊢ blocksFun c (index c (↑(embedding c i) y)) = blocksFun c i
[PROOFSTEP]
rw [c.index_embedding]
[GOAL]
n : ℕ
c : Composition n
n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin (length c₁)
i₂ : Fin (length c₂)
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
[PROOFSTEP]
cases hn
[GOAL]
case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
[PROOFSTEP]
rw [← Composition.ext_iff] at hc 
[GOAL]
case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
[PROOFSTEP]
cases hc
[GOAL]
case refl.refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₁ i₂
[PROOFSTEP]
congr
[GOAL]
case refl.refl.e_a
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂
[PROOFSTEP]
rwa [Fin.ext_iff]
[GOAL]
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
⊢ c = c' ↔ c.snd.blocks = c'.snd.blocks
[PROOFSTEP]
refine' ⟨fun H => by rw [H], fun H => _⟩
[GOAL]
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd.blocks = c'.snd.blocks
[PROOFSTEP]
rw [H]
[GOAL]
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'
[PROOFSTEP]
rcases c with ⟨n, c⟩
[GOAL]
case mk
n✝ : ℕ
c✝ : Composition n✝
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : { fst := n, snd := c }.snd.blocks = c'.snd.blocks
⊢ { fst := n, snd := c } = c'
[PROOFSTEP]
rcases c' with ⟨n', c'⟩
[GOAL]
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
[PROOFSTEP]
have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
⊢ n = n'
[PROOFSTEP]
rw [← c.blocks_sum, ← c'.blocks_sum, H]
[GOAL]
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
this : n = n'
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
[PROOFSTEP]
induction this
[GOAL]
case mk.mk.refl
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n, snd := c' }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.refl.e_snd
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c = c'
[PROOFSTEP]
ext1
[GOAL]
case mk.mk.refl.e_snd.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c.blocks = c'.blocks
[PROOFSTEP]
exact H
[GOAL]
n✝ : ℕ
c : Composition n✝
n i : ℕ
hi : i ∈ replicate n 1
⊢ 0 < i
[PROOFSTEP]
simp [List.eq_of_mem_replicate hi]
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
⊢ sum (replicate n 1) = n
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
i : Fin (length (ones n))
⊢ blocksFun (ones n) i = 1
[PROOFSTEP]
simp only [blocksFun, ones, blocks, i.2, List.nthLe_replicate]
[GOAL]
n✝ : ℕ
c : Composition n✝
n i : ℕ
⊢ sizeUpTo (ones n) i = min i n
[PROOFSTEP]
simp [sizeUpTo, ones_blocks, take_replicate]
[GOAL]
n : ℕ
c : Composition n
i : Fin (length (ones n))
h : 0 < blocksFun (ones n) i
⊢ ↑(embedding (ones n) i) { val := 0, isLt := h } = { val := ↑i, isLt := (_ : ↑i < n) }
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
c : Composition n
i : Fin (length (ones n))
h : 0 < blocksFun (ones n) i
⊢ ↑(↑(embedding (ones n) i) { val := 0, isLt := h }) = ↑{ val := ↑i, isLt := (_ : ↑i < n) }
[PROOFSTEP]
simpa using i.2.le
[GOAL]
n : ℕ
c✝ c : Composition n
⊢ c = ones n ↔ ∀ (i : ℕ), i ∈ c.blocks → i = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → ∀ (i : ℕ), i ∈ c.blocks → i = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
n : ℕ
c : Composition n
⊢ ∀ (i : ℕ), i ∈ (ones n).blocks → i = 1
[PROOFSTEP]
exact fun i => eq_of_mem_replicate
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
⊢ (∀ (i : ℕ), i ∈ c.blocks → i = 1) → c = ones n
[PROOFSTEP]
intro H
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c = ones n
[PROOFSTEP]
ext1
[GOAL]
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c.blocks = (ones n).blocks
[PROOFSTEP]
have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
[GOAL]
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ c.blocks = (ones n).blocks
[PROOFSTEP]
have : c.blocks.length = n := by
  conv_rhs => rw [← c.blocks_sum, A]
  simp
[GOAL]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ List.length c.blocks = n
[PROOFSTEP]
conv_rhs => rw [← c.blocks_sum, A]
[GOAL]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
| n
[PROOFSTEP]
rw [← c.blocks_sum, A]
[GOAL]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
| n
[PROOFSTEP]
rw [← c.blocks_sum, A]
[GOAL]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
| n
[PROOFSTEP]
rw [← c.blocks_sum, A]
[GOAL]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ List.length c.blocks = sum (replicate (List.length c.blocks) 1)
[PROOFSTEP]
simp
[GOAL]
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
this : List.length c.blocks = n
⊢ c.blocks = (ones n).blocks
[PROOFSTEP]
rw [A, this, ones_blocks]
[GOAL]
n : ℕ
c✝ c : Composition n
⊢ c ≠ ones n ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
[PROOFSTEP]
refine' (not_congr eq_ones_iff).trans _
[GOAL]
n : ℕ
c✝ c : Composition n
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
[PROOFSTEP]
have : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1 := fun j hj => by simp [le_antisymm_iff, c.one_le_blocks hj]
[GOAL]
n : ℕ
c✝ c : Composition n
j : ℕ
hj : j ∈ c.blocks
⊢ j = 1 ↔ j ≤ 1
[PROOFSTEP]
simp [le_antisymm_iff, c.one_le_blocks hj]
[GOAL]
n : ℕ
c✝ c : Composition n
this : ∀ (j : ℕ), j ∈ c.blocks → (j = 1 ↔ j ≤ 1)
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
[PROOFSTEP]
simp (config := { contextual := true }) [this]
[GOAL]
n : ℕ
c✝ c : Composition n
⊢ c = ones n ↔ length c = n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → length c = n
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
n : ℕ
c : Composition n
⊢ length (ones n) = n
[PROOFSTEP]
exact ones_length n
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
⊢ length c = n → c = ones n
[PROOFSTEP]
contrapose
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
⊢ ¬c = ones n → ¬length c = n
[PROOFSTEP]
intro H length_n
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ False
[PROOFSTEP]
apply lt_irrefl n
[GOAL]
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ n < n
[PROOFSTEP]
calc
  n = ∑ i : Fin c.length, 1 := by simp [length_n]
  _ < ∑ i : Fin c.length, c.blocksFun i := by
    {
    obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
    rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi 
    obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
    rw [← hj] at i_blocks 
    exact Finset.sum_lt_sum (fun i _ => by simp [blocksFun]) ⟨j, Finset.mem_univ _, i_blocks⟩
  }
  _ = n := c.sum_blocksFun
[GOAL]
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ n = ∑ i : Fin (length c), 1
[PROOFSTEP]
simp [length_n]
[GOAL]
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
{ obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
  rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi 
  obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
  rw [← hj] at i_blocks 
  exact Finset.sum_lt_sum (fun i _ => by simp [blocksFun]) ⟨j, Finset.mem_univ _, i_blocks⟩
}
[GOAL]
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
[GOAL]
case intro.intro
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi 
[GOAL]
case intro.intro
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i : ℕ
hi : ∃ y, blocksFun c y = i
i_blocks : 1 < i
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
[GOAL]
case intro.intro.intro
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i : ℕ
i_blocks : 1 < i
j : Fin (length c)
hj : blocksFun c j = i
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
rw [← hj] at i_blocks 
[GOAL]
case intro.intro.intro
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i : ℕ
j : Fin (length c)
i_blocks : 1 < blocksFun c j
hj : blocksFun c j = i
⊢ ∑ i : Fin (length c), 1 < ∑ i : Fin (length c), blocksFun c i
[PROOFSTEP]
exact Finset.sum_lt_sum (fun i _ => by simp [blocksFun]) ⟨j, Finset.mem_univ _, i_blocks⟩
[GOAL]
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i✝ : ℕ
j : Fin (length c)
i_blocks : 1 < blocksFun c j
hj : blocksFun c j = i✝
i : Fin (length c)
x✝ : i ∈ Finset.univ
⊢ 1 ≤ blocksFun c i
[PROOFSTEP]
simp [blocksFun]
[GOAL]
n : ℕ
c✝ c : Composition n
⊢ c = ones n ↔ n ≤ length c
[PROOFSTEP]
simp [eq_ones_iff_length, le_antisymm_iff, c.length_le]
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ ∀ {i : ℕ}, i ∈ [n] → 0 < i
[PROOFSTEP]
simp [h]
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ sum [n] = n
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin (length (single n h))
⊢ blocksFun (single n h) i = n
[PROOFSTEP]
simp [blocksFun, single, blocks, i.2]
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(embedding (single n h) 0) i = i
[PROOFSTEP]
ext
[GOAL]
case h
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(↑(embedding (single n h) 0) i) = ↑i
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h ↔ length c = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h → length c = 1
[PROOFSTEP]
intro H
[GOAL]
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ length c = 1
[PROOFSTEP]
rw [H]
[GOAL]
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ length (single n h) = 1
[PROOFSTEP]
exact single_length h
[GOAL]
case mpr
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
⊢ length c = 1 → c = single n h
[PROOFSTEP]
intro H
[GOAL]
case mpr
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : length c = 1
⊢ c = single n h
[PROOFSTEP]
ext1
[GOAL]
case mpr.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : length c = 1
⊢ c.blocks = (single n h).blocks
[PROOFSTEP]
have A : c.blocks.length = 1 := H ▸ c.blocks_length
[GOAL]
case mpr.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : length c = 1
A : List.length c.blocks = 1
⊢ c.blocks = (single n h).blocks
[PROOFSTEP]
have B : c.blocks.sum = n := c.blocks_sum
[GOAL]
case mpr.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : length c = 1
A : List.length c.blocks = 1
B : sum c.blocks = n
⊢ c.blocks = (single n h).blocks
[PROOFSTEP]
rw [eq_cons_of_length_one A] at B ⊢
[GOAL]
case mpr.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
h : 0 < n
c : Composition n
H : length c = 1
A : List.length c.blocks = 1
B : sum [nthLe c.blocks 0 (_ : 0 < List.length c.blocks)] = n
⊢ [nthLe c.blocks 0 (_ : 0 < List.length c.blocks)] = (single n h).blocks
[PROOFSTEP]
simpa [single_blocks] using B
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin (length c)), blocksFun c i < n
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ ¬c ≠ single n hn ↔ ¬∀ (i : Fin (length c)), blocksFun c i < n
[PROOFSTEP]
push_neg
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ blocksFun c i
[PROOFSTEP]
constructor
[GOAL]
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ blocksFun c i
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ blocksFun (single n hn) i
[PROOFSTEP]
exact ⟨⟨0, by simp⟩, by simp⟩
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ 0 < length (single n hn)
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ n ≤ blocksFun (single n hn) { val := 0, isLt := (_ : 0 < 1) }
[PROOFSTEP]
simp
[GOAL]
case mpr
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ blocksFun c i) → c = single n hn
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ c = single n hn
[PROOFSTEP]
rw [eq_single_iff_length]
[GOAL]
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ length c = 1
[PROOFSTEP]
have : ∀ j : Fin c.length, j = i := by
  intro j
  by_contra ji
  apply lt_irrefl (∑ k, c.blocksFun k)
  calc
    ∑ k, c.blocksFun k ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
    _ < ∑ k, c.blocksFun k :=
      Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j) fun _ _ _ => zero_le _
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ ∀ (j : Fin (length c)), j = i
[PROOFSTEP]
intro j
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
⊢ j = i
[PROOFSTEP]
by_contra ji
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ False
[PROOFSTEP]
apply lt_irrefl (∑ k, c.blocksFun k)
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ ∑ k : Fin (length c), blocksFun c k < ∑ k : Fin (length c), blocksFun c k
[PROOFSTEP]
calc
  ∑ k, c.blocksFun k ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
  _ < ∑ k, c.blocksFun k :=
    Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j) fun _ _ _ => zero_le _
[GOAL]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ ∑ k : Fin (length c), blocksFun c k ≤ blocksFun c i
[PROOFSTEP]
simp only [c.sum_blocksFun, hi]
[GOAL]
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
this : ∀ (j : Fin (length c)), j = i
⊢ length c = 1
[PROOFSTEP]
simpa using Fintype.card_eq_one_of_forall_eq this
[GOAL]
n✝ : ℕ
α : Type u_1
l : List α
n : ℕ
ns : List ℕ
⊢ splitWrtCompositionAux l (n :: ns) = take n l :: splitWrtCompositionAux (drop n l) ns
[PROOFSTEP]
simp [splitWrtCompositionAux]
[GOAL]
n : ℕ
α : Type u_1
l : List α
ns : List ℕ
⊢ length (splitWrtCompositionAux l ns) = length ns
[PROOFSTEP]
induction ns generalizing l
[GOAL]
case nil
n : ℕ
α : Type u_1
l : List α
⊢ length (splitWrtCompositionAux l []) = length []
[PROOFSTEP]
simp [splitWrtCompositionAux, *]
[GOAL]
case cons
n : ℕ
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), length (splitWrtCompositionAux l tail✝) = length tail✝
l : List α
⊢ length (splitWrtCompositionAux l (head✝ :: tail✝)) = length (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
n : ℕ
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
[PROOFSTEP]
induction' ns with n ns IH
[GOAL]
case nil
n : ℕ
α : Type u_1
⊢ ∀ {l : List α}, sum [] ≤ length l → map length (splitWrtCompositionAux l []) = []
[PROOFSTEP]
intro l h
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
⊢ ∀ {l : List α}, sum (n :: ns) ≤ length l → map length (splitWrtCompositionAux l (n :: ns)) = n :: ns
[PROOFSTEP]
intro l h
[GOAL]
case nil
n : ℕ
α : Type u_1
l : List α
h : sum [] ≤ length l
⊢ map length (splitWrtCompositionAux l []) = []
[PROOFSTEP]
simp at h 
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : sum (n :: ns) ≤ length l
⊢ map length (splitWrtCompositionAux l (n :: ns)) = n :: ns
[PROOFSTEP]
simp at h 
[GOAL]
case nil
n : ℕ
α : Type u_1
l : List α
h : True
⊢ map length (splitWrtCompositionAux l []) = []
[PROOFSTEP]
simp
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
⊢ map length (splitWrtCompositionAux l (n :: ns)) = n :: ns
[PROOFSTEP]
have := le_trans (Nat.le_add_right _ _) h
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ map length (splitWrtCompositionAux l (n :: ns)) = n :: ns
[PROOFSTEP]
simp only [splitWrtCompositionAux_cons, this]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ map length (take n l :: splitWrtCompositionAux (drop n l) ns) = n :: ns
[PROOFSTEP]
dsimp
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ length (take n l) :: map length (splitWrtCompositionAux (drop n l) ns) = n :: ns
[PROOFSTEP]
rw [length_take, IH]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ min n (length l) :: ns = n :: ns
[PROOFSTEP]
simp [length_drop]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ sum ns ≤ length (drop n l)
[PROOFSTEP]
simp [length_drop]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ n ≤ length l
[PROOFSTEP]
assumption
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
this : n ≤ length l
⊢ sum ns ≤ length l - n
[PROOFSTEP]
exact le_tsub_of_add_le_left h
[GOAL]
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
⊢ 0 < length l'
[PROOFSTEP]
have : l'.length ∈ (l.splitWrtComposition c).map List.length := List.mem_map_of_mem List.length h
[GOAL]
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
this : length l' ∈ map length (splitWrtComposition l c)
⊢ 0 < length l'
[PROOFSTEP]
rw [map_length_splitWrtComposition] at this 
[GOAL]
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
this : length l' ∈ c.blocks
⊢ 0 < length l'
[PROOFSTEP]
exact c.blocks_pos this
[GOAL]
n : ℕ
α : Type u_1
l : List α
c : Composition (length l)
i : ℕ
⊢ sum (take i (map length (splitWrtComposition l c))) = Composition.sizeUpTo c i
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
n : ℕ
α : Type u_1
l : List α
c : Composition (length l)
i : ℕ
⊢ map length (splitWrtComposition l c) = c.blocks
[PROOFSTEP]
exact map_length_splitWrtComposition l c
[GOAL]
n : ℕ
α : Type u_1
l : List α
ns : List ℕ
i : ℕ
hi : i < length (splitWrtCompositionAux l ns)
⊢ nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
[PROOFSTEP]
induction' ns with n ns IH generalizing l i
[GOAL]
case nil
n : ℕ
α : Type u_1
l✝ : List α
ns : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns)
l : List α
i : ℕ
hi : i < length (splitWrtCompositionAux l [])
⊢ nthLe (splitWrtCompositionAux l []) i hi = drop (sum (take i [])) (take (sum (take (i + 1) [])) l)
[PROOFSTEP]
cases hi
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : i < length (splitWrtCompositionAux l (n :: ns))
⊢ nthLe (splitWrtCompositionAux l (n :: ns)) i hi =
    drop (sum (take i (n :: ns))) (take (sum (take (i + 1) (n :: ns))) l)
[PROOFSTEP]
cases' i with i
[GOAL]
case cons.zero
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i : ℕ
hi✝ : i < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
hi : Nat.zero < length (splitWrtCompositionAux l (n :: ns))
⊢ nthLe (splitWrtCompositionAux l (n :: ns)) Nat.zero hi =
    drop (sum (take Nat.zero (n :: ns))) (take (sum (take (Nat.zero + 1) (n :: ns))) l)
[PROOFSTEP]
rw [Nat.add_zero, List.take_zero, sum_nil, nthLe_zero]
[GOAL]
case cons.zero
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i : ℕ
hi✝ : i < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
hi : Nat.zero < length (splitWrtCompositionAux l (n :: ns))
⊢ head! (splitWrtCompositionAux l (n :: ns)) = drop 0 (take (sum (take 1 (n :: ns))) l)
[PROOFSTEP]
dsimp
[GOAL]
case cons.zero
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i : ℕ
hi✝ : i < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
hi : Nat.zero < length (splitWrtCompositionAux l (n :: ns))
⊢ head! (splitWrtCompositionAux l (n :: ns)) = take (sum [n]) l
[PROOFSTEP]
simp only [splitWrtCompositionAux_cons, head!, sum, foldl, zero_add]
[GOAL]
case cons.succ
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : Nat.succ i < length (splitWrtCompositionAux l (n :: ns))
⊢ nthLe (splitWrtCompositionAux l (n :: ns)) (Nat.succ i) hi =
    drop (sum (take (Nat.succ i) (n :: ns))) (take (sum (take (Nat.succ i + 1) (n :: ns))) l)
[PROOFSTEP]
simp only [splitWrtCompositionAux_cons, take, sum_cons, Nat.add_eq, add_zero, gt_iff_lt, nthLe_cons, IH]
[GOAL]
case cons.succ
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : Nat.succ i < length (splitWrtCompositionAux l (n :: ns))
⊢ (if h : False then take n l
    else drop (sum (take (Nat.succ i - 1) ns)) (take (sum (take (Nat.succ i - 1 + 1) ns)) (drop n l))) =
    drop (n + sum (take i ns)) (take (n + sum (take (Nat.succ i) ns)) l)
[PROOFSTEP]
dsimp
[GOAL]
case cons.succ
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : Nat.succ i < length (splitWrtCompositionAux l (n :: ns))
⊢ drop (sum (take (Nat.succ i - 1) ns)) (take (sum (take (Nat.succ i - 1 + 1) ns)) (drop n l)) =
    drop (n + sum (take i ns)) (take (n + sum (take (Nat.succ i) ns)) l)
[PROOFSTEP]
rw [Nat.succ_sub_succ_eq_sub, ← Nat.succ_eq_add_one, tsub_zero]
[GOAL]
case cons.succ
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : Nat.succ i < length (splitWrtCompositionAux l (n :: ns))
⊢ drop (sum (take i ns)) (take (sum (take (Nat.succ i) ns)) (drop n l)) =
    drop (n + sum (take i ns)) (take (n + sum (take (Nat.succ i) ns)) l)
[PROOFSTEP]
simp only [← drop_take, drop_drop]
[GOAL]
case cons.succ
n✝ : ℕ
α : Type u_1
l✝ : List α
ns✝ : List ℕ
i✝ : ℕ
hi✝ : i✝ < length (splitWrtCompositionAux l✝ ns✝)
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < length (splitWrtCompositionAux l ns)),
    nthLe (splitWrtCompositionAux l ns) i hi = drop (sum (take i ns)) (take (sum (take (i + 1) ns)) l)
l : List α
i : ℕ
hi : Nat.succ i < length (splitWrtCompositionAux l (n :: ns))
⊢ drop (sum (take i ns) + n) (take (n + sum (take (Nat.succ i) ns)) l) =
    drop (n + sum (take i ns)) (take (n + sum (take (Nat.succ i) ns)) l)
[PROOFSTEP]
rw [add_comm]
[GOAL]
n : ℕ
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
[PROOFSTEP]
induction' ns with n ns IH
[GOAL]
case nil
n : ℕ
α : Type u_1
⊢ ∀ {l : List α}, sum [] = length l → join (splitWrtCompositionAux l []) = l
[PROOFSTEP]
intro l h
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
⊢ ∀ {l : List α}, sum (n :: ns) = length l → join (splitWrtCompositionAux l (n :: ns)) = l
[PROOFSTEP]
intro l h
[GOAL]
case nil
n : ℕ
α : Type u_1
l : List α
h : sum [] = length l
⊢ join (splitWrtCompositionAux l []) = l
[PROOFSTEP]
simp at h 
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : sum (n :: ns) = length l
⊢ join (splitWrtCompositionAux l (n :: ns)) = l
[PROOFSTEP]
simp at h 
[GOAL]
case nil
n : ℕ
α : Type u_1
l : List α
h : 0 = length l
⊢ join (splitWrtCompositionAux l []) = l
[PROOFSTEP]
exact (length_eq_zero.1 h.symm).symm
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : n + sum ns = length l
⊢ join (splitWrtCompositionAux l (n :: ns)) = l
[PROOFSTEP]
simp only [splitWrtCompositionAux_cons]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : n + sum ns = length l
⊢ join (take n l :: splitWrtCompositionAux (drop n l) ns) = l
[PROOFSTEP]
dsimp
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : n + sum ns = length l
⊢ take n l ++ join (splitWrtCompositionAux (drop n l) ns) = l
[PROOFSTEP]
rw [IH]
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : n + sum ns = length l
⊢ take n l ++ drop n l = l
[PROOFSTEP]
simp
[GOAL]
case cons
n✝ : ℕ
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
l : List α
h : n + sum ns = length l
⊢ sum ns = length (drop n l)
[PROOFSTEP]
rw [length_drop, ← h, add_tsub_cancel_left]
[GOAL]
n : ℕ
α : Type u_1
L : List (List α)
c : Composition (length (join L))
h : map length L = c.blocks
⊢ splitWrtComposition (join L) c = L
[PROOFSTEP]
simp only [eq_self_iff_true, and_self_iff, eq_iff_join_eq, join_splitWrtComposition, map_length_splitWrtComposition, h]
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (n - 1)
⊢ 1 + ↑i < Nat.succ n
[PROOFSTEP]
apply (add_lt_add_left i.is_lt 1).trans_le
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (n - 1)
⊢ 1 + (n - 1) ≤ Nat.succ n
[PROOFSTEP]
rw [Nat.succ_eq_add_one, add_comm]
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (n - 1)
⊢ n - 1 + 1 ≤ n + 1
[PROOFSTEP]
exact add_le_add (Nat.sub_le n 1) (le_refl 1)
[GOAL]
n✝ n : ℕ
s : Finset (Fin (n - 1))
⊢ 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
s : Finset (Fin (n - 1))
⊢ Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
⊢ Function.LeftInverse
    (fun s =>
      { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
        zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
        getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
    fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries}
[PROOFSTEP]
intro c
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun s =>
        { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
          zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
          getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
      ((fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries}) c) =
    c
[PROOFSTEP]
ext i
[GOAL]
case boundaries.a
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
⊢ i ∈
      ((fun s =>
            { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
              zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
              getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
          ((fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries})
            c)).boundaries ↔
    i ∈ c.boundaries
[PROOFSTEP]
simp only [add_comm, Set.toFinset_setOf, Finset.mem_univ, forall_true_left, Finset.mem_filter, true_and, exists_prop]
[GOAL]
case boundaries.a
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1) ↔
    i ∈ c.boundaries
[PROOFSTEP]
constructor
[GOAL]
case boundaries.a.mp
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1) →
    i ∈ c.boundaries
[PROOFSTEP]
rintro (rfl | rfl | ⟨j, hj1, hj2⟩)
[GOAL]
case boundaries.a.mp.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries
[PROOFSTEP]
exact c.zero_mem
[GOAL]
case boundaries.a.mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries
[PROOFSTEP]
exact c.getLast_mem
[GOAL]
case boundaries.a.mp.inr.inr.intro.intro
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
j : Fin (n - 1)
hj1 : { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries
[PROOFSTEP]
convert hj1
[GOAL]
case boundaries.a.mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
⊢ i ∈ c.boundaries →
    i = 0 ∨ i = Fin.last n ∨ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1
[PROOFSTEP]
simp only [or_iff_not_imp_left]
[GOAL]
case boundaries.a.mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
⊢ i ∈ c.boundaries →
    ¬i = 0 → ¬i = Fin.last n → ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1
[PROOFSTEP]
intro i_mem i_ne_zero i_ne_last
[GOAL]
case boundaries.a.mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬i = 0
i_ne_last : ¬i = Fin.last n
⊢ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1
[PROOFSTEP]
simp [Fin.ext_iff] at i_ne_zero i_ne_last 
[GOAL]
case boundaries.a.mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
⊢ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1
[PROOFSTEP]
have A : (1 + (i - 1) : ℕ) = (i : ℕ) := by
  rw [add_comm]
  exact Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr i_ne_zero)
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
⊢ 1 + (↑i - 1) = ↑i
[PROOFSTEP]
rw [add_comm]
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
⊢ ↑i - 1 + 1 = ↑i
[PROOFSTEP]
exact Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr i_ne_zero)
[GOAL]
case boundaries.a.mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ∃ j, { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ n) } ∈ c.boundaries ∧ ↑i = ↑j + 1
[PROOFSTEP]
refine' ⟨⟨i - 1, _⟩, _, _⟩
[GOAL]
case boundaries.a.mpr.refine'_1
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑i - 1 < n - 1
[PROOFSTEP]
have : (i : ℕ) < n + 1 := i.2
[GOAL]
case boundaries.a.mpr.refine'_1
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
this : ↑i < n + 1
⊢ ↑i - 1 < n - 1
[PROOFSTEP]
simp [Nat.lt_succ_iff_lt_or_eq, i_ne_last] at this 
[GOAL]
case boundaries.a.mpr.refine'_1
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
this : ↑i < n
⊢ ↑i - 1 < n - 1
[PROOFSTEP]
exact Nat.pred_lt_pred i_ne_zero this
[GOAL]
case boundaries.a.mpr.refine'_2
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ { val := ↑{ val := ↑i - 1, isLt := (_ : Nat.pred (Nat.sub (↑i) 0) < Nat.pred (Nat.sub n 0)) } + 1,
      isLt :=
        (_ : ↑{ val := ↑i - 1, isLt := (_ : Nat.pred (Nat.sub (↑i) 0) < Nat.pred (Nat.sub n 0)) } + 1 < Nat.succ n) } ∈
    c.boundaries
[PROOFSTEP]
convert i_mem
[GOAL]
case h.e'_4.h.e'_2
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑{ val := ↑i - 1, isLt := (_ : Nat.pred (Nat.sub (↑i) 0) < Nat.pred (Nat.sub n 0)) } + 1 = ↑i
[PROOFSTEP]
simp only [ge_iff_le]
[GOAL]
case h.e'_4.h.e'_2
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑i - 1 + 1 = ↑i
[PROOFSTEP]
rwa [add_comm]
[GOAL]
case boundaries.a.mpr.refine'_3
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑i = ↑{ val := ↑i - 1, isLt := (_ : Nat.pred (Nat.sub (↑i) 0) < Nat.pred (Nat.sub n 0)) } + 1
[PROOFSTEP]
simp only [ge_iff_le]
[GOAL]
case boundaries.a.mpr.refine'_3
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑i = ↑i - 1 + 1
[PROOFSTEP]
symm
[GOAL]
case boundaries.a.mpr.refine'_3
n✝ n : ℕ
c : CompositionAsSet n
i : Fin (Nat.succ n)
i_mem : i ∈ c.boundaries
i_ne_zero : ¬↑i = 0
i_ne_last : ¬↑i = n
A : 1 + (↑i - 1) = ↑i
⊢ ↑i - 1 + 1 = ↑i
[PROOFSTEP]
rwa [add_comm]
[GOAL]
n✝ n : ℕ
⊢ Function.RightInverse
    (fun s =>
      { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
        zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
        getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
    fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries}
[PROOFSTEP]
intro s
[GOAL]
n✝ n : ℕ
s : Finset (Fin (n - 1))
⊢ (fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries})
      ((fun s =>
          { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
            zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
            getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
        s) =
    s
[PROOFSTEP]
ext i
[GOAL]
case a
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ i ∈
      (fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries})
        ((fun s =>
            { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
              zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
              getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
          s) ↔
    i ∈ s
[PROOFSTEP]
have : 1 + (i : ℕ) ≠ n := by
  apply ne_of_lt
  convert add_lt_add_left i.is_lt 1
  rw [add_comm]
  apply (Nat.succ_pred_eq_of_pos _).symm
  exact (zero_le i.val).trans_lt (i.2.trans_le (Nat.sub_le n 1))
[GOAL]
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ 1 + ↑i ≠ n
[PROOFSTEP]
apply ne_of_lt
[GOAL]
case h
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ 1 + ↑i < n
[PROOFSTEP]
convert add_lt_add_left i.is_lt 1
[GOAL]
case h.e'_4
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ n = 1 + (n - 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case h.e'_4
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ n = n - 1 + 1
[PROOFSTEP]
apply (Nat.succ_pred_eq_of_pos _).symm
[GOAL]
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ 0 < n
[PROOFSTEP]
exact (zero_le i.val).trans_lt (i.2.trans_le (Nat.sub_le n 1))
[GOAL]
case a
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ i ∈
      (fun c => Set.toFinset {i | { val := 1 + ↑i, isLt := (_ : 1 + ↑i < Nat.succ n) } ∈ c.boundaries})
        ((fun s =>
            { boundaries := Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1},
              zero_mem := (_ : 0 ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}),
              getLast_mem := (_ : Fin.last n ∈ Set.toFinset {i | i = 0 ∨ i = Fin.last n ∨ ∃ j _hj, ↑i = ↑j + 1}) })
          s) ↔
    i ∈ s
[PROOFSTEP]
simp only [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf, Finset.mem_univ,
  forall_true_left, Finset.mem_filter, add_eq_zero_iff, and_false, add_left_inj, false_or, true_and]
[GOAL]
case a
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ (↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j) ↔ i ∈ s
[PROOFSTEP]
erw [Set.mem_setOf_eq]
[GOAL]
case a
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ (↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j) ↔ i ∈ s.val
[PROOFSTEP]
simp [this, false_or_iff, add_right_inj, add_eq_zero_iff, one_ne_zero, false_and_iff, Fin.val_mk]
[GOAL]
case a
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ (↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j) ↔ i ∈ s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ (↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j) → i ∈ s
[PROOFSTEP]
intro h
[GOAL]
case a.mp
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
h : ↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j
⊢ i ∈ s
[PROOFSTEP]
cases' h with n h
[GOAL]
case a.mp.inl
n✝¹ n✝ : ℕ
s : Finset (Fin (n✝ - 1))
i : Fin (n✝ - 1)
this : 1 + ↑i ≠ n✝
n : ↑i + 1 = n✝
⊢ i ∈ s
[PROOFSTEP]
rw [add_comm] at this 
[GOAL]
case a.mp.inl
n✝¹ n✝ : ℕ
s : Finset (Fin (n✝ - 1))
i : Fin (n✝ - 1)
this : ↑i + 1 ≠ n✝
n : ↑i + 1 = n✝
⊢ i ∈ s
[PROOFSTEP]
contradiction
[GOAL]
case a.mp.inr
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
h : ∃ j, j ∈ s ∧ ↑i = ↑j
⊢ i ∈ s
[PROOFSTEP]
cases' h with w h
[GOAL]
case a.mp.inr.intro
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
w : Fin (n - 1)
h : w ∈ s ∧ ↑i = ↑w
⊢ i ∈ s
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case a.mp.inr.intro.intro
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
w : Fin (n - 1)
h₁ : w ∈ s
h₂ : ↑i = ↑w
⊢ i ∈ s
[PROOFSTEP]
rw [← Fin.ext_iff] at h₂ 
[GOAL]
case a.mp.inr.intro.intro
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
w : Fin (n - 1)
h₁ : w ∈ s
h₂ : i = w
⊢ i ∈ s
[PROOFSTEP]
rwa [h₂]
[GOAL]
case a.mpr
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
⊢ i ∈ s → ↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j
[PROOFSTEP]
intro h
[GOAL]
case a.mpr
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
h : i ∈ s
⊢ ↑i + 1 = n ∨ ∃ j, j ∈ s ∧ ↑i = ↑j
[PROOFSTEP]
apply Or.inr
[GOAL]
case a.mpr.h
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : 1 + ↑i ≠ n
h : i ∈ s
⊢ ∃ j, j ∈ s ∧ ↑i = ↑j
[PROOFSTEP]
use i, h
[GOAL]
n✝ n : ℕ
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
[PROOFSTEP]
have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
[GOAL]
n✝ n : ℕ
⊢ Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
[PROOFSTEP]
rw [← this]
[GOAL]
n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
[PROOFSTEP]
exact Fintype.card_congr (compositionAsSetEquiv n)
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ length c < Finset.card c.boundaries
[PROOFSTEP]
rw [c.card_boundaries_eq_succ_length]
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ length c < length c + 1
[PROOFSTEP]
exact lt_add_one _
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ ↑(boundary c) { val := 0, isLt := (_ : 0 < Finset.card c.boundaries) } = 0
[PROOFSTEP]
rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ Finset.min' c.boundaries (_ : Finset.Nonempty c.boundaries) = 0
[PROOFSTEP]
exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ ↑(boundary c) { val := length c, isLt := (_ : length c < Finset.card c.boundaries) } = Fin.last n
[PROOFSTEP]
convert Finset.orderEmbOfFin_last rfl c.card_boundaries_pos
[GOAL]
case h.e'_3
n : ℕ
c : CompositionAsSet n
⊢ Fin.last n = Finset.max' c.boundaries (_ : Finset.Nonempty c.boundaries)
[PROOFSTEP]
exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)
[GOAL]
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < Finset.card c.boundaries
⊢ sum (take i (blocks c)) = ↑(↑(boundary c) { val := i, isLt := h })
[PROOFSTEP]
induction' i with i IH
[GOAL]
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 })
[PROOFSTEP]
simp
[GOAL]
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 })
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
rw [c.card_boundaries_eq_succ_length] at h 
[GOAL]
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)
[PROOFSTEP]
simp [blocks, Nat.lt_of_succ_lt_succ h]
[GOAL]
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 })
[PROOFSTEP]
have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length, Nat.sub_le])
[GOAL]
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
[PROOFSTEP]
simp [blocks, length, Nat.sub_le]
[GOAL]
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 })
[PROOFSTEP]
rw [sum_take_succ _ _ A, IH B]
[GOAL]
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 })
[PROOFSTEP]
simp only [blocks, blocksFun, nthLe_ofFn']
[GOAL]
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 })
[PROOFSTEP]
apply add_tsub_cancel_of_le
[GOAL]
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) })
[PROOFSTEP]
simp
[GOAL]
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
intro hj
[GOAL]
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
rcases(c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩
[GOAL]
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i =
    { val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
rw [Subtype.ext_iff, Subtype.coe_mk] at hi 
[GOAL]
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
refine' ⟨i.1, i.2, _⟩
[GOAL]
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi :
  ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i) =
    ↑{ val := j, property := hj }
⊢ sum (take (↑i) (blocks c)) = ↑j
[PROOFSTEP]
dsimp at hi 
[GOAL]
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ sum (take (↑i) (blocks c)) = ↑j
[PROOFSTEP]
rw [← hi, c.blocks_partial_sum i.2]
[GOAL]
case mp.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin (Finset.card c.boundaries)
hi : ↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i = j
⊢ ↑(↑(boundary c) { val := ↑i, isLt := (_ : ↑i < Finset.card c.boundaries) }) =
    ↑(↑(Finset.orderEmbOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries)) i)
[PROOFSTEP]
rfl
[GOAL]
case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j) → j ∈ c.boundaries
[PROOFSTEP]
rintro ⟨i, hi, H⟩
[GOAL]
case mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j ∈ c.boundaries
[PROOFSTEP]
convert (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
[GOAL]
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
[PROOFSTEP]
have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
[GOAL]
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
⊢ ↑(boundary c) { val := i, isLt := hi } = j
[PROOFSTEP]
rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
[GOAL]
case h.e'_4
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < Finset.card c.boundaries
H : sum (take i (blocks c)) = ↑j
this : ↑(boundary c) { val := i, isLt := hi } = j
⊢ j =
    ↑(↑(Finset.orderIsoOfFin c.boundaries (_ : Finset.card c.boundaries = Finset.card c.boundaries))
        { val := i, isLt := hi })
[PROOFSTEP]
exact this.symm
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ sum (blocks c) = n
[PROOFSTEP]
have : c.blocks.take c.length = c.blocks := take_all_of_le (by simp [blocks])
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ List.length (blocks c) ≤ length c
[PROOFSTEP]
simp [blocks]
[GOAL]
n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ sum (blocks c) = n
[PROOFSTEP]
rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]
[GOAL]
n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ ↑(Fin.last n) = n
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ ∀ {i : ℕ}, i ∈ blocks c → 0 < i
[PROOFSTEP]
simp only [blocks, forall_mem_ofFn_iff, blocksFun_pos c, forall_true_iff]
[GOAL]
n : ℕ
c : Composition n
⊢ CompositionAsSet.length (toCompositionAsSet c) = length c
[PROOFSTEP]
simp [Composition.toCompositionAsSet, CompositionAsSet.length, c.card_boundaries_eq_succ_length]
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ Composition.length (toComposition c) = length c
[PROOFSTEP]
simp [CompositionAsSet.toComposition, Composition.length, Composition.blocks]
[GOAL]
n : ℕ
c : Composition n
⊢ CompositionAsSet.blocks (toCompositionAsSet c) = c.blocks
[PROOFSTEP]
let d := c.toCompositionAsSet
[GOAL]
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks (toCompositionAsSet c) = c.blocks
[PROOFSTEP]
change d.blocks = c.blocks
[GOAL]
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ CompositionAsSet.blocks d = c.blocks
[PROOFSTEP]
have length_eq : d.blocks.length = c.blocks.length :=
  by
  convert c.toCompositionAsSet_length
  simp [CompositionAsSet.blocks]
[GOAL]
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ List.length (CompositionAsSet.blocks d) = List.length c.blocks
[PROOFSTEP]
convert c.toCompositionAsSet_length
[GOAL]
case h.e'_2
n : ℕ
c : Composition n
d : CompositionAsSet n := toCompositionAsSet c
⊢ List.length (CompositionAsSet.blocks d) = CompositionAsSet.length (toCompositionAsSet c)
[PROOFSTEP]
simp [CompositionAsSet.blocks]
[GOAL]
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
[PROOFSTEP]
suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum
[GOAL]
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)
[PROOFSTEP]
exact eq_of_sum_take_eq length_eq H
[GOAL]
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)
[PROOFSTEP]
intro i hi
[GOAL]
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)
[PROOFSTEP]
have i_lt : i < d.boundaries.card := by
  -- porting note: relied on `convert` unfolding definitions, switched to using a `simpa`simpa [CompositionAsSet.blocks,
    length_ofFn, Nat.succ_eq_add_one, d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
[GOAL]
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
[PROOFSTEP]
simpa [CompositionAsSet.blocks, length_ofFn, Nat.succ_eq_add_one, d.card_boundaries_eq_succ_length] using
  Nat.lt_succ_iff.2 hi
[GOAL]
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)
[PROOFSTEP]
have i_lt' : i < c.boundaries.card := i_lt
[GOAL]
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)
[PROOFSTEP]
have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt' 
[GOAL]
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
[PROOFSTEP]
rwa [c.card_boundaries_eq_succ_length] at i_lt' 
[GOAL]
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)
[PROOFSTEP]
have A :
  d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ = c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
  rfl
[GOAL]
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)
[PROOFSTEP]
have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
[GOAL]
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)
[PROOFSTEP]
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A, c.orderEmbOfFin_boundaries]
[GOAL]
n : ℕ
c : CompositionAsSet n
⊢ Composition.boundaries (toComposition c) = c.boundaries
[PROOFSTEP]
ext j
[GOAL]
case a
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ Composition.boundaries (toComposition c) ↔ j ∈ c.boundaries
[PROOFSTEP]
simp only [c.mem_boundaries_iff_exists_blocks_sum_take_eq, Composition.boundaries, Finset.mem_map]
[GOAL]
case a
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ a, a ∈ Finset.univ ∧ ↑(Composition.boundary (toComposition c)).toEmbedding a = j) ↔
    ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
constructor
[GOAL]
case a.mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ a, a ∈ Finset.univ ∧ ↑(Composition.boundary (toComposition c)).toEmbedding a = j) →
    ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
rintro ⟨i, _, hi⟩
[GOAL]
case a.mp.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (Composition.length (toComposition c) + 1)
left✝ : i ∈ Finset.univ
hi : ↑(Composition.boundary (toComposition c)).toEmbedding i = j
⊢ ∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j
[PROOFSTEP]
refine' ⟨i.1, _, _⟩
[GOAL]
case a.mp.intro.intro.refine'_1
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (Composition.length (toComposition c) + 1)
left✝ : i ∈ Finset.univ
hi : ↑(Composition.boundary (toComposition c)).toEmbedding i = j
⊢ ↑i < Finset.card c.boundaries
case a.mp.intro.intro.refine'_2
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (Composition.length (toComposition c) + 1)
left✝ : i ∈ Finset.univ
hi : ↑(Composition.boundary (toComposition c)).toEmbedding i = j
⊢ sum (take (↑i) (blocks c)) = ↑j
[PROOFSTEP]
simpa [c.card_boundaries_eq_succ_length] using i.2
[GOAL]
case a.mp.intro.intro.refine'_2
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : Fin (Composition.length (toComposition c) + 1)
left✝ : i ∈ Finset.univ
hi : ↑(Composition.boundary (toComposition c)).toEmbedding i = j
⊢ sum (take (↑i) (blocks c)) = ↑j
[PROOFSTEP]
simp [Composition.boundary, Composition.sizeUpTo, ← hi]
[GOAL]
case a.mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i, i < Finset.card c.boundaries ∧ sum (take i (blocks c)) = ↑j) →
    ∃ a, a ∈ Finset.univ ∧ ↑(Composition.boundary (toComposition c)).toEmbedding a = j
[PROOFSTEP]
rintro ⟨i, i_lt, hi⟩
[GOAL]
case a.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < Finset.card c.boundaries
hi : sum (take i (blocks c)) = ↑j
⊢ ∃ a, a ∈ Finset.univ ∧ ↑(Composition.boundary (toComposition c)).toEmbedding a = j
[PROOFSTEP]
refine' ⟨i, by simp, _⟩
[GOAL]
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < Finset.card c.boundaries
hi : sum (take i (blocks c)) = ↑j
⊢ ↑i ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
case a.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < Finset.card c.boundaries
hi : sum (take i (blocks c)) = ↑j
⊢ ↑(Composition.boundary (toComposition c)).toEmbedding ↑i = j
[PROOFSTEP]
rw [c.card_boundaries_eq_succ_length] at i_lt 
[GOAL]
case a.mpr.intro.intro
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
i_lt : i < length c + 1
hi : sum (take i (blocks c)) = ↑j
⊢ ↑(Composition.boundary (toComposition c)).toEmbedding ↑i = j
[PROOFSTEP]
simp [Composition.boundary, Nat.mod_eq_of_lt i_lt, Composition.sizeUpTo, hi]
[GOAL]
n✝ n : ℕ
c : Composition n
⊢ (fun c => CompositionAsSet.toComposition c) ((fun c => Composition.toCompositionAsSet c) c) = c
[PROOFSTEP]
ext1
[GOAL]
case blocks
n✝ n : ℕ
c : Composition n
⊢ ((fun c => CompositionAsSet.toComposition c) ((fun c => Composition.toCompositionAsSet c) c)).blocks = c.blocks
[PROOFSTEP]
exact c.toCompositionAsSet_blocks
[GOAL]
n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun c => Composition.toCompositionAsSet c) ((fun c => CompositionAsSet.toComposition c) c) = c
[PROOFSTEP]
ext1
[GOAL]
case boundaries
n✝ n : ℕ
c : CompositionAsSet n
⊢ ((fun c => Composition.toCompositionAsSet c) ((fun c => CompositionAsSet.toComposition c) c)).boundaries =
    c.boundaries
[PROOFSTEP]
exact c.toComposition_boundaries
[GOAL]
n✝ n : ℕ
⊢ Fintype.card (Composition n) = 2 ^ (n - 1)
[PROOFSTEP]
rw [← compositionAsSet_card n]
[GOAL]
n✝ n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
[PROOFSTEP]
exact Fintype.card_congr (compositionEquiv n)
