case nil
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ dropLast [] = take (pred (length [])) []

case cons
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
l : List α
⊢ dropLast (x :: l) = take (pred (length (x :: l))) (x :: l)
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
⊢ dropLast l = take (pred (length l)) l
cases' l with x l
no goals
case nil
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ dropLast [] = take (pred (length [])) []
simp [dropLast]
case cons.nil
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ x : α
⊢ dropLast [x] = take (pred (length [x])) [x]

case cons.cons
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : α
tl : List α
hl : ∀ (x : α), dropLast (x :: tl) = take (pred (length (x :: tl))) (x :: tl)
x : α
⊢ dropLast (x :: hd :: tl) = take (pred (length (x :: hd :: tl))) (x :: hd :: tl)
case cons
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
l : List α
⊢ dropLast (x :: l) = take (pred (length (x :: l))) (x :: l)
induction' l with hd tl hl generalizing x
no goals
case cons.nil
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ x : α
⊢ dropLast [x] = take (pred (length [x])) [x]
simp [dropLast]
no goals
case cons.cons
ι : Type ?u.195932
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : α
tl : List α
hl : ∀ (x : α), dropLast (x :: tl) = take (pred (length (x :: tl))) (x :: tl)
x : α
⊢ dropLast (x :: hd :: tl) = take (pred (length (x :: hd :: tl))) (x :: hd :: tl)
simp [dropLast, hl]