case slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
⊢ [] ∈ sublistsLen (length []) []

case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ l₁ ∈ sublistsLen (length l₁) (a :: l₂)

case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length (a :: l₁)) (a :: l₂)
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen (length l') l
induction' h with l₁ l₂ a s IH l₁ l₂ a s IH
no goals
case slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
⊢ [] ∈ sublistsLen (length []) []
simp
case cons.nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen (length []) l₂
⊢ [] ∈ sublistsLen (length []) (a :: l₂)

case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length (b :: l₁)) (a :: l₂)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ l₁ ∈ sublistsLen (length l₁) (a :: l₂)
cases' l₁ with b l₁
no goals
case cons.nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen (length []) l₂
⊢ [] ∈ sublistsLen (length []) (a :: l₂)
simp
case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length (b :: l₁)) (a :: l₂)
rw [length, sublistsLen_succ_cons]
no goals
case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
exact mem_append_left _ IH
case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length (a :: l₁)) (a :: l₂)
rw [length, sublistsLen_succ_cons]
no goals
case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)