no goals
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
h : l' ∈ sublistsLen 0 l
⊢ length l' = 0
simp_all
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ length l' = n + 1
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ length l' = n + 1
rw [sublistsLen_succ_cons, mem_append, mem_map] at h
case inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ length l' = n + 1

case inr.intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ length (a :: l') = n + 1
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ length l' = n + 1
rcases h with (h | ⟨l', h, rfl⟩)
no goals
case inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ length l' = n + 1
exact length_of_sublistsLen h