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'
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
⊢ 0 < length l'
have : l'.length ∈ (l.splitWrtComposition c).map List.length :=
  List.mem_map_of_mem List.length h
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
this : length l' ∈ c.blocks
⊢ 0 < length l'
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'
rw [map_length_splitWrtComposition] at this
no goals
n : ℕ
α : Type u_1
l l' : List α
c : Composition (length l)
h : l' ∈ splitWrtComposition l c
this : length l' ∈ c.blocks
⊢ 0 < length l'
exact c.blocks_pos this