case nil
n : ℕ
α : Type u_1
l : List α
h : 0 = length l
⊢ join (splitWrtCompositionAux l []) = l

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
n : ℕ
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, sum ns = length l → join (splitWrtCompositionAux l ns) = l
induction' ns with n ns IH <;> intro l h <;> simp at h
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
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
simp only [splitWrtCompositionAux_cons]
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
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
dsimp
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

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)
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
rw [IH]
no goals
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)
. rw [length_drop, ← h, add_tsub_cancel_left]
no goals
case nil
n : ℕ
α : Type u_1
l : List α
h : 0 = length l
⊢ join (splitWrtCompositionAux l []) = l
exact (length_eq_zero.1 h.symm).symm
no goals
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
simp
no goals
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)
rw [length_drop, ← h, add_tsub_cancel_left]