feat: remove DecidableEq argument from Finset.sym2 (#8211)

Mathlib.lean

@@ -1617,6 +1617,7 @@ import Mathlib.Data.List.Sections
 import Mathlib.Data.List.Sigma
 import Mathlib.Data.List.Sort
 import Mathlib.Data.List.Sublists
+import Mathlib.Data.List.Sym
 import Mathlib.Data.List.TFAE
 import Mathlib.Data.List.ToFinsupp
 import Mathlib.Data.List.Zip
@@ -1663,6 +1664,7 @@ import Mathlib.Data.Multiset.Range
 import Mathlib.Data.Multiset.Sections
 import Mathlib.Data.Multiset.Sort
 import Mathlib.Data.Multiset.Sum
+import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.MvPolynomial.Basic
 import Mathlib.Data.MvPolynomial.Cardinal
 import Mathlib.Data.MvPolynomial.Comap

Mathlib/Data/Finset/Sym.lean

@@ -8,7 +8,7 @@ Authors: Yaël Dillies
 import Mathlib.Data.Finset.Lattice
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Vector
-import Mathlib.Data.Sym.Sym2
+import Mathlib.Data.Multiset.Sym
 
 #align_import data.finset.sym from "leanprover-community/mathlib"@"02ba8949f486ebecf93fe7460f1ed0564b5e442c"
 
@@ -23,6 +23,7 @@ This file defines the symmetric powers of a finset as `Finset (Sym α n)` and `F
   whose elements are in `s`.
 * `Finset.sym2`: The symmetric square of a finset. `s.sym2` is all the pairs whose elements are in
   `s`.
+* A `Fintype (Sym2 α)` instance that does not require `DecidableEq α`.
 
 ## TODO
 
@@ -32,88 +33,132 @@ This file defines the symmetric powers of a finset as `Finset (Sym α n)` and `F
 
 namespace Finset
 
-variable {α : Type*} [DecidableEq α] {s t : Finset α} {a b : α}
+variable {α : Type*}
 
-theorem isDiag_mk'_of_mem_diag {a : α × α} (h : a ∈ s.diag) : Sym2.IsDiag ⟦a⟧ :=
-  (Sym2.isDiag_iff_proj_eq _).2 (mem_diag.1 h).2
-#align finset.is_diag_mk_of_mem_diag Finset.isDiag_mk'_of_mem_diag
+/-- `s.sym2` is the finset of all unordered pairs of elements from `s`.
+It is the image of `s ×ˢ s` under the quotient `α × α → Sym2 α`. -/
+@[simps]
+protected def sym2 (s : Finset α) : Finset (Sym2 α) := ⟨s.1.sym2, s.2.sym2⟩
+#align finset.sym2 Finset.sym2
 
-theorem not_isDiag_mk'_of_mem_offDiag {a : α × α} (h : a ∈ s.offDiag) : ¬Sym2.IsDiag ⟦a⟧ := by
-  rw [Sym2.isDiag_iff_proj_eq]
-  exact (mem_offDiag.1 h).2.2
-#align finset.not_is_diag_mk_of_mem_off_diag Finset.not_isDiag_mk'_of_mem_offDiag
+section
+variable {s t : Finset α} {a b : α}
 
-section Sym2
+theorem mk_mem_sym2_iff : ⟦(a, b)⟧ ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s := by
+  rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]
+#align finset.mk_mem_sym2_iff Finset.mk_mem_sym2_iff
 
-variable {m : Sym2 α}
+@[simp]
+theorem mem_sym2_iff {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s := by
+  rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]
+  simp only [mem_val]
+#align finset.mem_sym2_iff Finset.mem_sym2_iff
 
-/-- Lifts a finset to `Sym2 α`. `s.sym2` is the finset of all pairs with elements in `s`. -/
-protected def sym2 (s : Finset α) : Finset (Sym2 α) := (s ×ˢ s).image Quotient.mk'
-#align finset.sym2 Finset.sym2
+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)
 
+-- Note(kmill): Using a default argument to make this simp lemma more general.
 @[simp]
-theorem mem_sym2_iff : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s := by
-  refine
-    mem_image.trans
-      ⟨?_, fun h ↦ ⟨m.out, mem_product.2 ⟨h _ m.out_fst_mem, h _ m.out_snd_mem⟩, m.out_eq⟩⟩
-  rintro ⟨⟨a, b⟩, h, rfl⟩
-  rw [Quotient.mk', @Sym2.ball _ (fun x ↦ x ∈ s)]
-  rwa [mem_product] at h
-#align finset.mem_sym2_iff Finset.mem_sym2_iff
+theorem sym2_univ [Fintype α] (inst : Fintype (Sym2 α) := Sym2.instFintype) :
+    (univ : Finset α).sym2 = univ := by
+  ext
+  simp only [mem_sym2_iff, mem_univ, implies_true]
+#align finset.sym2_univ Finset.sym2_univ
+
+@[simp, mono]
+theorem sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2 := by
+  rw [← val_le_iff, sym2_val, sym2_val]
+  apply Multiset.sym2_mono
+  rwa [val_le_iff]
+#align finset.sym2_mono Finset.sym2_mono
+
+theorem monotone_sym2 : Monotone (Finset.sym2 : Finset α → _) := fun _ _ => sym2_mono
+
+theorem injective_sym2 : Function.Injective (Finset.sym2 : Finset α → _) := by
+  intro s t h
+  ext x
+  simpa using congr(⟦(x, x)⟧ ∈ $h)
+
+theorem strictMono_sym2 : StrictMono (Finset.sym2 : Finset α → _) :=
+  monotone_sym2.strictMono_of_injective injective_sym2
 
-theorem mk'_mem_sym2_iff : ⟦(a, b)⟧ ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s := by rw [mem_sym2_iff, Sym2.ball]
-#align finset.mk_mem_sym2_iff Finset.mk'_mem_sym2_iff
+theorem sym2_toFinset [DecidableEq α] (m : Multiset α) :
+    m.toFinset.sym2 = m.sym2.toFinset := by
+  ext z
+  refine z.ind fun x y ↦ ?_
+  simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]
 
 @[simp]
 theorem sym2_empty : (∅ : Finset α).sym2 = ∅ := rfl
 #align finset.sym2_empty Finset.sym2_empty
 
 @[simp]
 theorem sym2_eq_empty : s.sym2 = ∅ ↔ s = ∅ := by
-  rw [Finset.sym2, image_eq_empty, product_eq_empty, or_self_iff]
+  rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]
 #align finset.sym2_eq_empty Finset.sym2_eq_empty
 
 @[simp]
 theorem sym2_nonempty : s.sym2.Nonempty ↔ s.Nonempty := by
-  rw [Finset.sym2, Nonempty.image_iff, nonempty_product, and_self_iff]
+  rw [← not_iff_not]
+  simp_rw [not_nonempty_iff_eq_empty, sym2_eq_empty]
 #align finset.sym2_nonempty Finset.sym2_nonempty
 
-alias ⟨_, nonempty.sym2⟩ := sym2_nonempty
-#align finset.nonempty.sym2 Finset.nonempty.sym2
-
--- Porting note: attribute does not exist
--- attribute [protected] nonempty.sym2
+protected alias ⟨_, Nonempty.sym2⟩ := sym2_nonempty
+#align finset.nonempty.sym2 Finset.Nonempty.sym2
 
 @[simp]
-theorem sym2_univ [Fintype α] : (univ : Finset α).sym2 = univ := by
-  ext
-  simp only [mem_sym2_iff, mem_univ, implies_true]
-#align finset.sym2_univ Finset.sym2_univ
-
-@[simp]
-theorem sym2_singleton (a : α) : ({a} : Finset α).sym2 = {Sym2.diag a} := by
-  rw [Finset.sym2, singleton_product_singleton, image_singleton, Sym2.diag, Quotient.mk']
+theorem sym2_singleton (a : α) : ({a} : Finset α).sym2 = {Sym2.diag a} := rfl
 #align finset.sym2_singleton Finset.sym2_singleton
 
+/-- Finset **stars and bars** for the case `n = 2`. -/
+theorem card_sym2 (s : Finset α) : s.sym2.card = Nat.choose (s.card + 1) 2 := by
+  rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]
+#align finset.card_sym2 Finset.card_sym2
+
+end
+
+variable [DecidableEq α] {s t : Finset α} {a b : α}
+
+theorem sym2_eq_image : s.sym2 = (s ×ˢ s).image (Quotient.mk _) := by
+  ext z
+  refine z.ind fun x y ↦ ?_
+  rw [mk_mem_sym2_iff, mem_image]
+  constructor
+  · intro h
+    use (x, y)
+    simp only [mem_product, h, and_self, true_and]
+  · rintro ⟨⟨a, b⟩, h⟩
+    simp only [mem_product, Sym2.eq_iff] at h
+    obtain ⟨h, (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)⟩ := h
+      <;> simp [h]
+
+theorem isDiag_mk_of_mem_diag {a : α × α} (h : a ∈ s.diag) : Sym2.IsDiag ⟦a⟧ :=
+  (Sym2.isDiag_iff_proj_eq _).2 (mem_diag.1 h).2
+#align finset.is_diag_mk_of_mem_diag Finset.isDiag_mk_of_mem_diag
+
+theorem not_isDiag_mk_of_mem_offDiag {a : α × α} (h : a ∈ s.offDiag) : ¬Sym2.IsDiag ⟦a⟧ := by
+  rw [Sym2.isDiag_iff_proj_eq]
+  exact (mem_offDiag.1 h).2.2
+#align finset.not_is_diag_mk_of_mem_off_diag Finset.not_isDiag_mk_of_mem_offDiag
+
+section Sym2
+
+variable {m : Sym2 α}
+
 -- Porting note: add this lemma and remove simp in the next lemma since simpNF lint
 -- warns that its LHS is not in normal form
 @[simp]
 theorem diag_mem_sym2_mem_iff : (∀ b, b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s := by
   rw [← mem_sym2_iff]
-  exact mk'_mem_sym2_iff.trans <| and_self_iff
+  exact mk_mem_sym2_iff.trans <| and_self_iff
 
 theorem diag_mem_sym2_iff : Sym2.diag a ∈ s.sym2 ↔ a ∈ s := by simp [diag_mem_sym2_mem_iff]
 #align finset.diag_mem_sym2_iff Finset.diag_mem_sym2_iff
 
-@[simp]
-theorem sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2 := fun _m he ↦
-  mem_sym2_iff.2 fun _a ha ↦ h <| mem_sym2_iff.1 he _ ha
-#align finset.sym2_mono Finset.sym2_mono
-
 theorem image_diag_union_image_offDiag :
-    s.diag.image Quotient.mk' ∪ s.offDiag.image Quotient.mk' = s.sym2 := by
-  rw [← image_union, diag_union_offDiag]
-  rfl
+    s.diag.image (Quotient.mk _) ∪ s.offDiag.image (Quotient.mk _) = s.sym2 := by
+  rw [← image_union, diag_union_offDiag, sym2_eq_image]
 #align finset.image_diag_union_image_off_diag Finset.image_diag_union_image_offDiag
 
 end Sym2