chore(Data/Multiset): redistribute Nodup material

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

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

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

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

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

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
 
 /-!

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

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

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.

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

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

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