[Merged by Bors] - chore: classify simp cannot prove porting notes

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -200,7 +200,7 @@ instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
   refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
   · -- Porting note: broken ext
     apply LinearMap.ext_ring
-    -- Porting note: simp used to be able to close this goal
+    -- Porting note (#10959): simp used to be able to close this goal
     dsimp
     erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
       Finsupp.single_eq_same, id_apply]
@@ -210,7 +210,7 @@ instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
     apply LinearMap.ext_ring
     apply Finsupp.ext
     intro ⟨⟩
-    -- Porting note: simp used to be able to close this goal
+    -- Porting note (#10959): simp used to be able to close this goal
     dsimp
     erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
       Finsupp.single_eq_same]
@@ -323,7 +323,7 @@ def embedding : C ⥤ Free R C where
   map {X Y} f := Finsupp.single f 1
   map_id X := rfl
   map_comp {X Y Z} f g := by
-    -- Porting note: simp used to be able to close this goal
+    -- Porting note (#10959): simp used to be able to close this goal
     dsimp only []
     rw [single_comp_single, one_mul]
 #align category_theory.Free.embedding CategoryTheory.Free.embedding
@@ -341,7 +341,7 @@ def lift (F : C ⥤ D) : Free R C ⥤ D where
   map_id := by dsimp [CategoryTheory.categoryFree]; simp
   map_comp {X Y Z} f g := by
     apply Finsupp.induction_linear f
-    · -- Porting note: simp used to be able to close this goal
+    · -- Porting note (#10959): simp used to be able to close this goal
       dsimp
       rw [Limits.zero_comp, sum_zero_index, Limits.zero_comp]
     · intro f₁ f₂ w₁ w₂
@@ -355,7 +355,7 @@ def lift (F : C ⥤ D) : Free R C ⥤ D where
       · intros; simp only [add_smul]
     · intro f' r
       apply Finsupp.induction_linear g
-      · -- Porting note: simp used to be able to close this goal
+      · -- Porting note (#10959): simp used to be able to close this goal
         dsimp
         rw [Limits.comp_zero, sum_zero_index, Limits.comp_zero]
       · intro f₁ f₂ w₁ w₂
@@ -405,7 +405,7 @@ def ext {F G : Free R C ⥤ D} [F.Additive] [F.Linear R] [G.Additive] [G.Linear
     (by
       intro X Y f
       apply Finsupp.induction_linear f
-      · -- Porting note: simp used to be able to close this goal
+      · -- Porting note (#10959): simp used to be able to close this goal
         rw [Functor.map_zero, Limits.zero_comp, Functor.map_zero, Limits.comp_zero]
       · intro f₁ f₂ w₁ w₂
         -- Porting note: Using rw instead of simp

Mathlib/Algebra/ContinuedFractions/Translations.lean

@@ -154,7 +154,7 @@ theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some
 theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
     g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by
   simp [nth_cont_eq_succ_nth_cont_aux]
-  -- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2
+  -- Porting note (#10959): simp used to work here, but now it can't figure out that 1 + 1 = 2
   convert second_continuant_aux_eq zeroth_s_eq
 #align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq
 

Mathlib/Algebra/Homology/Augment.lean

@@ -334,14 +334,14 @@ def augmentTruncate (C : CochainComplex V ℕ) :
       comm' := fun i j => by
         rcases j with (_ | _ | j) <;> cases i <;>
           · dsimp
-            -- Porting note: simp can't handle this now but aesop does
+            -- Porting note (#10959): simp can't handle this now but aesop does
             aesop }
   inv :=
     { f := fun i => by cases i <;> exact 𝟙 _
       comm' := fun i j => by
         rcases j with (_ | _ | j) <;> cases' i with i <;>
           · dsimp
-            -- Porting note: simp can't handle this now but aesop does
+            -- Porting note (#10959): simp can't handle this now but aesop does
             aesop }
   hom_inv_id := by
     ext i

Mathlib/Analysis/NormedSpace/Star/Basic.lean

@@ -202,7 +202,7 @@ section Unital
 
 variable [NormedRing E] [StarRing E] [CstarRing E]
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem norm_one [Nontrivial E] : ‖(1 : E)‖ = 1 := by
   have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
   rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]

Mathlib/Analysis/Quaternion.lean

@@ -80,12 +80,12 @@ theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_coe a
 #align quaternion.nnnorm_coe Quaternion.nnnorm_coe
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
   simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
 #align quaternion.norm_star Quaternion.norm_star
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_star a
 #align quaternion.nnnorm_star Quaternion.nnnorm_star
@@ -147,7 +147,7 @@ theorem coeComplex_one : ((1 : ℂ) : ℍ) = 1 :=
   rfl
 #align quaternion.coe_complex_one Quaternion.coeComplex_one
 
-@[simp, norm_cast, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, norm_cast, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp
 #align quaternion.coe_real_complex_mul Quaternion.coe_real_complex_mul
 

Mathlib/Data/List/Basic.lean

@@ -3007,7 +3007,7 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
   rw [attach, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl
 #align list.pmap_eq_map_attach List.pmap_eq_map_attach
 
--- @[simp] -- Porting note: lean 4 simp can't rewrite with this
+-- @[simp] -- Porting note (#10959): lean 4 simp can't rewrite with this
 theorem attach_map_coe' (l : List α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, map_pmap]; exact pmap_eq_map _ _ _ _

Mathlib/Order/Filter/Germ.lean

@@ -252,7 +252,7 @@ theorem coe_compTendsto (f : α → β) {lc : Filter γ} {g : γ → α} (hg : T
   rfl
 #align filter.germ.coe_comp_tendsto Filter.Germ.coe_compTendsto
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem compTendsto'_coe (f : Germ l β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
     f.compTendsto' _ hg.germ_tendsto = f.compTendsto g hg :=
   rfl

Mathlib/RingTheory/Valuation/ValuationSubring.lean

@@ -47,7 +47,7 @@ instance : SetLike (ValuationSubring K) K where
     replace h := SetLike.coe_injective' h
     congr
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove that
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove that
 theorem mem_carrier (x : K) : x ∈ A.carrier ↔ x ∈ A := Iff.refl _
 #align valuation_subring.mem_carrier ValuationSubring.mem_carrier
 

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -1148,14 +1148,14 @@ theorem bfamilyOfFamily_typein {ι} (f : ι → α) (i) :
   bfamilyOfFamily'_typein _ f i
 #align ordinal.bfamily_of_family_typein Ordinal.bfamilyOfFamily_typein
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem familyOfBFamily'_enum {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o}
     (ho : type r = o) (f : ∀ a < o, α) (i hi) :
     familyOfBFamily' r ho f (enum r i (by rwa [ho])) = f i hi := by
   simp only [familyOfBFamily', typein_enum]
 #align ordinal.family_of_bfamily'_enum Ordinal.familyOfBFamily'_enum
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem familyOfBFamily_enum (o : Ordinal) (f : ∀ a < o, α) (i hi) :
     familyOfBFamily o f
         (enum (· < ·) i
@@ -1450,7 +1450,7 @@ theorem sup_eq_bsup' {o : Ordinal.{u}} {ι} (r : ι → ι → Prop) [IsWellOrde
   sup_eq_sup r _ ho _ f
 #align ordinal.sup_eq_bsup' Ordinal.sup_eq_bsup'
 
-@[simp, nolint simpNF] -- Porting note: simp cannot prove this
+@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
 theorem sSup_eq_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     sSup (brange o f) = bsup.{_, v} o f := by
   congr