α : Type u_1
l₁ l₂ : List α
n : Nat
hn : n < length l₁
hn' : n < length (l₁ ++ l₂)
⊢ get? (l₁ ++ l₂) n = get? l₁ n
α : Type u_1
l₁ l₂ : List α
n : Nat
hn : n < length l₁
⊢ get? (l₁ ++ l₂) n = get? l₁ n
have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
  length_append .. ▸ Nat.le_add_right ..
no goals
α : Type u_1
l₁ l₂ : List α
n : Nat
hn : n < length l₁
hn' : n < length (l₁ ++ l₂)
⊢ get? (l₁ ++ l₂) n = get? l₁ n
rw [get?_eq_get hn, get?_eq_get hn', get_append]