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)

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)
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)
induction' ns with n ns IH generalizing l i
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)

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)
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)
cases' i with i
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)
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)

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)
. rw [Nat.add_zero, List.take_zero, sum_nil, nthLe_zero]; dsimp
  simp only [splitWrtCompositionAux_cons, head!, sum, foldl, zero_add]
no goals
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)
. simp only [splitWrtCompositionAux_cons, take, sum_cons,
    Nat.add_eq, add_zero, gt_iff_lt, nthLe_cons, IH]; dsimp
  rw [Nat.succ_sub_succ_eq_sub, ←Nat.succ_eq_add_one,tsub_zero]
  simp only [← drop_take, drop_drop]
  rw [add_comm]
no goals
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)
cases hi
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)
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)
rw [Nat.add_zero, List.take_zero, sum_nil, nthLe_zero]
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
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)
dsimp
no goals
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
simp only [splitWrtCompositionAux_cons, head!, sum, foldl, zero_add]
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)
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)
simp only [splitWrtCompositionAux_cons, take, sum_cons,
  Nat.add_eq, add_zero, gt_iff_lt, nthLe_cons, IH]
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)
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)
dsimp
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)
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)
rw [Nat.succ_sub_succ_eq_sub, ←Nat.succ_eq_add_one,tsub_zero]
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)
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)
simp only [← drop_take, drop_drop]
no goals
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)
rw [add_comm]