Theorem: List.drop_isInfix (One.lean)

State before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ drop n l <:+: l
Tactic:
exists List.take n l, []
State after:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l ++ drop n l ++ [] = l

State before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l ++ drop n l ++ [] = l
Tactic:
simp only [take_append_drop, append_nil]
State after:
no goals