From 7810d9d91a0a60b56ba41d05e568a6060133d051 Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Fri, 20 Jan 2023 12:30:24 +0000
Subject: [PATCH] feat: port Data.Sym.Basic (#1672)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
---
 Mathlib.lean                |   1 +
 Mathlib/Data/Sym/Basic.lean | 681 ++++++++++++++++++++++++++++++++++++
 2 files changed, 682 insertions(+)
 create mode 100644 Mathlib/Data/Sym/Basic.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 997673ca92bbd..a6705560af6ad 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -478,6 +478,7 @@ import Mathlib.Data.String.Lemmas
 import Mathlib.Data.Subtype
 import Mathlib.Data.Sum.Basic
 import Mathlib.Data.Sum.Order
+import Mathlib.Data.Sym.Basic
 import Mathlib.Data.TwoPointing
 import Mathlib.Data.TypeVec
 import Mathlib.Data.TypeVec.Attr
diff --git a/Mathlib/Data/Sym/Basic.lean b/Mathlib/Data/Sym/Basic.lean
new file mode 100644
index 0000000000000..0c055d6808c22
--- /dev/null
+++ b/Mathlib/Data/Sym/Basic.lean
@@ -0,0 +1,681 @@
+/-
+Copyright (c) 2020 Kyle Miller All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+
+! This file was ported from Lean 3 source module data.sym.basic
+! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Multiset.Basic
+import Mathlib.Data.Vector.Basic
+import Mathlib.Data.Setoid.Basic
+import Mathlib.Tactic.ApplyFun
+import Mathlib.Tactic.Lift
+
+/-!
+# Symmetric powers
+
+This file defines symmetric powers of a type.  The nth symmetric power
+consists of homogeneous n-tuples modulo permutations by the symmetric
+group.
+
+The special case of 2-tuples is called the symmetric square, which is
+addressed in more detail in `Data.Sym.Sym2`.
+
+TODO: This was created as supporting material for `Sym2`; it
+needs a fleshed-out interface.
+
+## Tags
+
+symmetric powers
+
+-/
+
+
+open Function
+
+/-- The nth symmetric power is n-tuples up to permutation.  We define it
+as a subtype of `Multiset` since these are well developed in the
+library.  We also give a definition `Sym.sym'` in terms of vectors, and we
+show these are equivalent in `Sym.symEquivSym'`.
+-/
+def Sym (α : Type _) (n : ℕ) :=
+  { s : Multiset α // Multiset.card s = n }
+#align sym Sym
+
+--Porting note: new definition
+/-- The canoncial map to `Multiset α` that forgets that `s` has length `n` -/
+@[coe] def toMultiset {α : Type _} {n : ℕ} (s : Sym α n) : Multiset α :=
+  s.1
+
+instance Sym.hasCoe (α : Type _) (n : ℕ) : CoeOut (Sym α n) (Multiset α) :=
+  ⟨toMultiset⟩
+#align sym.has_coe Sym.hasCoe
+
+/-- This is the `List.Perm` setoid lifted to `Vector`.
+
+See note [reducible non-instances].
+-/
+@[reducible]
+def Vector.Perm.isSetoid (α : Type _) (n : ℕ) : Setoid (Vector α n) :=
+  (List.isSetoid α).comap Subtype.val
+#align vector.perm.is_setoid Vector.Perm.isSetoid
+
+attribute [local instance] Vector.Perm.isSetoid
+
+namespace Sym
+
+variable {α β : Type _} {n n' m : ℕ} {s : Sym α n} {a b : α}
+
+theorem coe_injective : Injective ((↑) : Sym α n → Multiset α) :=
+  Subtype.coe_injective
+#align sym.coe_injective Sym.coe_injective
+
+@[simp, norm_cast]
+theorem coe_inj {s₁ s₂ : Sym α n} : (s₁ : Multiset α) = s₂ ↔ s₁ = s₂ :=
+  coe_injective.eq_iff
+#align sym.coe_inj Sym.coe_inj
+
+--Porting note: new theorem
+@[ext] theorem ext {s₁ s₂ : Sym α n} (h : (s₁ : Multiset α) = ↑s₂) : s₁ = s₂ :=
+  coe_injective h
+
+--Porting note: new theorem
+@[simp]
+theorem val_eq_coe (s : Sym α n) : s.1 = ↑s :=
+  rfl
+
+/-- Construct an element of the `n`th symmetric power from a multiset of cardinality `n`.
+-/
+@[match_pattern] --Porting note: removed `@[simps]`, generated bad lemma
+abbrev mk (m : Multiset α) (h : Multiset.card m = n) : Sym α n :=
+  ⟨m, h⟩
+#align sym.mk Sym.mk
+
+/-- The unique element in `Sym α 0`. -/
+@[match_pattern]
+def nil : Sym α 0 :=
+  ⟨0, Multiset.card_zero⟩
+#align sym.nil Sym.nil
+
+@[simp]
+theorem coe_nil : ↑(@Sym.nil α) = (0 : Multiset α) :=
+  rfl
+#align sym.coe_nil Sym.coe_nil
+
+/-- Inserts an element into the term of `sym α n`, increasing the length by one.
+-/
+@[match_pattern]
+def cons (a : α) (s : Sym α n) : Sym α n.succ :=
+  ⟨a ::ₘ s.1, by rw [Multiset.card_cons, s.2]⟩
+#align sym.cons Sym.cons
+
+@[inherit_doc]
+infixr:67 " ::ₛ " => cons
+
+@[simp]
+theorem cons_inj_right (a : α) (s s' : Sym α n) : a ::ₛ s = a ::ₛ s' ↔ s = s' :=
+  Subtype.ext_iff.trans <| (Multiset.cons_inj_right _).trans Subtype.ext_iff.symm
+#align sym.cons_inj_right Sym.cons_inj_right
+
+@[simp]
+theorem cons_inj_left (a a' : α) (s : Sym α n) : a ::ₛ s = a' ::ₛ s ↔ a = a' :=
+  Subtype.ext_iff.trans <| Multiset.cons_inj_left _
+#align sym.cons_inj_left Sym.cons_inj_left
+
+theorem cons_swap (a b : α) (s : Sym α n) : a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s :=
+  Subtype.ext <| Multiset.cons_swap a b s.1
+#align sym.cons_swap Sym.cons_swap
+
+theorem coe_cons (s : Sym α n) (a : α) : (a ::ₛ s : Multiset α) = a ::ₘ s :=
+  rfl
+#align sym.coe_cons Sym.coe_cons
+
+/-- This is the quotient map that takes a list of n elements as an n-tuple and produces an nth
+symmetric power.
+-/
+def ofVector : Vector α n → Sym α n :=
+  fun x => ⟨↑x.val, (Multiset.coe_card _).trans x.2⟩
+
+/-- This is the quotient map that takes a list of n elements as an n-tuple and produces an nth
+symmetric power.
+-/
+instance : Coe (Vector α n) (Sym α n) where coe x := ofVector x
+
+@[simp]
+theorem of_vector_nil : ↑(Vector.nil : Vector α 0) = (Sym.nil : Sym α 0) :=
+  rfl
+#align sym.of_vector_nil Sym.of_vector_nil
+
+@[simp]
+theorem of_vector_cons (a : α) (v : Vector α n) : ↑(Vector.cons a v) = a ::ₛ (↑v : Sym α n) :=
+  by
+  cases v
+  rfl
+#align sym.of_vector_cons Sym.of_vector_cons
+
+/-- `α ∈ s` means that `a` appears as one of the factors in `s`.
+-/
+instance : Membership α (Sym α n) :=
+  ⟨fun a s => a ∈ s.1⟩
+
+instance decidableMem [DecidableEq α] (a : α) (s : Sym α n) : Decidable (a ∈ s) :=
+  s.1.decidableMem _
+#align sym.decidable_mem Sym.decidableMem
+
+@[simp]
+theorem mem_mk (a : α) (s : Multiset α) (h : Multiset.card s = n) : a ∈ mk s h ↔ a ∈ s :=
+  Iff.rfl
+#align sym.mem_mk Sym.mem_mk
+
+@[simp]
+theorem mem_cons : a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s :=
+  Multiset.mem_cons
+#align sym.mem_cons Sym.mem_cons
+
+@[simp]
+theorem mem_coe : a ∈ (s : Multiset α) ↔ a ∈ s :=
+  Iff.rfl
+#align sym.mem_coe Sym.mem_coe
+
+theorem mem_cons_of_mem (h : a ∈ s) : a ∈ b ::ₛ s :=
+  Multiset.mem_cons_of_mem h
+#align sym.mem_cons_of_mem Sym.mem_cons_of_mem
+
+--@[simp] Porting note: simp can prove it
+theorem mem_cons_self (a : α) (s : Sym α n) : a ∈ a ::ₛ s :=
+  Multiset.mem_cons_self a s.1
+#align sym.mem_cons_self Sym.mem_cons_self
+
+theorem cons_of_coe_eq (a : α) (v : Vector α n) : a ::ₛ (↑v : Sym α n) = ↑(a ::ᵥ v) :=
+  Subtype.ext <| by
+    cases v
+    rfl
+#align sym.cons_of_coe_eq Sym.cons_of_coe_eq
+
+theorem sound {a b : Vector α n} (h : a.val ~ b.val) : (↑a : Sym α n) = ↑b :=
+  Subtype.ext <| Quotient.sound h
+#align sym.sound Sym.sound
+
+/-- `erase s a h` is the sym that subtracts 1 from the
+  multiplicity of `a` if a is present in the sym. -/
+def erase [DecidableEq α] (s : Sym α (n + 1)) (a : α) (h : a ∈ s) : Sym α n :=
+  ⟨s.val.erase a, (Multiset.card_erase_of_mem h).trans <| s.property.symm ▸ n.pred_succ⟩
+#align sym.erase Sym.erase
+
+@[simp]
+theorem erase_mk [DecidableEq α] (m : Multiset α)
+    (hc : Multiset.card m = n + 1) (a : α) (h : a ∈ m) :
+    (mk m hc).erase a h =mk (m.erase a)
+        (by rw [Multiset.card_erase_of_mem h, hc]; rfl) :=
+  rfl
+#align sym.erase_mk Sym.erase_mk
+
+@[simp]
+theorem coe_erase [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) :
+    (s.erase a h : Multiset α) = Multiset.erase s a :=
+  rfl
+#align sym.coe_erase Sym.coe_erase
+
+@[simp]
+theorem cons_erase [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) : a ::ₛ s.erase a h = s :=
+  coe_injective <| Multiset.cons_erase h
+#align sym.cons_erase Sym.cons_erase
+
+@[simp]
+theorem erase_cons_head [DecidableEq α] (s : Sym α n) (a : α)
+    (h : a ∈ a ::ₛ s := mem_cons_self a s) : (a ::ₛ s).erase a h = s :=
+  coe_injective <| Multiset.erase_cons_head a s.1
+#align sym.erase_cons_head Sym.erase_cons_head
+
+/-- Another definition of the nth symmetric power, using vectors modulo permutations. (See `Sym`.)
+-/
+def Sym' (α : Type _) (n : ℕ) :=
+  Quotient (Vector.Perm.isSetoid α n)
+#align sym.sym' Sym.Sym'
+
+/-- This is `cons` but for the alternative `Sym'` definition.
+-/
+def cons' {α : Type _} {n : ℕ} : α → Sym' α n → Sym' α (Nat.succ n) := fun a =>
+  Quotient.map (Vector.cons a) fun ⟨_, _⟩ ⟨_, _⟩ h => List.Perm.cons _ h
+#align sym.cons' Sym.cons'
+
+@[inherit_doc]
+notation a "::" b => cons' a b
+
+/-- Multisets of cardinality n are equivalent to length-n vectors up to permutations.
+-/
+def symEquivSym' {α : Type _} {n : ℕ} : Sym α n ≃ Sym' α n :=
+  Equiv.subtypeQuotientEquivQuotientSubtype _ _ (fun _ => by rfl) fun _ _ => by rfl
+#align sym.sym_equiv_sym' Sym.symEquivSym'
+
+theorem cons_equiv_eq_equiv_cons (α : Type _) (n : ℕ) (a : α) (s : Sym α n) :
+    (a::symEquivSym' s) = symEquivSym' (a ::ₛ s) :=
+  by
+  rcases s with ⟨⟨l⟩, _⟩
+  rfl
+#align sym.cons_equiv_eq_equiv_cons Sym.cons_equiv_eq_equiv_cons
+
+instance : Zero (Sym α 0) :=
+  ⟨⟨0, rfl⟩⟩
+
+instance : EmptyCollection (Sym α 0) :=
+  ⟨0⟩
+
+theorem eq_nil_of_card_zero (s : Sym α 0) : s = nil :=
+  Subtype.ext <| Multiset.card_eq_zero.1 s.2
+#align sym.eq_nil_of_card_zero Sym.eq_nil_of_card_zero
+
+instance uniqueZero : Unique (Sym α 0) :=
+  ⟨⟨nil⟩, eq_nil_of_card_zero⟩
+#align sym.unique_zero Sym.uniqueZero
+
+/-- `replicate n a` is the sym containing only `a` with multiplicity `n`. -/
+def replicate (n : ℕ) (a : α) : Sym α n :=
+  ⟨Multiset.replicate n a, Multiset.card_replicate _ _⟩
+#align sym.replicate Sym.replicate
+
+theorem replicate_succ {a : α} {n : ℕ} : replicate n.succ a = a ::ₛ replicate n a :=
+  rfl
+#align sym.replicate_succ Sym.replicate_succ
+
+theorem coe_replicate : (replicate n a : Multiset α) = Multiset.replicate n a :=
+  rfl
+#align sym.coe_replicate Sym.coe_replicate
+
+@[simp]
+theorem mem_replicate : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a :=
+  Multiset.mem_replicate
+#align sym.mem_replicate Sym.mem_replicate
+
+theorem eq_replicate_iff : s = replicate n a ↔ ∀ b ∈ s, b = a := by
+  erw [Subtype.ext_iff, Multiset.eq_replicate]
+  exact and_iff_right s.2
+#align sym.eq_replicate_iff Sym.eq_replicate_iff
+
+theorem exists_mem (s : Sym α n.succ) : ∃ a, a ∈ s :=
+  Multiset.card_pos_iff_exists_mem.1 <| s.2.symm ▸ n.succ_pos
+#align sym.exists_mem Sym.exists_mem
+
+theorem exists_eq_cons_of_succ (s : Sym α n.succ) : ∃ (a : α)(s' : Sym α n), s = a ::ₛ s' :=
+  by
+  obtain ⟨a, ha⟩ := exists_mem s
+  classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
+#align sym.exists_eq_cons_of_succ Sym.exists_eq_cons_of_succ
+
+theorem eq_replicate {a : α} {n : ℕ} {s : Sym α n} : s = replicate n a ↔ ∀ b ∈ s, b = a :=
+  Subtype.ext_iff.trans <| Multiset.eq_replicate.trans <| and_iff_right s.prop
+#align sym.eq_replicate Sym.eq_replicate
+
+theorem eq_replicate_of_subsingleton [Subsingleton α] (a : α) {n : ℕ} (s : Sym α n) :
+    s = replicate n a :=
+  eq_replicate.2 fun _ _ => Subsingleton.elim _ _
+#align sym.eq_replicate_of_subsingleton Sym.eq_replicate_of_subsingleton
+
+instance [Subsingleton α] (n : ℕ) : Subsingleton (Sym α n) :=
+  ⟨by
+    cases n
+    · simp
+    · intro s s'
+      obtain ⟨b, -⟩ := exists_mem s
+      rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]⟩
+
+instance inhabitedSym [Inhabited α] (n : ℕ) : Inhabited (Sym α n) :=
+  ⟨replicate n default⟩
+#align sym.inhabited_sym Sym.inhabitedSym
+
+instance inhabitedSym' [Inhabited α] (n : ℕ) : Inhabited (Sym' α n) :=
+  ⟨Quotient.mk' (Vector.replicate n default)⟩
+#align sym.inhabited_sym' Sym.inhabitedSym'
+
+instance (n : ℕ) [IsEmpty α] : IsEmpty (Sym α n.succ) :=
+  ⟨fun s => by
+    obtain ⟨a, -⟩ := exists_mem s
+    exact isEmptyElim a⟩
+
+instance (n : ℕ) [Unique α] : Unique (Sym α n) :=
+  Unique.mk' _
+
+theorem replicate_right_inj {a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b :=
+  Subtype.ext_iff.trans (Multiset.replicate_right_inj h)
+#align sym.replicate_right_inj Sym.replicate_right_inj
+
+theorem replicate_right_injective {n : ℕ} (h : n ≠ 0) :
+    Function.Injective (replicate n : α → Sym α n) := fun _ _ => (replicate_right_inj h).1
+#align sym.replicate_right_injective Sym.replicate_right_injective
+
+instance (n : ℕ) [Nontrivial α] : Nontrivial (Sym α (n + 1)) :=
+  (replicate_right_injective n.succ_ne_zero).nontrivial
+
+/-- A function `α → β` induces a function `sym α n → sym β n` by applying it to every element of
+the underlying `n`-tuple. -/
+def map {n : ℕ} (f : α → β) (x : Sym α n) : Sym β n :=
+  ⟨x.val.map f, by simpa [Multiset.card_map] using x.property⟩
+#align sym.map Sym.map
+
+@[simp]
+theorem mem_map {n : ℕ} {f : α → β} {b : β} {l : Sym α n} :
+    b ∈ Sym.map f l ↔ ∃ a, a ∈ l ∧ f a = b :=
+  Multiset.mem_map
+#align sym.mem_map Sym.mem_map
+
+/-- Note: `sym.map_id` is not simp-normal, as simp ends up unfolding `id` with `sym.map_congr` -/
+@[simp]
+theorem map_id' {α : Type _} {n : ℕ} (s : Sym α n) : Sym.map (fun x : α => x) s = s := by
+  ext; simp [Sym.map]; rfl
+#align sym.map_id' Sym.map_id'
+
+theorem map_id {α : Type _} {n : ℕ} (s : Sym α n) : Sym.map id s = s := by
+  ext; simp [Sym.map]; rfl
+#align sym.map_id Sym.map_id
+
+@[simp]
+theorem map_map {α β γ : Type _} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n) :
+    Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s :=
+  Subtype.ext <| by dsimp only [Sym.map]; simp
+#align sym.map_map Sym.map_map
+
+@[simp]
+theorem map_zero (f : α → β) : Sym.map f (0 : Sym α 0) = (0 : Sym β 0) :=
+  rfl
+#align sym.map_zero Sym.map_zero
+
+@[simp]
+theorem map_cons {n : ℕ} (f : α → β) (a : α) (s : Sym α n) : (a ::ₛ s).map f = f a ::ₛ s.map f :=
+  ext <| Multiset.map_cons _ _ _
+#align sym.map_cons Sym.map_cons
+
+@[congr]
+theorem map_congr {f g : α → β} {s : Sym α n} (h : ∀ x ∈ s, f x = g x) : map f s = map g s :=
+  Subtype.ext <| Multiset.map_congr rfl h
+#align sym.map_congr Sym.map_congr
+
+@[simp]
+theorem map_mk {f : α → β} {m : Multiset α} {hc : Multiset.card m = n} :
+    map f (mk m hc) = mk (m.map f) (by simp [hc]) :=
+  rfl
+#align sym.map_mk Sym.map_mk
+
+@[simp]
+theorem coe_map (s : Sym α n) (f : α → β) : ↑(s.map f) = Multiset.map f s :=
+  rfl
+#align sym.coe_map Sym.coe_map
+
+theorem map_injective {f : α → β} (hf : Injective f) (n : ℕ) :
+    Injective (map f : Sym α n → Sym β n) := fun _ _ h =>
+  coe_injective <| Multiset.map_injective hf <| coe_inj.2 h
+#align sym.map_injective Sym.map_injective
+
+/-- Mapping an equivalence `α ≃ β` using `Sym.map` gives an equivalence between `Sym α n` and
+`Sym β n`. -/
+@[simps]
+def equivCongr (e : α ≃ β) : Sym α n ≃ Sym β n
+    where
+  toFun := map e
+  invFun := map e.symm
+  left_inv x := by rw [map_map, Equiv.symm_comp_self, map_id]
+  right_inv x := by rw [map_map, Equiv.self_comp_symm, map_id]
+#align sym.equiv_congr Sym.equivCongr
+
+/-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce
+an element of the symmetric power on `{x // x ∈ s}`. -/
+def attach (s : Sym α n) : Sym { x // x ∈ s } n :=
+  ⟨s.val.attach, by conv_rhs => rw [← s.2, ← Multiset.card_attach]⟩
+#align sym.attach Sym.attach
+
+@[simp]
+theorem attach_mk {m : Multiset α} {hc : Multiset.card m = n} :
+    attach (mk m hc) = mk m.attach (Multiset.card_attach.trans hc) :=
+  rfl
+#align sym.attach_mk Sym.attach_mk
+
+@[simp]
+theorem coe_attach (s : Sym α n) : (s.attach : Multiset { a // a ∈ s }) =
+    Multiset.attach (s : Multiset α) :=
+  rfl
+#align sym.coe_attach Sym.coe_attach
+
+theorem attach_map_coe (s : Sym α n) : s.attach.map (↑) = s :=
+  coe_injective <| Multiset.attach_map_val _
+#align sym.attach_map_coe Sym.attach_map_coe
+
+@[simp]
+theorem mem_attach (s : Sym α n) (x : { x // x ∈ s }) : x ∈ s.attach :=
+  Multiset.mem_attach _ _
+#align sym.mem_attach Sym.mem_attach
+
+@[simp]
+theorem attach_nil : (nil : Sym α 0).attach = nil :=
+  rfl
+#align sym.attach_nil Sym.attach_nil
+
+@[simp]
+theorem attach_cons (x : α) (s : Sym α n) :
+    (cons x s).attach =
+      cons ⟨x, mem_cons_self _ _⟩ (s.attach.map fun x => ⟨x, mem_cons_of_mem x.prop⟩) :=
+  coe_injective <| Multiset.attach_cons _ _
+#align sym.attach_cons Sym.attach_cons
+
+/-- Change the length of a `Sym` using an equality.
+The simp-normal form is for the `cast` to be pushed outward. -/
+protected def cast {n m : ℕ} (h : n = m) : Sym α n ≃ Sym α m
+    where
+  toFun s := ⟨s.val, s.2.trans h⟩
+  invFun s := ⟨s.val, s.2.trans h.symm⟩
+  left_inv _ := Subtype.ext rfl
+  right_inv _ := Subtype.ext rfl
+#align sym.cast Sym.cast
+
+@[simp]
+theorem cast_rfl : Sym.cast rfl s = s :=
+  Subtype.ext rfl
+#align sym.cast_rfl Sym.cast_rfl
+
+@[simp]
+theorem cast_cast {n'' : ℕ} (h : n = n') (h' : n' = n'') :
+    Sym.cast h' (Sym.cast h s) = Sym.cast (h.trans h') s :=
+  rfl
+#align sym.cast_cast Sym.cast_cast
+
+@[simp]
+theorem coe_cast (h : n = m) : (Sym.cast h s : Multiset α) = s :=
+  rfl
+#align sym.coe_cast Sym.coe_cast
+
+@[simp]
+theorem mem_cast (h : n = m) : a ∈ Sym.cast h s ↔ a ∈ s :=
+  Iff.rfl
+#align sym.mem_cast Sym.mem_cast
+
+/-- Append a pair of `sym` terms. -/
+def append (s : Sym α n) (s' : Sym α n') : Sym α (n + n') :=
+  ⟨s.1 + s'.1, by rw [map_add, s.2, s'.2]⟩
+#align sym.append Sym.append
+
+@[simp]
+theorem append_inj_right (s : Sym α n) {t t' : Sym α n'} : s.append t = s.append t' ↔ t = t' :=
+  Subtype.ext_iff.trans <| (add_right_inj _).trans Subtype.ext_iff.symm
+#align sym.append_inj_right Sym.append_inj_right
+
+@[simp]
+theorem append_inj_left {s s' : Sym α n} (t : Sym α n') : s.append t = s'.append t ↔ s = s' :=
+  Subtype.ext_iff.trans <| (add_left_inj _).trans Subtype.ext_iff.symm
+#align sym.append_inj_left Sym.append_inj_left
+
+theorem append_comm (s : Sym α n') (s' : Sym α n') :
+    s.append s' = Sym.cast (add_comm _ _) (s'.append s) := by
+  ext
+  simp [append, add_comm]
+#align sym.append_comm Sym.append_comm
+
+@[simp, norm_cast]
+theorem coe_append (s : Sym α n) (s' : Sym α n') : (s.append s' : Multiset α) = s + s' :=
+  rfl
+#align sym.coe_append Sym.coe_append
+
+theorem mem_append_iff {s' : Sym α m} : a ∈ s.append s' ↔ a ∈ s ∨ a ∈ s' :=
+  Multiset.mem_add
+#align sym.mem_append_iff Sym.mem_append_iff
+
+/-- 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`. -/
+def fill (a : α) (i : Fin (n + 1)) (m : Sym α (n - i)) : Sym α n :=
+  Sym.cast (Nat.sub_add_cancel i.is_le) (m.append (replicate i a))
+#align sym.fill Sym.fill
+
+theorem coe_fill {a : α} {i : Fin (n + 1)} {m : Sym α (n - i)} :
+    (fill a i m : Multiset α) = m + replicate i a :=
+  rfl
+#align sym.coe_fill Sym.coe_fill
+
+theorem mem_fill_iff {a b : α} {i : Fin (n + 1)} {s : Sym α (n - i)} :
+    a ∈ Sym.fill b i s ↔ (i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s := by
+  rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
+#align sym.mem_fill_iff Sym.mem_fill_iff
+
+open Multiset
+
+/-- Remove every `a` from a given `Sym α n`.
+Yields the number of copies `i` and a term of `Sym α (n - i)`. -/
+def filterNe [DecidableEq α] (a : α) (m : Sym α n) : Σi : Fin (n + 1), Sym α (n - i) :=
+  ⟨⟨m.1.count a, (count_le_card _ _).trans_lt <| by rw [m.2, Nat.lt_succ_iff]⟩,
+    m.1.filter ((· ≠ ·) a),
+    eq_tsub_of_add_eq <|
+      Eq.trans
+        (by
+          rw [← countp_eq_card_filter, add_comm]
+          simp only [eq_comm, Ne.def, count]
+          rw [← card_eq_countp_add_countp _ _])
+        m.2⟩
+#align sym.filter_ne Sym.filterNe
+
+theorem sigma_sub_ext {m₁ m₂ : Σi : Fin (n + 1), Sym α (n - i)} (h : (m₁.2 : Multiset α) = m₂.2) :
+    m₁ = m₂ :=
+  Sigma.subtype_ext
+    (Fin.ext <| by
+      rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
+        ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)])
+    h
+#align sym.sigma_sub_ext Sym.sigma_sub_ext
+
+theorem fill_filterNe [DecidableEq α] (a : α) (m : Sym α n) :
+    (m.filterNe a).2.fill a (m.filterNe a).1 = m :=
+  Sym.ext
+    (by
+      rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
+      ext b; dsimp
+      rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
+      obtain rfl | h := eq_or_ne a b
+      · rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
+      · rw [if_pos h, if_neg h.symm, add_zero])
+#align sym.fill_filter_ne Sym.fill_filterNe
+
+theorem filter_ne_fill [DecidableEq α] (a : α) (m : Σi : Fin (n + 1), Sym α (n - i)) (h : a ∉ m.2) :
+    (m.2.fill a m.1).filterNe a = m :=
+  sigma_sub_ext
+    (by
+      rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
+      rw [filter_add, filter_eq_self.2, add_right_eq_self, eq_zero_iff_forall_not_mem]
+      · intro b hb
+        rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
+        exact hb.2 hb.1.2.symm
+      · exact fun a ha ha' => h <| ha'.symm ▸ ha)
+#align sym.filter_ne_fill Sym.filter_ne_fill
+
+end Sym
+
+section Equiv
+
+/-! ### Combinatorial equivalences -/
+
+
+variable {α : Type _} {n : ℕ}
+
+open Sym
+
+namespace SymOptionSuccEquiv
+
+/-- Function from the symmetric product over `Option` splitting on whether or not
+it contains a `none`. -/
+def encode [DecidableEq α] (s : Sym (Option α) n.succ) : Sum (Sym (Option α) n) (Sym α n.succ) :=
+  if h : none ∈ s then Sum.inl (s.erase none h)
+  else
+    Sum.inr
+      (s.attach.map fun o =>
+        o.1.get <| Option.ne_none_iff_isSome.1 <| ne_of_mem_of_not_mem o.2 h)
+#align sym_option_succ_equiv.encode SymOptionSuccEquiv.encode
+
+@[simp]
+theorem encode_of_none_mem [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∈ s) :
+    encode s = Sum.inl (s.erase none h) :=
+  dif_pos h
+#align sym_option_succ_equiv.encode_of_none_mem SymOptionSuccEquiv.encode_of_none_mem
+
+@[simp]
+theorem encode_of_not_none_mem [DecidableEq α] (s : Sym (Option α) n.succ) (h : ¬none ∈ s) :
+    encode s =
+      Sum.inr
+        (s.attach.map fun o =>
+          o.1.get <| Option.ne_none_iff_isSome.1 <| ne_of_mem_of_not_mem o.2 h) :=
+  dif_neg h
+#align sym_option_succ_equiv.encode_of_not_none_mem SymOptionSuccEquiv.encode_of_not_none_mem
+
+/-- Inverse of `Sym_option_succ_equiv.decode`. -/
+-- @[simp] Porting note: not a nice simp lemma, applies too often in LEan4
+def decode : Sum (Sym (Option α) n) (Sym α n.succ) → Sym (Option α) n.succ
+  | Sum.inl s => none ::ₛ s
+  | Sum.inr s => s.map Embedding.some
+#align sym_option_succ_equiv.decode SymOptionSuccEquiv.decode
+
+-- Porting note: new theorem
+@[simp]
+theorem decode_inl (s : Sym (Option α) n) : decode (Sum.inl s) = none ::ₛ s :=
+  rfl
+
+--Porting note: new theorem
+@[simp]
+theorem decode_inr (s : Sym α n.succ) : decode (Sum.inr s) = s.map Embedding.some :=
+  rfl
+
+@[simp]
+theorem decode_encode [DecidableEq α] (s : Sym (Option α) n.succ) : decode (encode s) = s :=
+  by
+  by_cases h : none ∈ s
+  · simp [h]
+  · simp only [decode, h, not_false_iff, encode_of_not_none_mem, Embedding.some_apply, map_map,
+      comp_apply, Option.some_get]
+    convert s.attach_map_coe
+#align sym_option_succ_equiv.decode_encode SymOptionSuccEquiv.decode_encode
+
+@[simp]
+theorem encode_decode [DecidableEq α] (s : Sum (Sym (Option α) n) (Sym α n.succ)) :
+    encode (decode s) = s := by
+  obtain s | s := s
+  · simp
+  · unfold SymOptionSuccEquiv.encode
+    split_ifs with h
+    · obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
+      exact Option.some_ne_none _ ha
+    · refine' congr_arg Sum.inr _
+      refine' map_injective (Option.some_injective _) _ _
+      refine' Eq.trans _ (Eq.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe _)
+      simp; simp
+#align sym_option_succ_equiv.encode_decode SymOptionSuccEquiv.encode_decode
+
+end SymOptionSuccEquiv
+
+/-- The symmetric product over `Option` is a disjoint union over simpler symmetric products. -/
+--@[simps]
+def symOptionSuccEquiv [DecidableEq α] :
+    Sym (Option α) n.succ ≃ Sum (Sym (Option α) n) (Sym α n.succ)
+    where
+  toFun := SymOptionSuccEquiv.encode
+  invFun := SymOptionSuccEquiv.decode
+  left_inv := SymOptionSuccEquiv.decode_encode
+  right_inv := SymOptionSuccEquiv.encode_decode
+#align sym_option_succ_equiv symOptionSuccEquiv
+
+end Equiv