Theorem: List.dropLast_concat_getLast (Algdata/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
Tactic:
rw [as.dropLast_eq_take, as.singleton_getLast_eq_drop]
State after:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ take (length as - 1) as ++ drop (length as - 1) as = as

State before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ take (length as - 1) as ++ drop (length as - 1) as = as
Tactic:
exact as.take_append_drop (as.length - 1)
State after:
no goals