no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
n : ℕ
x✝ : Nodup []
⊢ take n [] = List.filter (fun x => decide (x ∈ take n [])) []
simp
no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
x✝ : Nodup (b :: l)
⊢ take 0 (b :: l) = List.filter (fun x => decide (x ∈ take 0 (b :: l))) (b :: l)
simp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ b :: List.filter (fun x => decide (x ∈ take n l)) l =
    b :: List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ take (n + 1) (b :: l) = List.filter (fun x => decide (x ∈ take (n + 1) (b :: l))) (b :: l)
rw [take_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), List.filter_cons_of_pos _ (by simp)]
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ List.filter (fun x => decide (x ∈ take n l)) l =
    List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ b :: List.filter (fun x => decide (x ∈ take n l)) l =
    b :: List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
congr 1
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ ∀ (x : α),
    x ∈ l → (decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true)
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ List.filter (fun x => decide (x ∈ take n l)) l =
    List.filter (fun x => decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l)) l
refine' List.filter_congr' _
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ ∀ (x : α),
    x ∈ l → (decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true)
intro x hx
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
this : x ≠ b
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
no goals
case e_tail
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
x : α
hx : x ∈ l
this : x ≠ b
⊢ decide (x ∈ take n l) = true ↔ decide (x ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
simp (config := {contextual := true}) [List.mem_filter, this, hx]
no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b✝ : α
inst✝ : DecidableEq α
b : α
l : List α
n : ℕ
hl : Nodup (b :: l)
⊢ decide (b ∈ b :: List.filter (fun x => decide (x ∈ take n l)) l) = true
simp