no goals
ι : Type ?u.198199
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List α
x✝ : l ≠ []
⊢ dropLast ([] ++ l) = [] ++ dropLast l
simp only [nil_append]
case x_2
ι : Type ?u.198199
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List α
a : α
l' : List α
h : l ≠ []
⊢ l' ++ l = [] → False
ι : Type ?u.198199
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List α
a : α
l' : List α
h : l ≠ []
⊢ dropLast (a :: l' ++ l) = a :: l' ++ dropLast l
rw [cons_append, dropLast, dropLast_append_of_ne_nil l' h, cons_append]
no goals
case x_2
ι : Type ?u.198199
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List α
a : α
l' : List α
h : l ≠ []
⊢ l' ++ l = [] → False
simp [h]