no goals
ι : Type ?u.213709
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i : ℕ
j : Fin (length (drop i L))
⊢ get (drop i L) j = get L { val := i + ↑j, isLt := (_ : i + ↑j < length L) }
rw [get_drop]