From 414bd49465c014736d566bffd0a798ba06c2b775 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 20 Feb 2024 23:51:58 +0000
Subject: [PATCH] chore: classify `dsimp can prove this` porting notes (#10686)

Classifies by adding issue number (#10685) to porting notes claiming `dsimp can prove this`.
---
 Mathlib/Computability/TuringMachine.lean    | 2 +-
 Mathlib/Data/Analysis/Topology.lean         | 2 +-
 Mathlib/Data/Multiset/Fintype.lean          | 2 +-
 Mathlib/Data/Nat/Digits.lean                | 2 +-
 Mathlib/GroupTheory/Subgroup/Basic.lean     | 2 +-
 Mathlib/MeasureTheory/Function/LpSpace.lean | 2 +-
 Mathlib/Order/JordanHolder.lean             | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index 033ed552333d9..85fb1cbd0e482 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -358,7 +358,7 @@ instance {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] : Inhabited (PointedMap Γ Γ')
 instance {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] : CoeFun (PointedMap Γ Γ') fun _ ↦ Γ → Γ' :=
   ⟨PointedMap.f⟩
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem PointedMap.mk_val {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : Γ → Γ') (pt) :
     (PointedMap.mk f pt : Γ → Γ') = f :=
   rfl
diff --git a/Mathlib/Data/Analysis/Topology.lean b/Mathlib/Data/Analysis/Topology.lean
index dd21cddf6de6a..9c8733b94e3c2 100644
--- a/Mathlib/Data/Analysis/Topology.lean
+++ b/Mathlib/Data/Analysis/Topology.lean
@@ -60,7 +60,7 @@ variable (F : Ctop α σ)
 instance : CoeFun (Ctop α σ) fun _ ↦ σ → Set α :=
   ⟨Ctop.f⟩
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem coe_mk (f T h₁ I h₂ h₃ a) : (@Ctop.mk α σ f T h₁ I h₂ h₃) a = f a := rfl
 #align ctop.coe_mk Ctop.coe_mk
 
diff --git a/Mathlib/Data/Multiset/Fintype.lean b/Mathlib/Data/Multiset/Fintype.lean
index ea3632dad8f53..507e55473b4d6 100644
--- a/Mathlib/Data/Multiset/Fintype.lean
+++ b/Mathlib/Data/Multiset/Fintype.lean
@@ -77,7 +77,7 @@ theorem Multiset.coe_eq {x y : m} : (x : α) = (y : α) ↔ x.1 = y.1 := by
   rfl
 #align multiset.coe_eq Multiset.coe_eq
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem Multiset.coe_mk {x : α} {i : Fin (m.count x)} : ↑(m.mkToType x i) = x :=
   rfl
 #align multiset.coe_mk Multiset.coe_mk
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index 5d70771bb1227..06c532f70bcb2 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -110,7 +110,7 @@ theorem digits_one (n : ℕ) : digits 1 n = List.replicate n 1 :=
   rfl
 #align nat.digits_one Nat.digits_one
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem digits_one_succ (n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n :=
   rfl
 #align nat.digits_one_succ Nat.digits_one_succ
diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
index 30740448fe506..63c28b3203fa3 100644
--- a/Mathlib/GroupTheory/Subgroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -751,7 +751,7 @@ theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
 #align subgroup.coe_pow Subgroup.coe_pow
 #align add_subgroup.coe_nsmul AddSubgroup.coe_nsmul
 
-@[to_additive (attr := norm_cast)] -- Porting note: dsimp can prove this
+@[to_additive (attr := norm_cast)] -- Porting note (#10685): dsimp can prove this
 theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
   rfl
 #align subgroup.coe_zpow Subgroup.coe_zpow
diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index 9e5edd40c86c5..c459c668c9c33 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -186,7 +186,7 @@ theorem coeFn_mk {f : α →ₘ[μ] E} (hf : snorm f p μ < ∞) : ((⟨f, hf⟩
   rfl
 #align measure_theory.Lp.coe_fn_mk MeasureTheory.Lp.coeFn_mk
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem coe_mk {f : α →ₘ[μ] E} (hf : snorm f p μ < ∞) : ((⟨f, hf⟩ : Lp E p μ) : α →ₘ[μ] E) = f :=
   rfl
 #align measure_theory.Lp.coe_mk MeasureTheory.Lp.coe_mk
diff --git a/Mathlib/Order/JordanHolder.lean b/Mathlib/Order/JordanHolder.lean
index 92e1fb11f9a40..8081e1ed6cc1c 100644
--- a/Mathlib/Order/JordanHolder.lean
+++ b/Mathlib/Order/JordanHolder.lean
@@ -157,7 +157,7 @@ theorem step (s : CompositionSeries X) :
   s.step'
 #align composition_series.step CompositionSeries.step
 
--- @[simp] -- Porting note: dsimp can prove this
+-- @[simp] -- Porting note (#10685): dsimp can prove this
 theorem coeFn_mk (length : ℕ) (series step) :
     (@CompositionSeries.mk X _ _ length series step : Fin length.succ → X) = series :=
   rfl