feat: basic results about Finset.sym2 (#14212)

Mathlib/Data/Finset/Sym.lean

@@ -32,7 +32,7 @@ This file defines the symmetric powers of a finset as `Finset (Sym α n)` and `F
 
 namespace Finset
 
-variable {α : Type*}
+variable {α β : Type*}
 
 /-- `s.sym2` is the finset of all unordered pairs of elements from `s`.
 It is the image of `s ×ˢ s` under the quotient `α × α → Sym2 α`. -/
@@ -53,6 +53,27 @@ theorem mem_sym2_iff {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s := by
   simp only [mem_val]
 #align finset.mem_sym2_iff Finset.mem_sym2_iff
 
+theorem sym2_cons (a : α) (s : Finset α) (ha : a ∉ s) :
+    (s.cons a ha).sym2 = ((s.cons a ha).map <| Sym2.mkEmbedding a).disjUnion s.sym2 (by
+      simp [Finset.disjoint_left, ha]) :=
+  val_injective <| Multiset.sym2_cons _ _
+
+theorem sym2_insert [DecidableEq α] (a : α) (s : Finset α) :
+    (insert a s).sym2 = ((insert a s).image fun b => s(a, b)) ∪ s.sym2 := by
+  obtain ha | ha := Decidable.em (a ∈ s)
+  · simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]
+    aesop
+  · simpa [map_eq_image] using sym2_cons a s ha
+
+theorem sym2_map (f : α ↪ β) (s : Finset α) : (s.map f).sym2 = s.sym2.map (.sym2Map f) :=
+  val_injective <| s.val.sym2_map _
+
+theorem sym2_image [DecidableEq β] (f : α → β) (s : Finset α) :
+    (s.image f).sym2 = s.sym2.image (Sym2.map f) := by
+  apply val_injective
+  dsimp [Finset.sym2]
+  rw [← Multiset.dedup_sym2, Multiset.sym2_map]
+
 instance _root_.Sym2.instFintype [Fintype α] : Fintype (Sym2 α) where
   elems := Finset.univ.sym2
   complete := fun x ↦ by rw [mem_sym2_iff]; exact (fun a _ ↦ mem_univ a)

Mathlib/Data/List/Sym.lean

@@ -27,7 +27,7 @@ from a given list. These are list versions of `Nat.multichoose`.
 
 namespace List
 
-variable {α : Type*}
+variable {α β : Type*}
 
 section Sym2
 
@@ -37,6 +37,12 @@ protected def sym2 : List α → List (Sym2 α)
   | [] => []
   | x :: xs => (x :: xs).map (fun y => s(x, y)) ++ xs.sym2
 
+theorem sym2_map (f : α → β) (xs : List α) :
+    (xs.map f).sym2 = xs.sym2.map (Sym2.map f) := by
+  induction xs with
+  | nil => simp [List.sym2]
+  | cons x xs ih => simp [List.sym2, ih, Function.comp]
+
 theorem mem_sym2_cons_iff {x : α} {xs : List α} {z : Sym2 α} :
     z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y, y ∈ xs ∧ z = s(x, y)) ∨ z ∈ xs.sym2 := by
   simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]
@@ -112,6 +118,67 @@ protected theorem Nodup.sym2 {xs : List α} (h : xs.Nodup) : xs.sym2.Nodup := by
       simp only [Sym2.eq_iff, true_and]
       rintro (rfl | ⟨rfl, rfl⟩) <;> rfl
 
+theorem map_mk_sublist_sym2 (x : α) (xs : List α) (h : x ∈ xs) :
+    map (fun y ↦ s(x, y)) xs <+ xs.sym2 := by
+  induction xs with
+  | nil => simp
+  | cons x' xs ih =>
+    simp [List.sym2]
+    cases h with
+    | head =>
+      exact (sublist_append_left _ _).cons₂ _
+    | tail _ h =>
+      refine .cons _ ?_
+      rw [← singleton_append]
+      refine .append ?_ (ih h)
+      rw [singleton_sublist, mem_map]
+      exact ⟨_, h, Sym2.eq_swap⟩
+
+theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) :
+    (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2 := by
+  induction xs with
+  | nil => simp
+  | cons x' xs ih =>
+    simp only [mem_cons, not_or] at h
+    rw [List.sym2, map_cons, map_cons, disjoint_cons_left, disjoint_append_right,
+      disjoint_cons_right]
+    refine ⟨?_, ⟨?_, ?_⟩, ?_⟩
+    · refine not_mem_cons_of_ne_of_not_mem ?_ (not_mem_append ?_ ?_)
+      · simp [h.1]
+      · simp_rw [mem_map, not_exists, not_and]
+        intro x'' hx
+        simp_rw [Sym2.mk_eq_mk_iff, Prod.swap_prod_mk, Prod.mk.injEq, true_and]
+        rintro (⟨rfl, rfl⟩ | rfl)
+        · exact h.2 hx
+        · exact h.2 hx
+      · simp [mk_mem_sym2_iff, h.2]
+    · simp [h.1]
+    · intro z hx hy
+      rw [List.mem_map] at hx hy
+      obtain ⟨a, hx, rfl⟩ := hx
+      obtain ⟨b, hy, hx⟩ := hy
+      simp [Sym2.mk_eq_mk_iff, Ne.symm h.1] at hx
+      obtain ⟨rfl, rfl⟩ := hx
+      exact h.2 hy
+    · exact ih h.2
+
+theorem dedup_sym2 [DecidableEq α] (xs : List α) : xs.sym2.dedup = xs.dedup.sym2 := by
+  induction xs with
+  | nil => simp only [List.sym2, dedup_nil]
+  | cons x xs ih =>
+    simp only [List.sym2, map_cons, cons_append]
+    obtain hm | hm := Decidable.em (x ∈ xs)
+    · rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
+        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
+      refine mem_append_of_mem_left _ ?_
+      rw [mem_map]
+      exact ⟨_, hm, Sym2.eq_swap⟩
+    · rw [dedup_cons_of_not_mem hm, List.sym2, map_cons, ← ih, dedup_cons_of_not_mem, cons_append,
+        List.Disjoint.dedup_append, dedup_map_of_injective]
+      · exact (Sym2.mkEmbedding _).injective
+      · exact map_mk_disjoint_sym2 x xs hm
+      · simp [hm, mem_sym2_iff]
+
 protected theorem Perm.sym2 {xs ys : List α} (h : xs ~ ys) :
     xs.sym2 ~ ys.sym2 := by
   induction h with

Mathlib/Data/Multiset/Sym.lean

@@ -32,7 +32,7 @@ unordered n-tuples from a given multiset. These are multiset versions of `Nat.mu
 
 namespace Multiset
 
-variable {α : Type*}
+variable {α β : Type*}
 
 section Sym2
 
@@ -47,6 +47,17 @@ protected def sym2 (m : Multiset α) : Multiset (Sym2 α) :=
 theorem sym2_eq_zero_iff {m : Multiset α} : m.sym2 = 0 ↔ m = 0 :=
   m.inductionOn fun xs => by simp
 
+@[simp]
+theorem sym2_zero : (0 : Multiset α).sym2 = 0 := rfl
+
+theorem sym2_cons (a : α) (m : Multiset α) :
+    (m.cons a).sym2 = ((m.cons a).map <| fun b => s(a, b)) + m.sym2 :=
+  m.inductionOn fun _ => rfl
+
+theorem sym2_map (f : α → β) (m : Multiset α) :
+    (m.map f).sym2 = m.sym2.map (Sym2.map f) :=
+  m.inductionOn fun xs => by simp [List.sym2_map]
+
 theorem mk_mem_sym2_iff {m : Multiset α} {a b : α} :
     s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m :=
   m.inductionOn fun xs => by simp [List.mk_mem_sym2_iff]
@@ -72,6 +83,9 @@ theorem card_sym2 {m : Multiset α} :
   refine m.inductionOn fun xs => ?_
   simp [List.length_sym2]
 
+theorem dedup_sym2 [DecidableEq α] (m : Multiset α) : m.sym2.dedup = m.dedup.sym2 :=
+  m.inductionOn fun xs => by simp [List.dedup_sym2]
+
 end Sym2
 
 end Multiset

Mathlib/Data/Sym/Sym2.lean

@@ -288,6 +288,20 @@ theorem map.injective {f : α → β} (hinj : Injective f) : Injective (map f) :
   simp [hinj.eq_iff]
 #align sym2.map.injective Sym2.map.injective
 
+/-- `mk a` as an embedding. This is the symmetric version of `Function.Embedding.sectl`. -/
+@[simps]
+def mkEmbedding (a : α) : α ↪ Sym2 α where
+  toFun b := s(a, b)
+  inj' b₁ b₁ h := by
+    simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, true_and, Prod.swap_prod_mk] at h
+    obtain rfl | ⟨rfl, rfl⟩ := h <;> rfl
+
+/-- `Sym2.map` as an embedding. -/
+@[simps]
+def _root_.Function.Embedding.sym2Map (f : α ↪ β) : Sym2 α ↪ Sym2 β where
+  toFun := map f
+  inj' := map.injective f.injective
+
 section Membership
 
 /-! ### Membership and set coercion -/