Theorem: List.mem_of_mem_take (One.lean)

State before:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ l
Tactic:
rw [← take_append_drop n l]
State after:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ take n l ++ drop n l

State before:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ take n l ++ drop n l
Tactic:
apply mem_append_left _ h
State after:
no goals