feat: more lemmas about List.dedup and other lattice operations (#1…

…4282)

Also the trivial `Multiset` wrappers.

Mathlib/Data/List/Dedup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.List.Nodup
+import Mathlib.Data.List.Lattice
 
 #align_import data.list.dedup from "leanprover-community/mathlib"@"d9e96a3e3e0894e93e10aff5244f4c96655bac1c"
 
@@ -24,7 +25,7 @@ universe u
 
 namespace List
 
-variable {α : Type u} [DecidableEq α]
+variable {α β : Type*} [DecidableEq α]
 
 @[simp]
 theorem dedup_nil : dedup [] = ([] : List α) :=
@@ -132,6 +133,42 @@ theorem dedup_append (l₁ l₂ : List α) : dedup (l₁ ++ l₂) = l₁ ∪ ded
   · rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]
 #align list.dedup_append List.dedup_append
 
+theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f)
+    (xs : List α) :
+    (xs.map f).dedup = xs.dedup.map f := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    rw [map_cons]
+    by_cases h : x ∈ xs
+    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem f h), ih]
+    · rw [dedup_cons_of_not_mem h, dedup_cons_of_not_mem <| (mem_map_of_injective hf).not.mpr h, ih,
+        map_cons]
+
+/-- Note that the weaker `List.Subset.dedup_append_left` is proved later. -/
+theorem Subset.dedup_append_right {xs ys : List α} (h : xs ⊆ ys) :
+    dedup (xs ++ ys) = dedup ys := by
+  rw [List.dedup_append, Subset.union_eq_right (h.trans <| subset_dedup _)]
+
+theorem Disjoint.union_eq {xs ys : List α} (h : Disjoint xs ys) :
+    xs ∪ ys = xs.dedup ++ ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    rw [cons_union]
+    rw [disjoint_cons_left] at h
+    by_cases hx : x ∈ xs
+    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
+    · rw [dedup_cons_of_not_mem hx, insert_of_not_mem, ih h.2, cons_append]
+      rw [mem_union_iff, not_or]
+      exact ⟨hx, h.1⟩
+
+theorem Disjoint.dedup_append {xs ys : List α} (h : Disjoint xs ys) :
+    dedup (xs ++ ys) = dedup xs ++ dedup ys := by
+  rw [List.dedup_append, Disjoint.union_eq]
+  intro a hx hy
+  exact h hx (mem_dedup.mp hy)
+
 theorem replicate_dedup {x : α} : ∀ {k}, k ≠ 0 → (replicate k x).dedup = [x]
   | 0, h => (h rfl).elim
   | 1, _ => rfl

Mathlib/Data/List/Lattice.lean

@@ -118,6 +118,13 @@ theorem forall_mem_of_forall_mem_union_right (h : ∀ x ∈ l₁ ∪ l₂, p x)
   (forall_mem_union.1 h).2
 #align list.forall_mem_of_forall_mem_union_right List.forall_mem_of_forall_mem_union_right
 
+theorem Subset.union_eq_right {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    rw [cons_union, insert_of_mem <| mem_union_right _ <| h <| mem_cons_self _ _,
+      ih <| subset_of_cons_subset h]
+
 end Union
 
 /-! ### `inter` -/
@@ -140,6 +147,12 @@ theorem inter_cons_of_not_mem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) 
   simp [Inter.inter, List.inter, h]
 #align list.inter_cons_of_not_mem List.inter_cons_of_not_mem
 
+@[simp]
+theorem inter_nil' (l : List α) : l ∩ [] = [] := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih => by_cases x ∈ xs <;> simp [ih]
+
 theorem mem_of_mem_inter_left : a ∈ l₁ ∩ l₂ → a ∈ l₁ :=
   mem_of_mem_filter
 #align list.mem_of_mem_inter_left List.mem_of_mem_inter_left
@@ -169,6 +182,8 @@ theorem inter_eq_nil_iff_disjoint : l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂ :=
   rfl
 #align list.inter_eq_nil_iff_disjoint List.inter_eq_nil_iff_disjoint
 
+alias ⟨_, Disjoint.inter_eq_nil⟩ := inter_eq_nil_iff_disjoint
+
 theorem forall_mem_inter_of_forall_left (h : ∀ x ∈ l₁, p x) (l₂ : List α) :
     ∀ x, x ∈ l₁ ∩ l₂ → p x :=
   BAll.imp_left (fun _ => mem_of_mem_inter_left) h
@@ -184,6 +199,9 @@ theorem inter_reverse {xs ys : List α} : xs.inter ys.reverse = xs.inter ys := b
   simp only [List.inter, elem_eq_mem, mem_reverse]
 #align list.inter_reverse List.inter_reverse
 
+theorem Subset.inter_eq_left {xs ys : List α} (h : xs ⊆ ys) : xs ∩ ys = xs :=
+  List.filter_eq_self.mpr fun _ ha => elem_eq_true_of_mem (h ha)
+
 end Inter
 
 /-! ### `bagInter` -/

Mathlib/Data/Multiset/Dedup.lean

@@ -117,6 +117,11 @@ theorem dedup_ext {s t : Multiset α} : dedup s = dedup t ↔ ∀ a, a ∈ s ↔
   simp [Nodup.ext]
 #align multiset.dedup_ext Multiset.dedup_ext
 
+theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f)
+    (s : Multiset α) :
+    (s.map f).dedup = s.dedup.map f :=
+  Quot.induction_on s fun l => by simp [List.dedup_map_of_injective hf l]
+
 theorem dedup_map_dedup_eq [DecidableEq β] (f : α → β) (s : Multiset α) :
     dedup (map f (dedup s)) = dedup (map f s) := by
   simp [dedup_ext]
@@ -132,6 +137,25 @@ theorem Nodup.le_dedup_iff_le {s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedu
   simp [le_dedup, hno]
 #align multiset.nodup.le_dedup_iff_le Multiset.Nodup.le_dedup_iff_le
 
+theorem Subset.dedup_add_right {s t : Multiset α} (h : s ⊆ t) :
+    dedup (s + t) = dedup t := by
+  induction s, t using Quot.induction_on₂
+  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h
+
+theorem Subset.dedup_add_left {s t : Multiset α} (h : t ⊆ s) :
+    dedup (s + t) = dedup s := by
+  rw [add_comm, Subset.dedup_add_right h]
+
+theorem Disjoint.dedup_add {s t : Multiset α} (h : Disjoint s t) :
+    dedup (s + t) = dedup s + dedup t := by
+  induction s, t using Quot.induction_on₂
+  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.dedup_append h
+
+/-- Note that the stronger `List.Subset.dedup_append_right` is proved earlier. -/
+theorem _root_.List.Subset.dedup_append_left {s t : List α} (h : t ⊆ s) :
+    List.dedup (s ++ t) ~ List.dedup s := by
+  rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
+
 end Multiset
 
 theorem Multiset.Nodup.le_nsmul_iff_le {α : Type*} {s t : Multiset α} {n : ℕ} (h : s.Nodup)

Mathlib/Data/Multiset/FinsetOps.lean

@@ -205,6 +205,15 @@ theorem dedup_add (s t : Multiset α) : dedup (s + t) = ndunion s (dedup t) :=
   Quot.induction_on₂ s t fun _ _ => congr_arg ((↑) : List α → Multiset α) <| dedup_append _ _
 #align multiset.dedup_add Multiset.dedup_add
 
+theorem Disjoint.ndunion_eq {s t : Multiset α} (h : Disjoint s t) :
+    s.ndunion t = s.dedup + t := by
+  induction s, t using Quot.induction_on₂
+  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq h
+
+theorem Subset.ndunion_eq_right {s t : Multiset α} (h : s ⊆ t) : s.ndunion t = t := by
+  induction s, t using Quot.induction_on₂
+  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right h
+
 /-! ### finset inter -/
 
 
@@ -280,6 +289,12 @@ theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ D
   rw [← subset_zero]; simp [subset_iff, Disjoint]
 #align multiset.ndinter_eq_zero_iff_disjoint Multiset.ndinter_eq_zero_iff_disjoint
 
+alias ⟨_, Disjoint.ndinter_eq_zero⟩ := ndinter_eq_zero_iff_disjoint
+
+theorem Subset.ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s := by
+  induction s, t using Quot.induction_on₂
+  rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]
+
 end Multiset
 
 -- Assert that we define `Finset` without the material on the set lattice.