rw [get_of_eq (l.take_append_drop n).symm, get_append_left]
α : Type u
β : Type v
γ : Type w
l : List α
n i : Nat
hi₁ : i < length (take n l)
hi₂ : i < length l
⊢ get (take n l) { val := i, isLt := hi₁ } = get l { val := i, isLt := hi₂ }
no goals