no goals
α : Type u_1
l₁ l₂ : List α
n : Nat
h₁ : length l₁ ≤ n
h₂ : n < length (l₁ ++ l₂)
⊢ some (get (l₁ ++ l₂) { val := n, isLt := h₂ }) =
    some (get l₂ { val := n - length l₁, isLt := (_ : n - length l₁ < length l₂) })
rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]