chore: Rename lemmas about the coercion List → Multiset (#11099)

These did not respect the naming convention by having the `coe` as a prefix instead of a suffix, or vice-versa. Also add a bunch of `norm_cast`

Mathlib/Algebra/BigOperators/Basic.lean

@@ -438,7 +438,7 @@ section ToList
 
 @[to_additive (attr := simp)]
 theorem prod_to_list (s : Finset α) (f : α → β) : (s.toList.map f).prod = s.prod f := by
-  rw [Finset.prod, ← Multiset.coe_prod, ← Multiset.coe_map, Finset.coe_toList]
+  rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]
 #align finset.prod_to_list Finset.prod_to_list
 #align finset.sum_to_list Finset.sum_to_list
 
@@ -1563,7 +1563,7 @@ theorem prod_multiset_count_of_subset [DecidableEq α] [CommMonoid α] (m : Mult
     (hs : m.toFinset ⊆ s) : m.prod = ∏ i in s, i ^ m.count i := by
   revert hs
   refine' Quot.induction_on m fun l => _
-  simp only [quot_mk_to_coe'', coe_prod, coe_count]
+  simp only [quot_mk_to_coe'', prod_coe, coe_count]
   apply prod_list_count_of_subset l s
 #align finset.prod_multiset_count_of_subset Finset.prod_multiset_count_of_subset
 #align finset.sum_multiset_count_of_subset Finset.sum_multiset_count_of_subset
@@ -2371,7 +2371,7 @@ theorem disjoint_list_sum_right {a : Multiset α} {l : List (Multiset α)} :
 theorem disjoint_sum_left {a : Multiset α} {i : Multiset (Multiset α)} :
     Multiset.Disjoint i.sum a ↔ ∀ b ∈ i, Multiset.Disjoint b a :=
   Quotient.inductionOn i fun l => by
-    rw [quot_mk_to_coe, Multiset.coe_sum]
+    rw [quot_mk_to_coe, Multiset.sum_coe]
     exact disjoint_list_sum_left
 #align multiset.disjoint_sum_left Multiset.disjoint_sum_left
 

Mathlib/Algebra/BigOperators/Multiset/Basic.lean

@@ -61,15 +61,15 @@ theorem prod_eq_foldl (s : Multiset α) :
 #align multiset.sum_eq_foldl Multiset.sum_eq_foldl
 
 @[to_additive (attr := simp, norm_cast)]
-theorem coe_prod (l : List α) : prod ↑l = l.prod :=
+theorem prod_coe (l : List α) : prod ↑l = l.prod :=
   prod_eq_foldl _
-#align multiset.coe_prod Multiset.coe_prod
-#align multiset.coe_sum Multiset.coe_sum
+#align multiset.coe_prod Multiset.prod_coe
+#align multiset.coe_sum Multiset.sum_coe
 
 @[to_additive (attr := simp)]
 theorem prod_toList (s : Multiset α) : s.toList.prod = s.prod := by
   conv_rhs => rw [← coe_toList s]
-  rw [coe_prod]
+  rw [prod_coe]
 #align multiset.prod_to_list Multiset.prod_toList
 #align multiset.sum_to_list Multiset.sum_toList
 
@@ -87,14 +87,14 @@ theorem prod_cons (a : α) (s) : prod (a ::ₘ s) = a * prod s :=
 
 @[to_additive (attr := simp)]
 theorem prod_erase [DecidableEq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod := by
-  rw [← s.coe_toList, coe_erase, coe_prod, coe_prod, List.prod_erase (mem_toList.2 h)]
+  rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
 #align multiset.prod_erase Multiset.prod_erase
 #align multiset.sum_erase Multiset.sum_erase
 
 @[to_additive (attr := simp)]
 theorem prod_map_erase [DecidableEq ι] {a : ι} (h : a ∈ m) :
     f a * ((m.erase a).map f).prod = (m.map f).prod := by
-  rw [← m.coe_toList, coe_erase, coe_map, coe_map, coe_prod, coe_prod,
+  rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe,
     List.prod_map_erase f (mem_toList.2 h)]
 #align multiset.prod_map_erase Multiset.prod_map_erase
 #align multiset.sum_map_erase Multiset.sum_map_erase
@@ -157,7 +157,7 @@ theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).
 theorem prod_hom [CommMonoid β] (s : Multiset α) {F : Type*} [FunLike F α β]
     [MonoidHomClass F α β] (f : F) :
     (s.map f).prod = f s.prod :=
-  Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]
+  Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]
 #align multiset.prod_hom Multiset.prod_hom
 #align multiset.sum_hom Multiset.sum_hom
 
@@ -175,7 +175,7 @@ theorem prod_hom₂ [CommMonoid β] [CommMonoid γ] (s : Multiset ι) (f : α 
     (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α)
     (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
   Quotient.inductionOn s fun l => by
-    simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, coe_map, coe_prod]
+    simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]
 #align multiset.prod_hom₂ Multiset.prod_hom₂
 #align multiset.sum_hom₂ Multiset.sum_hom₂
 
@@ -184,7 +184,7 @@ theorem prod_hom_rel [CommMonoid β] (s : Multiset ι) {r : α → β → Prop}
     (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
     r (s.map f).prod (s.map g).prod :=
   Quotient.inductionOn s fun l => by
-    simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]
+    simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]
 #align multiset.prod_hom_rel Multiset.prod_hom_rel
 #align multiset.sum_hom_rel Multiset.sum_hom_rel
 
@@ -290,7 +290,7 @@ variable [NoZeroDivisors α] [Nontrivial α] {s : Multiset α}
 @[simp]
 theorem prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
   Quotient.inductionOn s fun l => by
-    rw [quot_mk_to_coe, coe_prod]
+    rw [quot_mk_to_coe, prod_coe]
     exact List.prod_eq_zero_iff
 #align multiset.prod_eq_zero_iff Multiset.prod_eq_zero_iff
 
@@ -388,7 +388,7 @@ theorem prod_le_pow_card (s : Multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) :
 theorem all_one_of_le_one_le_of_prod_eq_one :
     (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α) :=
   Quotient.inductionOn s (by
-    simp only [quot_mk_to_coe, coe_prod, mem_coe]
+    simp only [quot_mk_to_coe, prod_coe, mem_coe]
     exact fun l => List.all_one_of_le_one_le_of_prod_eq_one)
 #align multiset.all_one_of_le_one_le_of_prod_eq_one Multiset.all_one_of_le_one_le_of_prod_eq_one
 #align multiset.all_zero_of_le_zero_le_of_sum_eq_zero Multiset.all_zero_of_le_zero_le_of_sum_eq_zero
@@ -438,7 +438,7 @@ variable [OrderedCancelCommMonoid α] {s : Multiset ι} {f g : ι → α}
 theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
     (s.map f).prod < (s.map g).prod := by
   obtain ⟨l⟩ := s
-  simp only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_prod]
+  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
   exact List.prod_lt_prod' f g hle hlt
 
 @[to_additive sum_lt_sum_of_nonempty]

Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean

@@ -32,7 +32,7 @@ end Multiset
 lemma CanonicallyOrderedCommSemiring.multiset_prod_pos {R} [CanonicallyOrderedCommSemiring R]
     [Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ (∀ x ∈ m, (0 : R) < x) := by
   rcases m with ⟨l⟩
-  rw [Multiset.quot_mk_to_coe'', Multiset.coe_prod]
+  rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
   exact CanonicallyOrderedCommSemiring.list_prod_pos
 
 open Multiset
@@ -43,7 +43,7 @@ variable [NonUnitalNonAssocSemiring α] (s : Multiset α)
 
 theorem multiset_sum_right (a : α) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum := by
   induction s using Quotient.inductionOn
-  rw [quot_mk_to_coe, coe_sum]
+  rw [quot_mk_to_coe, sum_coe]
   exact Commute.list_sum_right _ _ h
 #align commute.multiset_sum_right Commute.multiset_sum_right
 

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -176,7 +176,7 @@ theorem sup_support_multiset_prod_le (degb0 : degb 0 ≤ 0)
     (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (m : Multiset R[A]) :
     m.prod.support.sup degb ≤ (m.map fun f : R[A] => f.support.sup degb).sum := by
   induction m using Quot.inductionOn
-  rw [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_sum, Multiset.coe_prod]
+  rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]
   exact sup_support_list_prod_le degb0 degbm _
 #align add_monoid_algebra.sup_support_multiset_prod_le AddMonoidAlgebra.sup_support_multiset_prod_le
 

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -624,7 +624,7 @@ theorem hasFDerivAt_list_prod_attach' [DecidableEq ι] {l : List ι} {x : {i //
 /--
 Auxiliary lemma for `hasStrictFDerivAt_multiset_prod`.
 
-For `NormedCommRing 𝔸'`, can rewrite as `Multiset` using `Multiset.coe_prod`.
+For `NormedCommRing 𝔸'`, can rewrite as `Multiset` using `Multiset.prod_coe`.
 -/
 theorem hasStrictFDerivAt_list_prod [DecidableEq ι] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
     HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -881,7 +881,7 @@ variable {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A]
 theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1 := by
   refine opNorm_le_bound _ zero_le_one fun m => ?_
   simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
-    Fin.prod_univ_def, Multiset.coe_map, Multiset.coe_prod]
+    Fin.prod_univ_def, Multiset.map_coe, Multiset.prod_coe]
   refine' (List.norm_prod_le' _).trans_eq _
   · rw [Ne.def, List.map_eq_nil, List.finRange_eq_nil]
     exact Nat.succ_ne_zero _

Mathlib/Combinatorics/Partition.lean

@@ -74,7 +74,7 @@ instance decidableEqPartition {n : ℕ} : DecidableEq (Partition n) :=
 def ofComposition (n : ℕ) (c : Composition n) : Partition n where
   parts := c.blocks
   parts_pos hi := c.blocks_pos hi
-  parts_sum := by rw [Multiset.coe_sum, c.blocks_sum]
+  parts_sum := by rw [Multiset.sum_coe, c.blocks_sum]
 #align nat.partition.of_composition Nat.Partition.ofComposition
 
 theorem ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n) := by

Mathlib/Data/Finsupp/BigOperators.lean

@@ -48,7 +48,7 @@ theorem List.support_sum_subset [AddMonoid M] (l : List (ι →₀ M)) :
 theorem Multiset.support_sum_subset [AddCommMonoid M] (s : Multiset (ι →₀ M)) :
     s.sum.support ⊆ (s.map Finsupp.support).sup := by
   induction s using Quot.inductionOn
-  simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_sum, Multiset.coe_map, Multiset.sup_coe,
+  simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
     List.foldr_map] using List.support_sum_subset _
 #align multiset.support_sum_subset Multiset.support_sum_subset
 
@@ -69,7 +69,7 @@ theorem List.mem_foldr_sup_support_iff [Zero M] {l : List (ι →₀ M)} {x : ι
 theorem Multiset.mem_sup_map_support_iff [Zero M] {s : Multiset (ι →₀ M)} {x : ι} :
     x ∈ (s.map Finsupp.support).sup ↔ ∃ f ∈ s, x ∈ f.support :=
   Quot.inductionOn s fun _ ↦ by
-    simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.sup_coe, List.foldr_map]
+    simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
     using List.mem_foldr_sup_support_iff
 #align multiset.mem_sup_map_support_iff Multiset.mem_sup_map_support_iff
 
@@ -103,11 +103,11 @@ theorem Multiset.support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))
   obtain ⟨l, hl, hd⟩ := hs
   suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
     convert List.support_sum_eq a this
-    · simp only [Multiset.quot_mk_to_coe'', Multiset.coe_sum]
+    · simp only [Multiset.quot_mk_to_coe'', Multiset.sum_coe]
     · dsimp only [Function.comp_def]
-      simp only [quot_mk_to_coe'', coe_map, sup_coe, ge_iff_le, Finset.le_eq_subset,
+      simp only [quot_mk_to_coe'', map_coe, sup_coe, ge_iff_le, Finset.le_eq_subset,
         Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
-  simp only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_eq_coe] at hl
+  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.coe_eq_coe] at hl
   exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h
 #align multiset.support_sum_eq Multiset.support_sum_eq
 

Mathlib/Data/Multiset/Antidiagonal.lean

@@ -76,7 +76,7 @@ theorem antidiagonal_cons (a : α) (s) :
       map (Prod.map id (cons a)) (antidiagonal s) + map (Prod.map (cons a) id) (antidiagonal s) :=
   Quotient.inductionOn s fun l ↦ by
     simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe,
-      coe_map, antidiagonal_coe', coe_add]
+      map_coe, antidiagonal_coe', coe_add]
     rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
     · congr; simp; rw [map_reverse]; simp
     · simp

Mathlib/Data/Multiset/Basic.lean

@@ -1203,10 +1203,8 @@ theorem forall_mem_map_iff {f : α → β} {p : β → Prop} {s : Multiset α} :
   Quotient.inductionOn' s fun _L => List.forall_mem_map_iff
 #align multiset.forall_mem_map_iff Multiset.forall_mem_map_iff
 
-@[simp]
-theorem coe_map (f : α → β) (l : List α) : map f ↑l = l.map f :=
-  rfl
-#align multiset.coe_map Multiset.coe_map
+@[simp, norm_cast] lemma map_coe (f : α → β) (l : List α) : map f l = l.map f := rfl
+#align multiset.coe_map Multiset.map_coe
 
 @[simp]
 theorem map_zero (f : α → β) : map f 0 = 0 :=
@@ -1230,7 +1228,7 @@ theorem map_singleton (f : α → β) (a : α) : ({a} : Multiset α).map f = {f
 
 @[simp]
 theorem map_replicate (f : α → β) (k : ℕ) (a : α) : (replicate k a).map f = replicate k (f a) := by
-  simp only [← coe_replicate, coe_map, List.map_replicate]
+  simp only [← coe_replicate, map_coe, List.map_replicate]
 #align multiset.map_replicate Multiset.map_replicate
 
 @[simp]
@@ -1245,7 +1243,7 @@ instance canLift (c) (p) [CanLift α β c p] :
   prf := by
     rintro ⟨l⟩ hl
     lift l to List β using hl
-    exact ⟨l, coe_map _ _⟩
+    exact ⟨l, map_coe _ _⟩
 #align multiset.can_lift Multiset.canLift
 
 /-- `Multiset.map` as an `AddMonoidHom`. -/
@@ -1973,10 +1971,8 @@ def filter (s : Multiset α) : Multiset α :=
   Quot.liftOn s (fun l => (List.filter p l : Multiset α)) fun _l₁ _l₂ h => Quot.sound <| h.filter p
 #align multiset.filter Multiset.filter
 
-@[simp]
-theorem coe_filter (l : List α) : filter p ↑l = l.filter p :=
-  rfl
-#align multiset.coe_filter Multiset.coe_filter
+@[simp, norm_cast] lemma filter_coe (l : List α) : filter p l = l.filter p := rfl
+#align multiset.coe_filter Multiset.filter_coe
 
 @[simp]
 theorem filter_zero : filter p 0 = 0 :=
@@ -2179,10 +2175,9 @@ def filterMap (f : α → Option β) (s : Multiset α) : Multiset β :=
     fun _l₁ _l₂ h => Quot.sound <| h.filterMap f
 #align multiset.filter_map Multiset.filterMap
 
-@[simp]
-theorem coe_filterMap (f : α → Option β) (l : List α) : filterMap f l = l.filterMap f :=
-  rfl
-#align multiset.coe_filter_map Multiset.coe_filterMap
+@[simp, norm_cast]
+lemma filterMap_coe (f : α → Option β) (l : List α) : filterMap f l = l.filterMap f := rfl
+#align multiset.coe_filter_map Multiset.filterMap_coe
 
 @[simp]
 theorem filterMap_zero (f : α → Option β) : filterMap f 0 = 0 :=
@@ -2584,7 +2579,7 @@ theorem le_count_iff_replicate_le {a : α} {s : Multiset α} {n : ℕ} :
 theorem count_filter_of_pos {p} [DecidablePred p] {a} {s : Multiset α} (h : p a) :
     count a (filter p s) = count a s :=
   Quot.inductionOn s fun _l => by
-    simp only [quot_mk_to_coe'', coe_filter, mem_coe, coe_count, decide_eq_true_eq]
+    simp only [quot_mk_to_coe'', filter_coe, mem_coe, coe_count, decide_eq_true_eq]
     apply count_filter
     simpa using h
 #align multiset.count_filter_of_pos Multiset.count_filter_of_pos
@@ -2604,7 +2599,7 @@ theorem count_filter {p} [DecidablePred p] {a} {s : Multiset α} :
 
 theorem ext {s t : Multiset α} : s = t ↔ ∀ a, count a s = count a t :=
   Quotient.inductionOn₂ s t fun _l₁ _l₂ => Quotient.eq.trans <| by
-    simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count, decide_eq_true_eq]
+    simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count, decide_eq_true_eq]
     apply perm_iff_count
 #align multiset.ext Multiset.ext
 
@@ -2662,7 +2657,7 @@ theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) (
 
 theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b :=
   Quotient.inductionOn s fun l => by
-    simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count]
+    simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count]
     rw [List.filter_eq l b, coe_replicate]
 #align multiset.filter_eq' Multiset.filter_eq'
 
@@ -2961,7 +2956,7 @@ lemma filter_attach' (s : Multiset α) (p : {a // a ∈ s} → Prop) [DecidableE
   classical
   refine' Multiset.map_injective Subtype.val_injective _
   rw [map_filter' _ Subtype.val_injective]
-  simp only [Function.comp, Subtype.exists, coe_mk,
+  simp only [Function.comp, Subtype.exists, coe_mk, Subtype.map,
     exists_and_right, exists_eq_right, attach_map_val, map_map, map_coe, id.def]
 #align multiset.filter_attach' Multiset.filter_attach'
 

Mathlib/Data/Multiset/Bind.lean

@@ -42,7 +42,7 @@ theorem coe_join :
   | [] => rfl
   | l :: L => by
       -- Porting note: was `congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)`
-      simp only [join, List.map, coe_sum, List.sum_cons, List.join, ← coe_add, ← coe_join L]
+      simp only [join, List.map, sum_coe, List.sum_cons, List.join, ← coe_add, ← coe_join L]
 #align multiset.coe_join Multiset.coe_join
 
 @[simp]

Mathlib/Data/Multiset/Functor.lean

@@ -94,7 +94,7 @@ theorem lift_coe {α β : Type*} (x : List α) (f : List α → β)
 @[simp]
 theorem map_comp_coe {α β} (h : α → β) :
     Functor.map h ∘ Coe.coe = (Coe.coe ∘ Functor.map h : List α → Multiset β) := by
-  funext; simp only [Function.comp_apply, Coe.coe, fmap_def, coe_map, List.map_eq_map]
+  funext; simp only [Function.comp_apply, Coe.coe, fmap_def, map_coe, List.map_eq_map]
 #align multiset.map_comp_coe Multiset.map_comp_coe
 
 theorem id_traverse {α : Type*} (x : Multiset α) : traverse (pure : α → Id α) x = x := by
@@ -128,7 +128,7 @@ theorem traverse_map {G : Type* → Type _} [Applicative G] [CommApplicative G]
     (g : α → β) (h : β → G γ) (x : Multiset α) : traverse h (map g x) = traverse (h ∘ g) x := by
   refine' Quotient.inductionOn x _
   intro
-  simp only [traverse, quot_mk_to_coe, coe_map, lift_coe, Function.comp_apply]
+  simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]
   rw [← Traversable.traverse_map h g, List.map_eq_map]
 #align multiset.traverse_map Multiset.traverse_map
 

Mathlib/Data/Multiset/NatAntidiagonal.lean

@@ -58,12 +58,12 @@ theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
 @[simp]
 theorem antidiagonal_succ {n : ℕ} :
     antidiagonal (n + 1) = (0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id) := by
-  simp only [antidiagonal, List.Nat.antidiagonal_succ, coe_map, cons_coe]
+  simp only [antidiagonal, List.Nat.antidiagonal_succ, map_coe, cons_coe]
 #align multiset.nat.antidiagonal_succ Multiset.Nat.antidiagonal_succ
 
 theorem antidiagonal_succ' {n : ℕ} :
     antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ) := by
-  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, coe_map,
+  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, map_coe,
     coe_add, List.singleton_append, cons_coe]
 #align multiset.nat.antidiagonal_succ' Multiset.Nat.antidiagonal_succ'
 
@@ -75,7 +75,7 @@ theorem antidiagonal_succ_succ' {n : ℕ} :
 #align multiset.nat.antidiagonal_succ_succ' Multiset.Nat.antidiagonal_succ_succ'
 
 theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n := by
-  rw [antidiagonal, coe_map, List.Nat.map_swap_antidiagonal, coe_reverse]
+  rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]
 #align multiset.nat.map_swap_antidiagonal Multiset.Nat.map_swap_antidiagonal
 
 end Nat

Mathlib/Data/Multiset/Powerset.lean

@@ -112,7 +112,7 @@ theorem mem_powerset {s t : Multiset α} : s ∈ powerset t ↔ s ≤ t :=
 
 theorem map_single_le_powerset (s : Multiset α) : s.map singleton ≤ powerset s :=
   Quotient.inductionOn s fun l => by
-    simp only [powerset_coe, quot_mk_to_coe, coe_le, coe_map]
+    simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]
     show l.map (((↑) : List α → Multiset α) ∘ List.ret) <+~ (sublists l).map (↑)
     rw [← List.map_map]
     exact ((map_ret_sublist_sublists _).map _).subperm

Mathlib/Data/MvPolynomial/Variables.lean

@@ -726,7 +726,7 @@ theorem totalDegree_list_prod :
 theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
     s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum := by
   refine' Quotient.inductionOn s fun l => _
-  rw [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map, Multiset.coe_sum]
+  rw [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe, Multiset.sum_coe]
   exact totalDegree_list_prod l
 #align mv_polynomial.total_degree_multiset_prod MvPolynomial.totalDegree_multiset_prod