α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ~ List.filter (fun x => decide (x ∈ take n xs)) ys
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ~ List.inter ys (take n xs)
simp only [List.inter]
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ~ List.filter (fun x => decide (x ∈ take n xs)) ys
exact Perm.trans (show xs.take n ~ xs.filter (. ∈ xs.take n) by
    conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
  (Perm.filter _ h)
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ~ List.filter (fun x => decide (x ∈ take n xs)) xs
conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]