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

case cons
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
n : ℕ
⊢ tail (drop n (hd :: tl)) = drop (n + 1) (hd :: tl)
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
⊢ tail (drop n l) = drop (n + 1) l
induction' l with hd tl hl generalizing n
no goals
case nil
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ n : ℕ
⊢ tail (drop n []) = drop (n + 1) []
simp
case cons.zero
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
⊢ tail (drop zero (hd :: tl)) = drop (zero + 1) (hd :: tl)

case cons.succ
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
n✝ : ℕ
⊢ tail (drop (succ n✝) (hd :: tl)) = drop (succ n✝ + 1) (hd :: tl)
case cons
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
n : ℕ
⊢ tail (drop n (hd :: tl)) = drop (n + 1) (hd :: tl)
cases n
no goals
case cons.zero
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
⊢ tail (drop zero (hd :: tl)) = drop (zero + 1) (hd :: tl)
simp
no goals
case cons.succ
ι : Type ?u.199621
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ (n : ℕ), tail (drop n tl) = drop (n + 1) tl
n✝ : ℕ
⊢ tail (drop (succ n✝) (hd :: tl)) = drop (succ n✝ + 1) (hd :: tl)
simp [hl]