-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem map_length_splitWrtCompositionAux {ns : List ℕ} :
    ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ n ≤ l.length

Tactic:
assumption

Result:
no goals

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Tactic:
simp only [splitWrtCompositionAux_cons, this]

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ map length (take n l :: (drop n l).splitWrtCompositionAux ns) = n :: ns

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : (n :: ns).sum ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Tactic:
simp only [sum_cons] at h

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ (take n l).length :: map length ((drop n l).splitWrtCompositionAux ns) = n :: ns

Tactic:
rw [length_take, IH] <;> simp [length_drop]

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ n ≤ l.length

case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ ns.sum ≤ l.length - n

Proof state:
case nil
α : Type u_1
⊢ ∀ {l : List α}, [].sum ≤ l.length → map length (l.splitWrtCompositionAux []) = []

Tactic:
simp [splitWrtCompositionAux]

Result:
no goals

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ ns.sum ≤ l.length - n

Tactic:
exact le_tsub_of_add_le_left h

Result:
no goals

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Tactic:
have := le_trans (Nat.le_add_right _ _) h

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ map length (take n l :: (drop n l).splitWrtCompositionAux ns) = n :: ns

Tactic:
dsimp

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : n + ns.sum ≤ l.length
this : n ≤ l.length
⊢ (take n l).length :: map length ((drop n l).splitWrtCompositionAux ns) = n :: ns

Proof state:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
⊢ ∀ {l : List α}, (n :: ns).sum ≤ l.length → map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Tactic:
intro l h

Result:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
l : List α
h : (n :: ns).sum ≤ l.length
⊢ map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns