feat(Mathlib/Data): setOf_mem_list_eq_singleton_of_nodup

Mathlib/Data/List/Lemmas.lean

@@ -17,6 +17,18 @@ variable {α β γ : Type*}
 
 namespace List
 
+theorem set_of_mem_empty : { x | x ∈ ([] : List α) } = ∅ := by
+  ext
+  rw [Set.mem_setOf_eq, Set.mem_empty_iff_false, List.mem_nil_iff]
+
+theorem set_of_mem_eq_empty_iff (l : List α) : { x | x ∈ l } = ∅ ↔ l = [] := by
+  refine ⟨fun h ↦ eq_nil_iff_forall_not_mem.mpr ?_, fun h ↦ ?_⟩
+  · rw [Set.empty_def, Set.setOf_iff] at h
+    rw [h]
+    exact fun _ a ↦ a
+  · subst h
+    exact set_of_mem_empty
+
 set_option linter.deprecated false in
 @[simp, deprecated "No deprecation message was provided." (since := "2024-10-17")]
 lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum := rfl

Mathlib/Data/List/Nodup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau
 -/
 import Mathlib.Data.List.Forall2
+import Mathlib.Data.List.Lemmas
 import Mathlib.Data.Set.Pairwise.Basic
 
 /-!
@@ -388,6 +389,22 @@ theorem Nodup.take_eq_filter_mem [DecidableEq α] :
     intro x hx
     have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
     simp (config := {contextual := true}) [List.mem_filter, this, hx]
+
+theorem setOf_singleton_iff_nodup (H : Nodup l) {a : α} [DecidableEq α]
+    : { x | x ∈ l } = {a} ↔ l = [a] := by
+  refine ⟨fun h ↦ ?_, by simp_all⟩
+  induction' l with a' l
+  · absurd h
+    rw [set_of_mem_empty]
+    exact (Set.singleton_ne_empty a).symm
+  · have h₁ := {x | x ∈ l}.mem_insert a'
+    rw [List.set_of_mem_cons] at h
+    rw [h] at h₁
+    rw [h₁] at h
+    congr
+    exact l.set_of_mem_eq_empty_iff.mp <|
+      (Set.insert_diff_self_of_not_mem (Set.nmem_setOf_iff.mpr H.not_mem)).symm.trans (by simp_all)
+
 end List
 
 theorem Option.toList_nodup : ∀ o : Option α, o.toList.Nodup

Mathlib/Data/Set/Basic.lean

@@ -193,6 +193,9 @@ theorem mem_of_mem_of_subset {x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t
 theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b := by
   tauto
 
+@[simp]
+theorem setOf_iff {p q : α → Prop} : { x | p x } = { x | q x } ↔ p = q := by rfl
+
 /-! ### Lemmas about `mem` and `setOf` -/
 
 theorem mem_setOf {a : α} {p : α → Prop} : a ∈ { x | p x } ↔ p a :=