[Merged by Bors] - chore: move Multiset.lift_coe

Mathlib/Data/Multiset/Basic.lean

@@ -57,6 +57,12 @@ theorem quot_mk_to_coe'' (l : List α) : @Eq (Multiset α) (Quot.mk Setoid.r l)
   rfl
 #align multiset.quot_mk_to_coe'' Multiset.quot_mk_to_coe''
 
+@[simp]
+theorem lift_coe {α β : Type*} (x : List α) (f : List α → β)
+    (h : ∀ a b : List α, a ≈ b → f a = f b) : Quotient.lift f h (x : Multiset α) = f x :=
+  Quotient.lift_mk _ _ _
+#align multiset.lift_coe Multiset.lift_coe
+
 @[simp]
 theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ ~ l₂ :=
   Quotient.eq

Mathlib/Data/Multiset/Functor.lean

@@ -87,12 +87,6 @@ open Functor
 
 open Traversable LawfulTraversable
 
-@[simp]
-theorem lift_coe {α β : Type*} (x : List α) (f : List α → β)
-    (h : ∀ a b : List α, a ≈ b → f a = f b) : Quotient.lift f h (x : Multiset α) = f x :=
-  Quotient.lift_mk _ _ _
-#align multiset.lift_coe Multiset.lift_coe
-
 @[simp]
 theorem map_comp_coe {α β} (h : α → β) :
     Functor.map h ∘ Coe.coe = (Coe.coe ∘ Functor.map h : List α → Multiset β) := by