case nil
ι : Type ?u.204814
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
n : ℕ
⊢ drop n ([] ++ l₂) = drop n [] ++ drop (n - length []) l₂

case cons
ι : Type ?u.204814
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - length tail✝) l₂
n : ℕ
⊢ drop n (head✝ :: tail✝ ++ l₂) = drop n (head✝ :: tail✝) ++ drop (n - length (head✝ :: tail✝)) l₂
ι : Type ?u.204814
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
⊢ drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - length l₁) l₂
induction l₁ generalizing n
no goals
case cons
ι : Type ?u.204814
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - length tail✝) l₂
n : ℕ
⊢ drop n (head✝ :: tail✝ ++ l₂) = drop n (head✝ :: tail✝) ++ drop (n - length (head✝ :: tail✝)) l₂
cases n <;> simp [*]
no goals
case nil
ι : Type ?u.204814
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
n : ℕ
⊢ drop n ([] ++ l₂) = drop n [] ++ drop (n - length []) l₂
simp