From 51f96bb7df0e3744b70f94c3645cec8f5a63f33b Mon Sep 17 00:00:00 2001
From: "Anne C.A. Baanen" <vierkantor@vierkantor.com>
Date: Mon, 3 Mar 2025 16:26:11 +0100
Subject: [PATCH 1/2] chore(Data/Multiset): redistribute `Nodup` material

Now that `Multiset.Nodup` lives in `Multiset/Defs.lean`, all the material on `Nodup` in `Nodup.lean` can be upstreamed to other files in the `Multiset` folder. We are left with `Pairwise.forall` which doesn't mention `Nodup` at all, so I renamed the file to `Pairwise.lean`. (Note that Git decided it is a deletion + addition, not a rename...)
---
 Mathlib.lean                          |   2 +-
 Mathlib/Data/Finset/Attach.lean       |   2 +-
 Mathlib/Data/Finset/Empty.lean        |   2 +-
 Mathlib/Data/Finset/Erase.lean        |   2 +-
 Mathlib/Data/Finset/Filter.lean       |   1 +
 Mathlib/Data/Multiset/AddSub.lean     |  23 +++
 Mathlib/Data/Multiset/Count.lean      |  25 ++++
 Mathlib/Data/Multiset/Dedup.lean      |   2 +-
 Mathlib/Data/Multiset/Defs.lean       |   6 +
 Mathlib/Data/Multiset/Filter.lean     |  25 ++++
 Mathlib/Data/Multiset/MapFold.lean    |  55 +++++++
 Mathlib/Data/Multiset/Nodup.lean      | 200 --------------------------
 Mathlib/Data/Multiset/Pairwise.lean   |  18 +++
 Mathlib/Data/Multiset/Powerset.lean   |   1 +
 Mathlib/Data/Multiset/Range.lean      |  10 ++
 Mathlib/Data/Multiset/Replicate.lean  |  22 +++
 Mathlib/Data/Multiset/Sum.lean        |   1 -
 Mathlib/Data/Multiset/UnionInter.lean |  25 ++++
 Mathlib/Data/Multiset/ZeroCons.lean   |  23 +++
 19 files changed, 239 insertions(+), 206 deletions(-)
 delete mode 100644 Mathlib/Data/Multiset/Nodup.lean
 create mode 100644 Mathlib/Data/Multiset/Pairwise.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 9714609cd19dce..c937d28143bb66 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2966,8 +2966,8 @@ import Mathlib.Data.Multiset.Interval
 import Mathlib.Data.Multiset.Lattice
 import Mathlib.Data.Multiset.MapFold
 import Mathlib.Data.Multiset.NatAntidiagonal
-import Mathlib.Data.Multiset.Nodup
 import Mathlib.Data.Multiset.OrderedMonoid
+import Mathlib.Data.Multiset.Pairwise
 import Mathlib.Data.Multiset.Pi
 import Mathlib.Data.Multiset.Powerset
 import Mathlib.Data.Multiset.Range
diff --git a/Mathlib/Data/Finset/Attach.lean b/Mathlib/Data/Finset/Attach.lean
index a4c0208e2e1e5a..74e8de5c5fb102 100644
--- a/Mathlib/Data/Finset/Attach.lean
+++ b/Mathlib/Data/Finset/Attach.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Defs
-import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.MapFold
 
 /-!
 # Attaching a proof of membership to a finite set
diff --git a/Mathlib/Data/Finset/Empty.lean b/Mathlib/Data/Finset/Empty.lean
index 71e06d44e33e4c..fb9eebf4dda892 100644
--- a/Mathlib/Data/Finset/Empty.lean
+++ b/Mathlib/Data/Finset/Empty.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Defs
-import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.ZeroCons
 
 /-!
 # Empty and nonempty finite sets
diff --git a/Mathlib/Data/Finset/Erase.lean b/Mathlib/Data/Finset/Erase.lean
index def5fbbebaecb6..7b93b125a4e12c 100644
--- a/Mathlib/Data/Finset/Erase.lean
+++ b/Mathlib/Data/Finset/Erase.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Defs
-import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.Filter
 
 /-!
 # Erasing an element from a finite set
diff --git a/Mathlib/Data/Finset/Filter.lean b/Mathlib/Data/Finset/Filter.lean
index 9208749635987b..42c809eeac98c1 100644
--- a/Mathlib/Data/Finset/Filter.lean
+++ b/Mathlib/Data/Finset/Filter.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Empty
+import Mathlib.Data.Multiset.Filter
 
 /-!
 # Filtering a finite set
diff --git a/Mathlib/Data/Multiset/AddSub.lean b/Mathlib/Data/Multiset/AddSub.lean
index 86f0aa0ff65bc4..6ddd84d635633d 100644
--- a/Mathlib/Data/Multiset/AddSub.lean
+++ b/Mathlib/Data/Multiset/AddSub.lean
@@ -390,4 +390,27 @@ theorem rel_add_right {as bs₀ bs₁} :
 
 end Rel
 
+section Nodup
+
+@[simp]
+theorem nodup_singleton : ∀ a : α, Nodup ({a} : Multiset α) :=
+  List.nodup_singleton
+
+theorem not_nodup_pair : ∀ a : α, ¬Nodup (a ::ₘ a ::ₘ 0) :=
+  List.not_nodup_pair
+
+theorem Nodup.erase [DecidableEq α] (a : α) {l} : Nodup l → Nodup (l.erase a) :=
+  nodup_of_le (erase_le _ _)
+
+theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) :
+    a ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
+  ⟨fun h =>
+    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' => by
+      refine count_eq_zero.1 ?_ h
+      rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
+      exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
+    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/Count.lean b/Mathlib/Data/Multiset/Count.lean
index a96f8fe6b2d8b3..fe760cf5dec703 100644
--- a/Mathlib/Data/Multiset/Count.lean
+++ b/Mathlib/Data/Multiset/Count.lean
@@ -217,4 +217,29 @@ theorem Rel.countP_eq (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t
 
 end Rel
 
+section Nodup
+
+variable {s : Multiset α} {a : α}
+
+theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1 :=
+  Quot.induction_on s fun _l => by
+    simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
+    exact List.nodup_iff_count_le_one
+
+theorem nodup_iff_count_eq_one [DecidableEq α] : Nodup s ↔ ∀ a ∈ s, count a s = 1 :=
+  Quot.induction_on s fun _l => by simpa using List.nodup_iff_count_eq_one
+
+@[simp]
+theorem count_eq_one_of_mem [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) (h : a ∈ s) :
+    count a s = 1 :=
+  nodup_iff_count_eq_one.mp d a h
+
+theorem count_eq_of_nodup [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) :
+    count a s = if a ∈ s then 1 else 0 := by
+  split_ifs with h
+  · exact count_eq_one_of_mem d h
+  · exact count_eq_zero_of_not_mem h
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/Dedup.lean b/Mathlib/Data/Multiset/Dedup.lean
index 07c9eabf1192c7..78597216551a62 100644
--- a/Mathlib/Data/Multiset/Dedup.lean
+++ b/Mathlib/Data/Multiset/Dedup.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.List.Dedup
-import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.UnionInter
 
 /-!
 # Erasing duplicates in a multiset.
diff --git a/Mathlib/Data/Multiset/Defs.lean b/Mathlib/Data/Multiset/Defs.lean
index e705c9366379ec..b57ec37bdba6a0 100644
--- a/Mathlib/Data/Multiset/Defs.lean
+++ b/Mathlib/Data/Multiset/Defs.lean
@@ -356,6 +356,12 @@ theorem Nodup.ext {s t : Multiset α} : Nodup s → Nodup t → (s = t ↔ ∀ a
 theorem le_iff_subset {s t : Multiset α} : Nodup s → (s ≤ t ↔ s ⊆ t) :=
   Quotient.inductionOn₂ s t fun _ _ d => ⟨subset_of_le, d.subperm⟩
 
+theorem nodup_of_le {s t : Multiset α} (h : s ≤ t) : Nodup t → Nodup s :=
+  Multiset.leInductionOn h fun {_ _} => Nodup.sublist
+
+instance nodupDecidable [DecidableEq α] (s : Multiset α) : Decidable (Nodup s) :=
+  Quotient.recOnSubsingleton s fun l => l.nodupDecidable
+
 end Nodup
 
 section SizeOf
diff --git a/Mathlib/Data/Multiset/Filter.lean b/Mathlib/Data/Multiset/Filter.lean
index 938c6f29b389ee..6ca8301e3b57b9 100644
--- a/Mathlib/Data/Multiset/Filter.lean
+++ b/Mathlib/Data/Multiset/Filter.lean
@@ -400,4 +400,29 @@ lemma filter_attach' (s : Multiset α) (p : {a // a ∈ s} → Prop) [DecidableE
 
 end Map
 
+section Nodup
+
+variable {s : Multiset α}
+
+theorem Nodup.filter (p : α → Prop) [DecidablePred p] {s} : Nodup s → Nodup (filter p s) :=
+  Quot.induction_on s fun _ => List.Nodup.filter (p ·)
+
+theorem Nodup.erase_eq_filter [DecidableEq α] (a : α) {s} :
+    Nodup s → s.erase a = Multiset.filter (· ≠ a) s :=
+  Quot.induction_on s fun _ d =>
+    congr_arg ((↑) : List α → Multiset α) <| by simpa using List.Nodup.erase_eq_filter d a
+
+protected theorem Nodup.filterMap (f : α → Option β) (H : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
+    Nodup s → Nodup (filterMap f s) :=
+  Quot.induction_on s fun _ => List.Nodup.filterMap H
+
+theorem Nodup.mem_erase_iff [DecidableEq α] {a b : α} {l} (d : Nodup l) :
+    a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
+  rw [d.erase_eq_filter b, mem_filter, and_comm]
+
+theorem Nodup.not_mem_erase [DecidableEq α] {a : α} {s} (h : Nodup s) : a ∉ s.erase a := fun ha =>
+  (h.mem_erase_iff.1 ha).1 rfl
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/MapFold.lean b/Mathlib/Data/Multiset/MapFold.lean
index ea487bfb1d138f..4e78366de8a497 100644
--- a/Mathlib/Data/Multiset/MapFold.lean
+++ b/Mathlib/Data/Multiset/MapFold.lean
@@ -423,4 +423,59 @@ theorem induction_on_multiset_quot {r : α → α → Prop} {p : Multiset (Quot
 
 end Quot
 
+section Nodup
+
+variable {s : Multiset α}
+
+theorem Nodup.of_map (f : α → β) : Nodup (map f s) → Nodup s :=
+  Quot.induction_on s fun _ => List.Nodup.of_map f
+
+theorem Nodup.map_on {f : α → β} :
+    (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Nodup s → Nodup (map f s) :=
+  Quot.induction_on s fun _ => List.Nodup.map_on
+
+theorem Nodup.map {f : α → β} {s : Multiset α} (hf : Injective f) : Nodup s → Nodup (map f s) :=
+  Nodup.map_on fun _ _ _ _ h => hf h
+
+theorem nodup_map_iff_of_inj_on {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) :
+    Nodup (map f s) ↔ Nodup s :=
+  ⟨Nodup.of_map _, fun h => h.map_on d⟩
+
+theorem nodup_map_iff_of_injective {f : α → β} (d : Function.Injective f) :
+    Nodup (map f s) ↔ Nodup s :=
+  ⟨Nodup.of_map _, fun h => h.map d⟩
+
+theorem inj_on_of_nodup_map {f : α → β} {s : Multiset α} :
+    Nodup (map f s) → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
+  Quot.induction_on s fun _ => List.inj_on_of_nodup_map
+
+theorem nodup_map_iff_inj_on {f : α → β} {s : Multiset α} (d : Nodup s) :
+    Nodup (map f s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
+  ⟨inj_on_of_nodup_map, fun h => d.map_on h⟩
+
+theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H}
+    (hf : ∀ a ha b hb, f a ha = f b hb → a = b) : Nodup s → Nodup (pmap f s H) :=
+  Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H
+
+@[simp]
+theorem nodup_attach {s : Multiset α} : Nodup (attach s) ↔ Nodup s :=
+  Quot.induction_on s fun _ => List.nodup_attach
+
+protected alias ⟨_, Nodup.attach⟩ := nodup_attach
+
+theorem map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β}
+    (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)
+    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
+    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : s.map f = t.map g := by
+  have : t = s.attach.map fun x => i x.1 x.2 := by
+    rw [ht.ext]
+    · aesop
+    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
+  calc
+    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
+    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
+    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/Nodup.lean b/Mathlib/Data/Multiset/Nodup.lean
deleted file mode 100644
index be2c1941691ce1..00000000000000
--- a/Mathlib/Data/Multiset/Nodup.lean
+++ /dev/null
@@ -1,200 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Mathlib.Data.Multiset.Range
-import Mathlib.Data.List.Pairwise
-
-/-!
-# The `Nodup` predicate for multisets without duplicate elements.
-
-## TODO
-
-Many of the results in this file can be upstreamed to an earlier file.
--/
-
-assert_not_exists Monoid
-
-namespace Multiset
-
-open Function List
-
-variable {α β γ : Type*} {r : α → α → Prop} {s t : Multiset α} {a : α}
-
-@[simp]
-theorem nodup_zero : @Nodup α 0 :=
-  Pairwise.nil
-
-@[simp]
-theorem nodup_cons {a : α} {s : Multiset α} : Nodup (a ::ₘ s) ↔ a ∉ s ∧ Nodup s :=
-  Quot.induction_on s fun _ => List.nodup_cons
-
-theorem Nodup.cons (m : a ∉ s) (n : Nodup s) : Nodup (a ::ₘ s) :=
-  nodup_cons.2 ⟨m, n⟩
-
-@[simp]
-theorem nodup_singleton : ∀ a : α, Nodup ({a} : Multiset α) :=
-  List.nodup_singleton
-
-theorem Nodup.of_cons (h : Nodup (a ::ₘ s)) : Nodup s :=
-  (nodup_cons.1 h).2
-
-theorem Nodup.not_mem (h : Nodup (a ::ₘ s)) : a ∉ s :=
-  (nodup_cons.1 h).1
-
-theorem nodup_of_le {s t : Multiset α} (h : s ≤ t) : Nodup t → Nodup s :=
-  Multiset.leInductionOn h fun {_ _} => Nodup.sublist
-
-theorem not_nodup_pair : ∀ a : α, ¬Nodup (a ::ₘ a ::ₘ 0) :=
-  List.not_nodup_pair
-
-theorem nodup_iff_le {s : Multiset α} : Nodup s ↔ ∀ a : α, ¬a ::ₘ a ::ₘ 0 ≤ s :=
-  Quot.induction_on s fun _ =>
-    nodup_iff_sublist.trans <| forall_congr' fun a => not_congr (@replicate_le_coe _ a 2 _).symm
-
-theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t :=
-  nodup_iff_le.trans
-    ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
-      let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
-      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩
-
-theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1 :=
-  Quot.induction_on s fun _l => by
-    simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
-    exact List.nodup_iff_count_le_one
-
-theorem nodup_iff_count_eq_one [DecidableEq α] : Nodup s ↔ ∀ a ∈ s, count a s = 1 :=
-  Quot.induction_on s fun _l => by simpa using List.nodup_iff_count_eq_one
-
-@[simp]
-theorem count_eq_one_of_mem [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) (h : a ∈ s) :
-    count a s = 1 :=
-  nodup_iff_count_eq_one.mp d a h
-
-theorem count_eq_of_nodup [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) :
-    count a s = if a ∈ s then 1 else 0 := by
-  split_ifs with h
-  · exact count_eq_one_of_mem d h
-  · exact count_eq_zero_of_not_mem h
-
-theorem nodup_iff_pairwise {α} {s : Multiset α} : Nodup s ↔ Pairwise (· ≠ ·) s :=
-  Quotient.inductionOn s fun _ => (pairwise_coe_iff_pairwise fun _ _ => Ne.symm).symm
-
-protected theorem Nodup.pairwise : (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → Nodup s → Pairwise r s :=
-  Quotient.inductionOn s fun l h hl => ⟨l, rfl, hl.imp_of_mem fun {a b} ha hb => h a ha b hb⟩
-
-theorem Pairwise.forall (H : Symmetric r) (hs : Pairwise r s) :
-    ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ≠ b → r a b :=
-  let ⟨_, hl₁, hl₂⟩ := hs
-  hl₁.symm ▸ hl₂.forall H
-
-theorem nodup_add {s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
-  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append]
-
-theorem disjoint_of_nodup_add {s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t :=
-  (nodup_add.1 d).2.2
-
-theorem Nodup.add_iff (d₁ : Nodup s) (d₂ : Nodup t) : Nodup (s + t) ↔ Disjoint s t := by
-  simp [nodup_add, d₁, d₂]
-
-theorem Nodup.of_map (f : α → β) : Nodup (map f s) → Nodup s :=
-  Quot.induction_on s fun _ => List.Nodup.of_map f
-
-theorem Nodup.map_on {f : α → β} :
-    (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Nodup s → Nodup (map f s) :=
-  Quot.induction_on s fun _ => List.Nodup.map_on
-
-theorem Nodup.map {f : α → β} {s : Multiset α} (hf : Injective f) : Nodup s → Nodup (map f s) :=
-  Nodup.map_on fun _ _ _ _ h => hf h
-
-theorem nodup_map_iff_of_inj_on {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) :
-    Nodup (map f s) ↔ Nodup s :=
-  ⟨Nodup.of_map _, fun h => h.map_on d⟩
-
-theorem nodup_map_iff_of_injective {f : α → β} (d : Function.Injective f) :
-    Nodup (map f s) ↔ Nodup s :=
-  ⟨Nodup.of_map _, fun h => h.map d⟩
-
-theorem inj_on_of_nodup_map {f : α → β} {s : Multiset α} :
-    Nodup (map f s) → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
-  Quot.induction_on s fun _ => List.inj_on_of_nodup_map
-
-theorem nodup_map_iff_inj_on {f : α → β} {s : Multiset α} (d : Nodup s) :
-    Nodup (map f s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
-  ⟨inj_on_of_nodup_map, fun h => d.map_on h⟩
-
-theorem Nodup.filter (p : α → Prop) [DecidablePred p] {s} : Nodup s → Nodup (filter p s) :=
-  Quot.induction_on s fun _ => List.Nodup.filter (p ·)
-
-@[simp]
-theorem nodup_attach {s : Multiset α} : Nodup (attach s) ↔ Nodup s :=
-  Quot.induction_on s fun _ => List.nodup_attach
-
-protected alias ⟨_, Nodup.attach⟩ := nodup_attach
-
-theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H}
-    (hf : ∀ a ha b hb, f a ha = f b hb → a = b) : Nodup s → Nodup (pmap f s H) :=
-  Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H
-
-instance nodupDecidable [DecidableEq α] (s : Multiset α) : Decidable (Nodup s) :=
-  Quotient.recOnSubsingleton s fun l => l.nodupDecidable
-
-theorem Nodup.erase_eq_filter [DecidableEq α] (a : α) {s} :
-    Nodup s → s.erase a = Multiset.filter (· ≠ a) s :=
-  Quot.induction_on s fun _ d =>
-    congr_arg ((↑) : List α → Multiset α) <| by simpa using List.Nodup.erase_eq_filter d a
-
-theorem Nodup.erase [DecidableEq α] (a : α) {l} : Nodup l → Nodup (l.erase a) :=
-  nodup_of_le (erase_le _ _)
-
-theorem Nodup.mem_erase_iff [DecidableEq α] {a b : α} {l} (d : Nodup l) :
-    a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
-  rw [d.erase_eq_filter b, mem_filter, and_comm]
-
-theorem Nodup.not_mem_erase [DecidableEq α] {a : α} {s} (h : Nodup s) : a ∉ s.erase a := fun ha =>
-  (h.mem_erase_iff.1 ha).1 rfl
-
-protected theorem Nodup.filterMap (f : α → Option β) (H : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
-    Nodup s → Nodup (filterMap f s) :=
-  Quot.induction_on s fun _ => List.Nodup.filterMap H
-
-theorem nodup_range (n : ℕ) : Nodup (range n) :=
-  List.nodup_range _
-
-lemma Nodup.inter_left [DecidableEq α] (t) : Nodup s → Nodup (s ∩ t) := nodup_of_le inter_le_left
-lemma Nodup.inter_right [DecidableEq α] (s) : Nodup t → Nodup (s ∩ t) := nodup_of_le inter_le_right
-
-@[simp]
-theorem nodup_union [DecidableEq α] {s t : Multiset α} : Nodup (s ∪ t) ↔ Nodup s ∧ Nodup t :=
-  ⟨fun h => ⟨nodup_of_le le_union_left h, nodup_of_le le_union_right h⟩, fun ⟨h₁, h₂⟩ =>
-    nodup_iff_count_le_one.2 fun a => by
-      rw [count_union]
-      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)⟩
-
-theorem range_le {m n : ℕ} : range m ≤ range n ↔ m ≤ n :=
-  (le_iff_subset (nodup_range _)).trans range_subset
-
-theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) :
-    a ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
-  ⟨fun h =>
-    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' => by
-      refine count_eq_zero.1 ?_ h
-      rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
-      exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
-    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩
-
-theorem map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β}
-    (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)
-    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : s.map f = t.map g := by
-  have : t = s.attach.map fun x => i x.1 x.2 := by
-    rw [ht.ext]
-    · aesop
-    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
-  calc
-    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
-    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
-    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _
-
-end Multiset
diff --git a/Mathlib/Data/Multiset/Pairwise.lean b/Mathlib/Data/Multiset/Pairwise.lean
new file mode 100644
index 00000000000000..95d8c1415b6f70
--- /dev/null
+++ b/Mathlib/Data/Multiset/Pairwise.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2025 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Mathlib.Data.List.Pairwise
+import Mathlib.Data.Multiset.Defs
+
+namespace Multiset
+
+variable {α : Type*} {r : α → α → Prop} {s : Multiset α}
+
+theorem Pairwise.forall (H : Symmetric r) (hs : Pairwise r s) :
+    ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ≠ b → r a b :=
+  let ⟨_, hl₁, hl₂⟩ := hs
+  hl₁.symm ▸ hl₂.forall H
+
+end Multiset
diff --git a/Mathlib/Data/Multiset/Powerset.lean b/Mathlib/Data/Multiset/Powerset.lean
index 7f294a1f20d3ef..9fe6778a461750 100644
--- a/Mathlib/Data/Multiset/Powerset.lean
+++ b/Mathlib/Data/Multiset/Powerset.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.List.Sublists
 import Mathlib.Data.List.Zip
 import Mathlib.Data.Multiset.Bind
+import Mathlib.Data.Multiset.Range
 
 /-!
 # The powerset of a multiset
diff --git a/Mathlib/Data/Multiset/Range.lean b/Mathlib/Data/Multiset/Range.lean
index bcc6154065f019..5568ff70fe0e50 100644
--- a/Mathlib/Data/Multiset/Range.lean
+++ b/Mathlib/Data/Multiset/Range.lean
@@ -62,4 +62,14 @@ theorem range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ (range b).m
   rw [range_add, add_eq_union_iff_disjoint]
   apply range_disjoint_map_add
 
+section Nodup
+
+theorem nodup_range (n : ℕ) : Nodup (range n) :=
+  List.nodup_range _
+
+theorem range_le {m n : ℕ} : range m ≤ range n ↔ m ≤ n :=
+  (le_iff_subset (nodup_range _)).trans range_subset
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/Replicate.lean b/Mathlib/Data/Multiset/Replicate.lean
index c5b7e8362cd75e..07b81c315f7bb9 100644
--- a/Mathlib/Data/Multiset/Replicate.lean
+++ b/Mathlib/Data/Multiset/Replicate.lean
@@ -148,4 +148,26 @@ theorem rel_replicate_right {m : Multiset α} {a : α} {r : α → α → Prop}
 
 end Rel
 
+section Replicate
+
+variable {r : α → α → Prop} {s : Multiset α}
+
+theorem nodup_iff_le {s : Multiset α} : Nodup s ↔ ∀ a : α, ¬a ::ₘ a ::ₘ 0 ≤ s :=
+  Quot.induction_on s fun _ =>
+    nodup_iff_sublist.trans <| forall_congr' fun a => not_congr (@replicate_le_coe _ a 2 _).symm
+
+theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t :=
+  nodup_iff_le.trans
+    ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
+      let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
+      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩
+
+theorem nodup_iff_pairwise {α} {s : Multiset α} : Nodup s ↔ Pairwise (· ≠ ·) s :=
+  Quotient.inductionOn s fun _ => (pairwise_coe_iff_pairwise fun _ _ => Ne.symm).symm
+
+protected theorem Nodup.pairwise : (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → Nodup s → Pairwise r s :=
+  Quotient.inductionOn s fun l h hl => ⟨l, rfl, hl.imp_of_mem fun {a b} ha hb => h a ha b hb⟩
+
+end Replicate
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/Sum.lean b/Mathlib/Data/Multiset/Sum.lean
index 66512fa5879092..91a04f9feb6a0f 100644
--- a/Mathlib/Data/Multiset/Sum.lean
+++ b/Mathlib/Data/Multiset/Sum.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Group.Multiset
-import Mathlib.Data.Multiset.Nodup
 
 /-!
 # Disjoint sum of multisets
diff --git a/Mathlib/Data/Multiset/UnionInter.lean b/Mathlib/Data/Multiset/UnionInter.lean
index b8147facfbf224..fbb39e5e2b1780 100644
--- a/Mathlib/Data/Multiset/UnionInter.lean
+++ b/Mathlib/Data/Multiset/UnionInter.lean
@@ -353,4 +353,29 @@ theorem map_set_pairwise {f : α → β} {r : β → β → Prop} {m : Multiset
     obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
     exact h H₁ H₂ (mt (congr_arg f) hn)
 
+section Nodup
+
+variable {s t : Multiset α} {a : α}
+
+theorem nodup_add {s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
+  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append]
+
+theorem disjoint_of_nodup_add {s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t :=
+  (nodup_add.1 d).2.2
+
+theorem Nodup.add_iff (d₁ : Nodup s) (d₂ : Nodup t) : Nodup (s + t) ↔ Disjoint s t := by
+  simp [nodup_add, d₁, d₂]
+
+lemma Nodup.inter_left [DecidableEq α] (t) : Nodup s → Nodup (s ∩ t) := nodup_of_le inter_le_left
+lemma Nodup.inter_right [DecidableEq α] (s) : Nodup t → Nodup (s ∩ t) := nodup_of_le inter_le_right
+
+@[simp]
+theorem nodup_union [DecidableEq α] {s t : Multiset α} : Nodup (s ∪ t) ↔ Nodup s ∧ Nodup t :=
+  ⟨fun h => ⟨nodup_of_le le_union_left h, nodup_of_le le_union_right h⟩, fun ⟨h₁, h₂⟩ =>
+    nodup_iff_count_le_one.2 fun a => by
+      rw [count_union]
+      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)⟩
+
+end Nodup
+
 end Multiset
diff --git a/Mathlib/Data/Multiset/ZeroCons.lean b/Mathlib/Data/Multiset/ZeroCons.lean
index cabfcde851df81..d7cb951ac6f365 100644
--- a/Mathlib/Data/Multiset/ZeroCons.lean
+++ b/Mathlib/Data/Multiset/ZeroCons.lean
@@ -592,4 +592,27 @@ end Rel
 theorem pairwise_zero (r : α → α → Prop) : Multiset.Pairwise r 0 :=
   ⟨[], rfl, List.Pairwise.nil⟩
 
+section Nodup
+
+variable {s : Multiset α} {a : α}
+
+@[simp]
+theorem nodup_zero : @Nodup α 0 :=
+  Pairwise.nil
+
+@[simp]
+theorem nodup_cons {a : α} {s : Multiset α} : Nodup (a ::ₘ s) ↔ a ∉ s ∧ Nodup s :=
+  Quot.induction_on s fun _ => List.nodup_cons
+
+theorem Nodup.cons (m : a ∉ s) (n : Nodup s) : Nodup (a ::ₘ s) :=
+  nodup_cons.2 ⟨m, n⟩
+
+theorem Nodup.of_cons (h : Nodup (a ::ₘ s)) : Nodup s :=
+  (nodup_cons.1 h).2
+
+theorem Nodup.not_mem (h : Nodup (a ::ₘ s)) : a ∉ s :=
+  (nodup_cons.1 h).1
+
+end Nodup
+
 end Multiset

From 1fca12ecaf3002a61a709765b6179597a442acc4 Mon Sep 17 00:00:00 2001
From: "Anne C.A. Baanen" <vierkantor@vierkantor.com>
Date: Mon, 3 Mar 2025 16:36:10 +0100
Subject: [PATCH 2/2] Fixes

---
 Mathlib/Data/Finset/Range.lean      | 1 +
 Mathlib/Data/Multiset/Pairwise.lean | 7 +++++++
 2 files changed, 8 insertions(+)

diff --git a/Mathlib/Data/Finset/Range.lean b/Mathlib/Data/Finset/Range.lean
index dbf606c086f597..a8e994a5f10d5e 100644
--- a/Mathlib/Data/Finset/Range.lean
+++ b/Mathlib/Data/Finset/Range.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Insert
+import Mathlib.Data.Multiset.Range
 import Mathlib.Order.Interval.Set.Defs
 
 /-!
diff --git a/Mathlib/Data/Multiset/Pairwise.lean b/Mathlib/Data/Multiset/Pairwise.lean
index 95d8c1415b6f70..607a21404e498f 100644
--- a/Mathlib/Data/Multiset/Pairwise.lean
+++ b/Mathlib/Data/Multiset/Pairwise.lean
@@ -6,6 +6,13 @@ Authors: Chris Hughes
 import Mathlib.Data.List.Pairwise
 import Mathlib.Data.Multiset.Defs
 
+/-!
+# Pairwise relations on a multiset
+
+This file provides basic results about `Multiset.Pairwise` (definitions are in
+`Mathlib.Data.Multiset.Defs`).
+-/
+
 namespace Multiset
 
 variable {α : Type*} {r : α → α → Prop} {s : Multiset α}