feat(data/list/basic): map_erase, map_diff, map_union

data/list/basic.lean

@@ -2146,6 +2146,15 @@ end
 else by simp [hb, mt mem_of_mem_erase hb]
 else by simp [ha, mt mem_of_mem_erase ha]
 
+theorem map_erase [decidable_eq β] {f : α → β} (finj : injective f) {a : α} :
+  ∀ (l : list α), map f (l.erase a) = (map f l).erase (f a)
+| []     := by simp [list.erase]
+| (b::l) := if h : f b = f a then by simp [h, finj h] else by simp [h, mt (congr_arg f) h, map_erase l]
+
+theorem map_foldl_erase [decidable_eq β] {f : α → β} (finj : injective f) {l₁ l₂ : list α} :
+  map f (foldl list.erase l₁ l₂) = foldl (λ l a, l.erase (f a)) (map f l₁) l₂ :=
+by induction l₂ generalizing l₁; simp [map_erase finj, *]
+
 end erase
 
 /- diff -/
@@ -2164,6 +2173,11 @@ theorem diff_eq_foldl : ∀ (l₁ l₂ : list α), l₁.diff l₂ = foldl list.e
 @[simp] theorem diff_append (l₁ l₂ l₃ : list α) : l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃ :=
 by simp [diff_eq_foldl]
 
+@[simp] theorem map_diff [decidable_eq β] {f : α → β} (finj : injective f) {l₁ l₂ : list α} :
+  map f (l₁.diff l₂) = (map f l₁).diff (map f l₂) :=
+by simp [diff_eq_foldl, map_foldl_erase finj]
+
+
 end diff
 
 /- zip & unzip -/

data/multiset.lean

@@ -1105,6 +1105,11 @@ by rw ← eq_union_left h₂; exact union_le_union_right h₁ t
 ⟨λ h, (mem_add.1 h).imp_left (mem_of_le $ sub_le_self _ _),
  or.rec (mem_of_le $ le_union_left _ _) (mem_of_le $ le_union_right _ _)⟩
 
+@[simp] theorem map_union [decidable_eq β] {f : α → β} (finj : function.injective f) {s t : multiset α} :
+  map f (s ∪ t) = map f s ∪ map f t :=
+quotient.induction_on₂ s t $ λ l₁ l₂,
+congr_arg coe (by rw [list.map_append f, list.map_diff finj])
+
 /- inter -/
 
 /-- `s ∩ t` is the lattice meet operation with respect to the