no goals
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l₁ : List α
x✝ : Nodup l₁
⊢ List.diff l₁ [] = List.filter (fun x => decide ¬x ∈ []) l₁
simp
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : Nodup l₁
⊢ List.filter (fun a_1 => decide ((decide ¬a_1 ∈ l₂) = true ∧ decide (a_1 ≠ a) = true)) l₁ =
    List.filter (fun x => decide ¬x ∈ a :: l₂) l₁
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : Nodup l₁
⊢ List.diff l₁ (a :: l₂) = List.filter (fun x => decide ¬x ∈ a :: l₂) l₁
rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
no goals
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : Nodup l₁
⊢ List.filter (fun a_1 => decide ((decide ¬a_1 ∈ l₂) = true ∧ decide (a_1 ≠ a) = true)) l₁ =
    List.filter (fun x => decide ¬x ∈ a :: l₂) l₁
simp only [decide_not, Bool.not_eq_true', decide_eq_false_iff_not, ne_eq, and_comm,
  Bool.decide_and, find?, mem_cons, not_or]