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

State before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ concat (dropLast as) (getLast as h) = as
Tactic:
rw [List.concat_eq_append]
State after:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as

State before:
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
Tactic:
exact as.dropLast_concat_getLast h
State after:
no goals