ι : Type ?u.37180
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
c : α
hc : c ∈ getLast? (b :: l)
⊢ dropLast (a :: b :: l) ++ [c] = a :: b :: l
ι : Type ?u.37180
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
c : α
hc : c ∈ getLast? (a :: b :: l)
⊢ dropLast (a :: b :: l) ++ [c] = a :: b :: l
rw [getLast?_cons_cons] at hc
no goals
ι : Type ?u.37180
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
c : α
hc : c ∈ getLast? (b :: l)
⊢ dropLast (a :: b :: l) ++ [c] = a :: b :: l
rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]