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

State before:
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ get (l ++ [a]) { val := length l, isLt := h } = a
Tactic:
apply Option.some.inj
State after:
case x
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ some (get (l ++ [a]) { val := length l, isLt := h }) = some a

State before:
case x
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ some (get (l ++ [a]) { val := length l, isLt := h }) = some a
Tactic:
rw [←get?_eq_get, get?_concat_length]
State after:
no goals