Theorem: List.take_isInfix (One.lean)

State before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l <:+: l
Tactic:
exists [], drop 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 [nil_append, take_append_drop]
State after:
no goals