no goals
ι : Type ?u.207245
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
i : ℕ
⊢ drop (length l₁ + i) (l₁ ++ l₂) = drop i l₂
rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;> simp