-- Mathlib/Data/List/Nodup.lean
theorem Nodup.take_eq_filter_mem [DecidableEq α] :
    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (l.take n).elem
  | [], n, _ => by simp
  | b::l, 0, _ => by simp
  | b::l, n+1, hl => by
    rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
    congr 1
    refine List.filter_congr ?_
    intro x hx
    have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
    simp (config := {contextual := true}) [List.mem_filter, this, hx]

Proof state:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
this : x ≠ b
⊢ elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)

Tactic:
simp (config := {contextual := true}) [List.mem_filter, this, hx]

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x✝ : [].Nodup
⊢ take n [] = List.filter (fun a => elem a (take n [])) []

Tactic:
simp

Result:
no goals

Proof state:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)

Tactic:
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)

Result:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
this : x ≠ b
⊢ elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)

Proof state:
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ take (n + 1) (b :: l) = List.filter (fun a => elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]

Result:
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a => elem a (take n l)) l =
    b :: List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l

Proof state:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ ∀ x ∈ l, elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)

Tactic:
intro x hx

Result:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)

Proof state:
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a => elem a (take n l)) l =
    b :: List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l

Tactic:
congr 1

Result:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ List.filter (fun a => elem a (take n l)) l =
    List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l

Proof state:
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ elem b (b :: List.filter (fun a => elem a (take n l)) l) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
x✝ : (b :: l).Nodup
⊢ take 0 (b :: l) = List.filter (fun a => elem a (take 0 (b :: l))) (b :: l)

Tactic:
simp

Result:
no goals

Proof state:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ List.filter (fun a => elem a (take n l)) l =
    List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l

Tactic:
refine List.filter_congr ?_

Result:
case e_tail
α : Type u
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ ∀ x ∈ l, elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)