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

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
n : ℕ
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, sum ns ≤ length l → map length (splitWrtCompositionAux l ns) = ns
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 → map length (splitWrtCompositionAux l ns) = ns
l : List α
h : n + sum ns ≤ length l
⊢ map length (splitWrtCompositionAux l (n :: ns)) = n :: ns
case nil
n : ℕ
α : Type u_1
l : List α
h : True
⊢ map length (splitWrtCompositionAux l []) = []

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
. simp
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
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
have := le_trans (Nat.le_add_right _ _) h
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
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
simp only [splitWrtCompositionAux_cons, this]
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
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
dsimp
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

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
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
rw [length_take, IH] <;> simp [length_drop]
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
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

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
. assumption
no goals
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
. exact le_tsub_of_add_le_left h
no goals
case nil
n : ℕ
α : Type u_1
l : List α
h : True
⊢ map length (splitWrtCompositionAux l []) = []
simp
no goals
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
assumption
no goals
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
exact le_tsub_of_add_le_left h