ι : Type ?u.30890
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: (dropLast (b :: l) ++ [getLast (b :: l) (_ : b :: l ≠ [])]) = a :: b :: l
ι : Type ?u.30890
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ dropLast (a :: b :: l) ++ [getLast (a :: b :: l) h] = a :: b :: l
rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]
case e_tail
ι : Type ?u.30890
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ dropLast (b :: l) ++ [getLast (b :: l) (_ : b :: l ≠ [])] = b :: l
ι : Type ?u.30890
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: (dropLast (b :: l) ++ [getLast (b :: l) (_ : b :: l ≠ [])]) = a :: b :: l
congr
no goals
case e_tail
ι : Type ?u.30890
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ dropLast (b :: l) ++ [getLast (b :: l) (_ : b :: l ≠ [])] = b :: l
exact dropLast_append_getLast (cons_ne_nil b l)