feat(List): a list contains a single element iff it's a singleton (#20488)

Adds `setOf_eq_singleton_iff_of_nodup` with the generalizing `setOf_nodup_perm`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Tristan F.-R. <tristanf@reed.edu>

Author: tristan-f-r

Mathlib/Data/List/Lemmas.lean

@@ -17,6 +17,10 @@ variable {α β γ : Type*}
 
 namespace List
 
+@[simp]
+theorem setOf_mem_eq_empty_iff {l : List α} : { x | x ∈ l } = ∅ ↔ l = [] :=
+  Set.eq_empty_iff_forall_not_mem.trans eq_nil_iff_forall_not_mem.symm
+
 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/Set/Basic.lean

@@ -195,6 +195,10 @@ 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
 
+theorem setOf_injective : Function.Injective (@setOf α) := injective_id
+
+theorem setOf_inj {p q : α → Prop} : { x | p x } = { x | q x } ↔ p = q := Iff.rfl
+
 /-! ### Lemmas about `mem` and `setOf` -/
 
 theorem mem_setOf {a : α} {p : α → Prop} : a ∈ { x | p x } ↔ p a :=

Mathlib/Data/Set/Insert.lean

@@ -264,6 +264,21 @@ theorem eq_singleton_iff_nonempty_unique_mem : s = {a} ↔ s.Nonempty ∧ ∀ x
   eq_singleton_iff_unique_mem.trans <|
     and_congr_left fun H => ⟨fun h' => ⟨_, h'⟩, fun ⟨x, h⟩ => H x h ▸ h⟩
 
+theorem setOf_mem_list_eq_replicate {l : List α} {a : α} :
+    { x | x ∈ l } = {a} ↔ ∃ n > 0, l = List.replicate n a := by
+  simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
+    List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩
+
+theorem setOf_mem_list_eq_singleton_of_nodup {l : List α} (H : l.Nodup) {a : α} :
+    { x | x ∈ l } = {a} ↔ l = [a] := by
+  constructor
+  · rw [setOf_mem_list_eq_replicate]
+    rintro ⟨n, hn, rfl⟩
+    simp only [List.nodup_replicate] at H
+    simp [show n = 1 by omega]
+  · rintro rfl
+    simp
+
 -- while `simp` is capable of proving this, it is not capable of turning the LHS into the RHS.
 @[simp]
 theorem default_coe_singleton (x : α) : (default : ({x} : Set α)) = ⟨x, rfl⟩ :=