feat(Data): lemmas for List.bagInter (#35892)

Basic API lemmas for `List.bagInter` and correct a few misnamed lemmas.

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>

Author: vlad902

Mathlib/Data/List/Lattice.lean

@@ -157,6 +157,14 @@ theorem inter_reverse {xs ys : List α} : xs ∩ ys.reverse = xs ∩ ys := by
 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)
 
+theorem Sublist.inter_left {l₁ l₂ l₃ : List α} (h : l₂.Sublist l₃) :
+    (l₁ ∩ l₂).Sublist (l₁ ∩ l₃) := by
+  grind [inter_def, monotone_filter_right]
+
+theorem Sublist.inter_right {l₁ l₂ l₃ : List α} (h : l₁.Sublist l₂) :
+    (l₁ ∩ l₃).Sublist (l₂ ∩ l₃) := by
+  grind [inter_def]
+
 end Inter
 
 /-! ### `bagInter` -/
@@ -171,20 +179,34 @@ theorem nil_bagInter (l : List α) : [].bagInter l = [] := by cases l <;> rfl
 theorem bagInter_nil (l : List α) : l.bagInter [] = [] := by cases l <;> rfl
 
 @[simp]
-theorem cons_bagInter_of_pos (l₁ : List α) (h : a ∈ l₂) :
+theorem cons_bagInter_of_mem (l₁ : List α) (h : a ∈ l₂) :
     (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a) := by
   cases l₂ with grind [List.bagInter]
 
+@[deprecated (since := "2026-05-13")]
+alias cons_bagInter_of_pos := cons_bagInter_of_mem
+
 @[simp]
-theorem cons_bagInter_of_neg (l₁ : List α) (h : a ∉ l₂) :
+theorem cons_bagInter_of_not_mem (l₁ : List α) (h : a ∉ l₂) :
     (a :: l₁).bagInter l₂ = l₁.bagInter l₂ := by
   cases l₂ with grind [List.bagInter]
 
+@[deprecated (since := "2026-05-13")]
+alias cons_bagInter_of_neg := cons_bagInter_of_not_mem
+
 @[grind =]
-theorem cons_bagInteger :
+theorem cons_bagInter :
     (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂ := by
   split_ifs <;> simp_all
 
+@[deprecated (since := "2026-05-13")]
+alias cons_bagInteger := cons_bagInter
+
+@[simp]
+theorem bagInter_cons_of_not_mem (l₂ : List α) (h : a ∉ l₁) :
+    l₁.bagInter (a :: l₂) = l₁.bagInter l₂ := by
+  induction l₁ generalizing l₂ <;> grind
+
 @[simp]
 theorem mem_bagInter {a : α} {l₁ l₂ : List α} : a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂ := by
   fun_induction List.bagInter with grind
@@ -197,13 +219,49 @@ theorem count_bagInter {a : α} {l₁ l₂ : List α} :
 theorem bagInter_sublist_left {l₁ l₂ : List α} : l₁.bagInter l₂ <+ l₁ := by
   fun_induction List.bagInter with grind
 
+theorem singleton_bagInter (a : α) : [a].bagInter l₁ = if a ∈ l₁ then [a] else [] := by
+  grind
+
+theorem bagInter_singleton (a : α) : l₁.bagInter [a] = if a ∈ l₁ then [a] else [] := by
+  induction l₁ <;> grind
+
+@[simp]
+theorem bagInter_erase_of_not_mem (h : a ∉ l₁) :
+    l₁.bagInter (l₂.erase a) = l₁.bagInter l₂ := by
+  induction l₁ generalizing l₂ <;> grind
+
+@[simp]
+theorem erase_bagInter_of_not_mem (h : a ∉ l₂) :
+    (l₁.erase a).bagInter l₂ = l₁.bagInter l₂ := by
+  induction l₁ generalizing l₂ <;> grind
+
 theorem bagInter_nil_iff_inter_nil : ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
   | [], l₂ => by simp
   | b :: l₁, l₂ => by
     by_cases h : b ∈ l₂
     · simp [h]
     · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂
 
+@[simp]
+theorem bagInter_eq_nil_iff_disjoint : l₁.bagInter l₂ = [] ↔ l₁.Disjoint l₂ :=
+  (bagInter_nil_iff_inter_nil _ _).trans inter_eq_nil_iff_disjoint
+
+theorem Nodup.bagInter_right (h : l₁.Nodup) : (l₁.bagInter l₂).Nodup :=
+  nodup_iff_count.mpr fun x ↦ (by grind [List.count_bagInter])
+
+theorem Nodup.bagInter_left (h : l₂.Nodup) : (l₁.bagInter l₂).Nodup :=
+  nodup_iff_count.mpr fun x ↦ (by grind [List.count_bagInter])
+
+theorem Sublist.bagInter_inter : (l₁.bagInter l₂).Sublist (l₁ ∩ l₂) := by
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons _ _ ih =>
+    rw [cons_bagInter]
+    split
+    · rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
+      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])
+    · simp_all
+
 end BagInter
 
 end List

Mathlib/Data/List/Perm/Lattice.lean

@@ -45,6 +45,9 @@ theorem Perm.bagInter {l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t
     l₁.bagInter t₁ ~ l₂.bagInter t₂ :=
   ht.bagInter_left l₂ ▸ hl.bagInter_right _
 
+theorem Perm.bagInter_symm (l₁ l₂ : List α) : (l₁.bagInter l₂).Perm (l₂.bagInter l₁) :=
+  perm_iff_count.mpr fun _ ↦ (by simp [List.count_bagInter, Nat.min_comm])
+
 theorem Perm.inter_append {l t₁ t₂ : List α} (h : Disjoint t₁ t₂) :
     l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ := by
   induction l with

Mathlib/Data/Multiset/UnionInter.lean

@@ -99,11 +99,11 @@ instance : Inter (Multiset α) := ⟨inter⟩
 
 @[simp]
 lemma cons_inter_of_pos (s : Multiset α) : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a :=
-  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_pos _ h
+  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_mem _ h
 
 @[simp]
 lemma cons_inter_of_neg (s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t :=
-  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_neg _ h
+  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_not_mem _ h
 
 lemma inter_le_left : s ∩ t ≤ s :=
   Quotient.inductionOn₂ s t fun _l₁ _l₂ => bagInter_sublist_left.subperm