From c4710ff5507e3b34c0daeb37d1a1cec689f29da9 Mon Sep 17 00:00:00 2001
From: Alessandro Iraci <SashaIr@users.noreply.github.com>
Date: Mon, 15 Jul 2024 10:38:44 +0200
Subject: [PATCH] Non-algebra from #12572

---
 .../Combinatorics/Enumerative/Partition.lean  | 43 +++++++++++++++++++
 Mathlib/Data/Sym/Basic.lean                   | 13 ++++++
 2 files changed, 56 insertions(+)

diff --git a/Mathlib/Combinatorics/Enumerative/Partition.lean b/Mathlib/Combinatorics/Enumerative/Partition.lean
index 5206a28a8fa28..73ae13a00953a 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition.lean
@@ -99,6 +99,34 @@ def ofSums (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : Partition n where
 def ofMultiset (l : Multiset ℕ) : Partition l.sum := ofSums _ l rfl
 #align nat.partition.of_multiset Nat.Partition.ofMultiset
 
+/-- An element `s` of `Sym σ n` induces a partition given by its multiplicities. -/
+def ofSym {n : ℕ} {σ : Type*} (s : Sym σ n) [DecidableEq σ] : n.Partition where
+  parts := s.1.dedup.map s.1.count
+  parts_pos := by simp [Multiset.count_pos]
+  parts_sum := by
+    show ∑ a ∈ s.1.toFinset, count a s.1 = n
+    rw [toFinset_sum_count_eq]
+    exact s.2
+
+variable {n : ℕ} {σ τ : Type*} [DecidableEq σ] [DecidableEq τ]
+
+lemma ofSym_map (e : σ ≃ τ) (s : Sym σ n) :
+    ofSym (s.map e) = ofSym s := by
+  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, toFinset_val, mk.injEq]
+  rw [Multiset.dedup_map_of_injective e.injective]
+  simp only [map_map, Function.comp_apply]
+  congr; funext i
+  rw [← Multiset.count_map_eq_count' e _ e.injective]
+
+/-- An equivalence between `σ` and `τ` induces an equivalence between the subtypes of `Sym σ n` and
+`Sym τ n` corresponding to a given partition. -/
+def ofSym_shape_equiv (μ : Partition n) (e : σ ≃ τ) :
+    {x : Sym σ n // ofSym x = μ} ≃ {x : Sym τ n // ofSym x = μ} where
+  toFun := fun x => ⟨Sym.equivCongr e x, by simp [ofSym_map, x.2]⟩
+  invFun := fun x => ⟨Sym.equivCongr e.symm x, by simp [ofSym_map, x.2]⟩
+  left_inv := by intro x; simp
+  right_inv := by intro x; simp
+
 /-- The partition of exactly one part. -/
 def indiscrete (n : ℕ) : Partition n := ofSums n {n} rfl
 #align nat.partition.indiscrete_partition Nat.Partition.indiscrete
@@ -123,6 +151,21 @@ instance UniquePartitionZero : Unique (Partition 0) where
 instance UniquePartitionOne : Unique (Partition 1) where
   uniq _ := Partition.ext _ _ <| by simp
 
+lemma ofSym_one (s : Sym σ 1) : ofSym s = indiscrete 1 := by
+  ext; simp
+
+/-- The equivalence between `σ` and `1`-tuples of elements of σ -/
+def ofSym_equiv_indiscrete (σ : Type*) [DecidableEq σ] : σ ≃
+    { a : Sym σ 1 // ofSym a = indiscrete 1 } where
+  toFun := fun a => ⟨Sym.oneEquiv a, by ext; simp⟩
+  invFun := fun a => Sym.oneEquiv.symm a.1
+  left_inv := by intro a; simp only [Sym.oneEquiv_apply]; rfl
+  right_inv := by intro a; simp only [Equiv.apply_symm_apply, Subtype.coe_eta]
+
+@[simp]
+lemma ofSym_equiv_indiscrete_apply (i : σ) :
+    ((ofSym_equiv_indiscrete σ) i : Multiset σ) = {i} := rfl
+
 /-- The number of times a positive integer `i` appears in the partition `ofSums n l hl` is the same
 as the number of times it appears in the multiset `l`.
 (For `i = 0`, `Partition.non_zero` combined with `Multiset.count_eq_zero_of_not_mem` gives that
diff --git a/Mathlib/Data/Sym/Basic.lean b/Mathlib/Data/Sym/Basic.lean
index e55b06848aa6d..2709848c2c9c1 100644
--- a/Mathlib/Data/Sym/Basic.lean
+++ b/Mathlib/Data/Sym/Basic.lean
@@ -534,6 +534,19 @@ theorem mem_append_iff {s' : Sym α m} : a ∈ s.append s' ↔ a ∈ s ∨ a ∈
   Multiset.mem_add
 #align sym.mem_append_iff Sym.mem_append_iff
 
+/-- Defines an equivalence between `α` and `Sym α 1`. -/
+@[simps apply]
+def oneEquiv : α ≃ Sym α 1 where
+  toFun a := ⟨{a}, by simp⟩
+  invFun s := (Equiv.subtypeQuotientEquivQuotientSubtype
+      (·.length = 1) _ (fun l ↦ Iff.rfl) (fun l l' ↦ by rfl) s).liftOn
+    (fun l ↦ l.1.head <| List.length_pos.mp <| by simp)
+    fun ⟨_, _⟩ ⟨_, h⟩ ↦ fun perm ↦ by
+      obtain ⟨a, rfl⟩ := List.length_eq_one.mp h
+      exact List.eq_of_mem_singleton (perm.mem_iff.mp <| List.head_mem _)
+  left_inv a := by rfl
+  right_inv := by rintro ⟨⟨l⟩, h⟩; obtain ⟨a, rfl⟩ := List.length_eq_one.mp h; rfl
+
 /-- Fill a term `m : Sym α (n - i)` with `i` copies of `a` to obtain a term of `Sym α n`.
 This is a convenience wrapper for `m.append (replicate i a)` that adjusts the term using
 `Sym.cast`. -/