chore: classify added dsimp porting notes (#11228)

Classifies by adding issue number #11227 to porting notes claiming anything equivalent to: 

- "added `dsimp`"
- "`dsimp` added"
- "`dsimp` now needed"

Mathlib/Order/Interval.lean

@@ -726,7 +726,7 @@ noncomputable instance completeLattice [@DecidableRel α (· ≤ ·)] :
           cases s with
           | none => exact bot_le
           | some s =>
-            dsimp -- Porting note: added
+            dsimp -- Porting note (#11227): added a `dsimp`
             split_ifs with h
             · exact WithBot.some_le_some.2
                 ⟨iSup₂_le fun t hb => (WithBot.coe_le_coe.1 <| ha _ hb).1,

Mathlib/RepresentationTheory/Basic.lean

@@ -456,11 +456,11 @@ def linHom : Representation k G (V →ₗ[k] W) where
       map_smul' := fun r f => by simp_rw [RingHom.id_apply, smul_comp, comp_smul] }
   map_one' :=
     LinearMap.ext fun x => by
-      dsimp -- Porting note: now needed
+      dsimp -- Porting note (#11227):now needed
       simp_rw [inv_one, map_one, one_eq_id, comp_id, id_comp]
   map_mul' g h :=
     LinearMap.ext fun x => by
-      dsimp -- Porting note: now needed
+      dsimp -- Porting note (#11227):now needed
       simp_rw [mul_inv_rev, map_mul, mul_eq_comp, comp_assoc]
 #align representation.lin_hom Representation.linHom
 
@@ -481,11 +481,11 @@ def dual : Representation k G (Module.Dual k V) where
         simp only [coe_comp, Function.comp_apply, smul_apply, RingHom.id_apply] }
   map_one' := by
     ext
-    dsimp -- Porting note: now needed
+    dsimp -- Porting note (#11227):now needed
     simp only [coe_comp, Function.comp_apply, map_one, inv_one, coe_mk, one_apply]
   map_mul' g h := by
     ext
-    dsimp -- Porting note: now needed
+    dsimp -- Porting note (#11227):now needed
     simp only [coe_comp, Function.comp_apply, mul_inv_rev, map_mul, coe_mk, mul_apply]
 #align representation.dual Representation.dual
 

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -235,7 +235,7 @@ variable {i x}
 @[simp]
 theorem lift_map (h : IsAdjoinRoot S f) (z : R[X]) : h.lift i x hx (h.map z) = z.eval₂ i x := by
   rw [lift, RingHom.coe_mk]
-  dsimp -- Porting note: added
+  dsimp -- Porting note (#11227):added a `dsimp`
   rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]
 #align is_adjoin_root.lift_map IsAdjoinRoot.lift_map
 
@@ -387,7 +387,7 @@ theorem modByMonicHom_map (h : IsAdjoinRootMonic S f) (g : R[X]) :
 @[simp]
 theorem map_modByMonicHom (h : IsAdjoinRootMonic S f) (x : S) : h.map (h.modByMonicHom x) = x := by
   rw [modByMonicHom, LinearMap.coe_mk]
-  dsimp -- Porting note: added
+  dsimp -- Porting note (#11227):added a `dsimp`
   rw [map_modByMonic, map_repr]
 #align is_adjoin_root_monic.map_mod_by_monic_hom IsAdjoinRootMonic.map_modByMonicHom
 
@@ -427,7 +427,7 @@ def basis (h : IsAdjoinRootMonic S f) : Basis (Fin (natDegree f)) R S :=
         by_cases hx : h.toIsAdjoinRoot.repr x %ₘ f = 0
         · simp [hx]
         refine coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le ?_ hi)
-        dsimp -- Porting note: added
+        dsimp -- Porting note (#11227):added a `dsimp`
         rw [natDegree_lt_natDegree_iff hx]
         · exact degree_modByMonic_lt _ h.Monic
       right_inv := fun g => by

Mathlib/Topology/Sheaves/Skyscraper.lean

@@ -151,15 +151,15 @@ noncomputable def skyscraperPresheafCoconeIsColimitOfSpecializes {y : X} (h : p
     IsColimit (skyscraperPresheafCoconeOfSpecializes p₀ A h) where
   desc c := eqToHom (if_pos trivial).symm ≫ c.ι.app (op ⊤)
   fac c U := by
-    dsimp -- Porting note: added a `dsimp`
+    dsimp -- Porting note (#11227):added a `dsimp`
     rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
     change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
     rw [dif_pos]
     · simp only [skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc,
         eqToHom_refl, Category.id_comp, unop_op, op_unop]
     · exact h.mem_open U.unop.1.2 U.unop.2
   uniq c f h := by
-    dsimp -- Porting note: added a `dsimp`
+    dsimp -- Porting note (#11227):added a `dsimp`
     rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl,
       Category.id_comp]
 #align skyscraper_presheaf_cocone_is_colimit_of_specializes skyscraperPresheafCoconeIsColimitOfSpecializes
@@ -200,7 +200,7 @@ noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {y : X} (h :
       refine' ((if_neg _).symm.ndrec terminalIsTerminal).hom_ext _ _
       exact fun h => h1.choose_spec h.1
     uniq := fun c f H => by
-      dsimp -- Porting note: added a `dsimp`
+      dsimp -- Porting note (#11227):added a `dsimp`
       rw [← Category.id_comp f, ← H, ← Category.assoc]
       congr 1; apply terminalIsTerminal.hom_ext }
 #align skyscraper_presheaf_cocone_is_colimit_of_not_specializes skyscraperPresheafCoconeIsColimitOfNotSpecializes