From ab08c7acc68fcfd7b0a488506af2933606145b25 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri, 4 Oct 2024 10:46:24 +0200
Subject: [PATCH] chore: avoid Coe.coe in Data.Multiset.Functor

This was ported incorrectly from mathlib3.
---
 Mathlib/Data/Multiset/Functor.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Data/Multiset/Functor.lean b/Mathlib/Data/Multiset/Functor.lean
index 81575f5f445c4..1704e68fcedf6 100644
--- a/Mathlib/Data/Multiset/Functor.lean
+++ b/Mathlib/Data/Multiset/Functor.lean
@@ -38,14 +38,15 @@ variable {α' β' : Type u} (f : α' → F β')
     and collect the results.
 -/
 def traverse : Multiset α' → F (Multiset β') := by
-  refine Quotient.lift (Functor.map Coe.coe ∘ Traversable.traverse f) ?_
+  refine Quotient.lift (Functor.map ((↑) : List β' → Multiset β') ∘ Traversable.traverse f) ?_
   introv p; unfold Function.comp
   induction p with
   | nil => rfl
   | @cons x l₁ l₂ _ h =>
     have :
-      Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
-        Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ := by rw [h]
+      Multiset.cons <$> f x <*> ((↑) : List β' → Multiset β') <$> Traversable.traverse f l₁ =
+        Multiset.cons <$> f x <*> ((↑) : List β' → Multiset β') <$> Traversable.traverse f l₂ := by
+      rw [h]
     simpa [functor_norm] using this
   | swap x y l =>
     have :
@@ -55,7 +56,7 @@ def traverse : Multiset α' → F (Multiset β') := by
       congr
       funext a b l
       simpa [flip] using Perm.swap a b l
-    simp [Function.comp_def, this, functor_norm, Coe.coe]
+    simp [Function.comp_def, this, functor_norm]
   | trans => simp [*]
 
 instance : Monad Multiset :=
@@ -83,13 +84,14 @@ open Traversable LawfulTraversable
 
 @[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, map_coe, List.map_eq_map]
+    Functor.map h ∘ ((↑) : List α → Multiset α) =
+      (((↑) : List β → Multiset β) ∘ Functor.map h : List α → Multiset β) := by
+  funext; simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]
 
 theorem id_traverse {α : Type*} (x : Multiset α) : traverse (pure : α → Id α) x = x := by
   refine Quotient.inductionOn x ?_
   intro
-  simp [traverse, Coe.coe]
+  simp [traverse]
 
 theorem comp_traverse {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G]
     [CommApplicative H] {α β γ : Type _} (g : α → G β) (h : β → H γ) (x : Multiset α) :
@@ -97,8 +99,7 @@ theorem comp_traverse {G H : Type _ → Type _} [Applicative G] [Applicative H]
     Comp.mk (Functor.map (traverse h) (traverse g x)) := by
   refine Quotient.inductionOn x ?_
   intro
-  simp only [traverse, quot_mk_to_coe, lift_coe, Coe.coe, Function.comp_apply, Functor.map_map,
-    functor_norm]
+  simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, functor_norm]
 
 theorem map_traverse {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _}
     (g : α → G β) (h : β → γ) (x : Multiset α) :
@@ -107,8 +108,7 @@ theorem map_traverse {G : Type* → Type _} [Applicative G] [CommApplicative G]
   intro
   simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, map_comp_coe]
   rw [Traversable.map_traverse']
-  simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map]
-  rfl
+  simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]
 
 theorem traverse_map {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _}
     (g : α → β) (h : β → G γ) (x : Multiset α) : traverse h (map g x) = traverse (h ∘ g) x := by