diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
index 42a25ab336b19..89f706b546d03 100644
--- a/Mathlib/Algebra/Algebra/Unitization.lean
+++ b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -743,8 +743,7 @@ def starLift : (A →⋆ₙₐ[R] C) ≃ (Unitization R A →⋆ₐ[R] C) :=
   right_inv := fun φ => Unitization.algHom_ext'' <| by
     simp }
 
--- Note (#6057) : tagging simpNF because linter complains
-@[simp high, nolint simpNF]
+@[simp high]
 theorem starLift_symm_apply_apply (φ : Unitization R A →⋆ₐ[R] C) (a : A) :
     Unitization.starLift.symm φ a = φ a :=
   rfl
diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
index a02b2d8a48142..dffd8f94b48be 100644
--- a/Mathlib/Algebra/BigOperators/Finsupp.lean
+++ b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -86,22 +86,17 @@ theorem prod_ite_eq [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M 
   dsimp [Finsupp.prod]
   rw [f.support.prod_ite_eq]
 
-/- Porting note: simpnf linter, added aux lemma below
-Left-hand side simplifies from
-  Finsupp.sum f fun x v => if a = x then v else 0
-to
-  if ↑f a = 0 then 0 else ↑f a
--/
--- @[simp]
 theorem sum_ite_self_eq [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
     (f.sum fun x v => ite (a = x) v 0) = f a := by
   classical
     convert f.sum_ite_eq a fun _ => id
     simp [ite_eq_right_iff.2 Eq.symm]
 
--- Porting note: Added this thm to replace the simp in the previous one. Need to add [DecidableEq N]
+/--
+The left hand side of `sum_ite_self_eq` simplifies; this is the variant that is useful for `simp`.
+-/
 @[simp]
-theorem sum_ite_self_eq_aux [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
+theorem if_mem_support [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
     (if a ∈ f.support then f a else 0) = f a := by
   simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
   exact fun h ↦ h.symm
@@ -113,6 +108,7 @@ theorem prod_ite_eq' [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M 
   dsimp [Finsupp.prod]
   rw [f.support.prod_ite_eq']
 
+/-- A restatement of `sum_ite_self_eq` with the equality test reversed. -/
 theorem sum_ite_self_eq' [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
     (f.sum fun x v => ite (x = a) v 0) = f a := by
   classical
diff --git a/Mathlib/Algebra/Group/WithOne/Basic.lean b/Mathlib/Algebra/Group/WithOne/Basic.lean
index 3dca5ba0dab77..b9d87ce1b04af 100644
--- a/Mathlib/Algebra/Group/WithOne/Basic.lean
+++ b/Mathlib/Algebra/Group/WithOne/Basic.lean
@@ -73,8 +73,7 @@ variable (f : α →ₙ* β)
 theorem lift_coe (x : α) : lift f x = f x :=
   rfl
 
--- Porting note (#11119): removed `simp` attribute to appease `simpNF` linter.
-@[to_additive]
+@[to_additive (attr := simp)]
 theorem lift_one : lift f 1 = 1 :=
   rfl
 
diff --git a/Mathlib/Algebra/Homology/ShortComplex/Homology.lean b/Mathlib/Algebra/Homology/ShortComplex/Homology.lean
index 25854245e340c..0c416a49f4df5 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/Homology.lean
+++ b/Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@@ -70,8 +70,6 @@ structure HomologyMapData where
 
 namespace HomologyMapData
 
-attribute [nolint simpNF] mk.injEq
-
 variable {φ h₁ h₂}
 
 @[reassoc]
diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
index 1022a52c7ab90..a8abcedd4972c 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
+++ b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@@ -266,7 +266,6 @@ structure LeftHomologyMapData where
 namespace LeftHomologyMapData
 
 attribute [reassoc (attr := simp)] commi commf' commπ
-attribute [nolint simpNF] mk.injEq
 
 /-- The left homology map data associated to the zero morphism between two short complexes. -/
 @[simps]
diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
index 865ffa00b94fb..3592289533893 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
+++ b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@@ -356,7 +356,6 @@ structure RightHomologyMapData where
 namespace RightHomologyMapData
 
 attribute [reassoc (attr := simp)] commp commg' commι
-attribute [nolint simpNF] mk.injEq
 
 /-- The right homology map data associated to the zero morphism between two short complexes. -/
 @[simps]
diff --git a/Mathlib/Algebra/Lie/IdealOperations.lean b/Mathlib/Algebra/Lie/IdealOperations.lean
index 75e9facacd878..459dce3dfdbf0 100644
--- a/Mathlib/Algebra/Lie/IdealOperations.lean
+++ b/Mathlib/Algebra/Lie/IdealOperations.lean
@@ -192,12 +192,10 @@ theorem sup_lie : ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆ := by
   use ⁅((⟨x₂, hx₂⟩ : J) : L), (n : N)⁆; constructor; · apply lie_coe_mem_lie
   simp [← h, ← hx']
 
--- @[simp] -- Porting note: not in simpNF
 theorem lie_inf : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆ := by
   rw [le_inf_iff]; constructor <;>
   apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]
 
--- @[simp] -- Porting note: not in simpNF
 theorem inf_lie : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆ := by
   rw [le_inf_iff]; constructor <;>
   apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]
diff --git a/Mathlib/Algebra/Module/GradedModule.lean b/Mathlib/Algebra/Module/GradedModule.lean
index 8adb7c6ada0a5..8797f2bbdd7b5 100644
--- a/Mathlib/Algebra/Module/GradedModule.lean
+++ b/Mathlib/Algebra/Module/GradedModule.lean
@@ -93,11 +93,9 @@ theorem smulAddMonoidHom_apply_of_of [DecidableEq ιA] [DecidableEq ιB] [GMonoi
     smulAddMonoidHom A M (DirectSum.of A i x) (of M j y) = of M (i +ᵥ j) (GSMul.smul x y) := by
   simp [smulAddMonoidHom]
 
--- @[simp] -- Porting note: simpNF lint
 theorem of_smul_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
     {i j} (x : A i) (y : M j) :
-    DirectSum.of A i x • of M j y = of M (i +ᵥ j) (GSMul.smul x y) :=
-  smulAddMonoidHom_apply_of_of _ _ _ _
+    DirectSum.of A i x • of M j y = of M (i +ᵥ j) (GSMul.smul x y) := by simp
 
 open AddMonoidHom
 
diff --git a/Mathlib/Algebra/Module/Submodule/Pointwise.lean b/Mathlib/Algebra/Module/Submodule/Pointwise.lean
index 3e0acab091ae2..c59d22e02a63f 100644
--- a/Mathlib/Algebra/Module/Submodule/Pointwise.lean
+++ b/Mathlib/Algebra/Module/Submodule/Pointwise.lean
@@ -161,9 +161,7 @@ instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M) where
 theorem add_eq_sup (p q : Submodule R M) : p + q = p ⊔ q :=
   rfl
 
--- dsimp loops when applying this lemma to its LHS,
--- probably https://github.com/leanprover/lean4/pull/2867
-@[simp, nolint simpNF]
+@[simp]
 theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
   rfl
 
diff --git a/Mathlib/Algebra/MvPolynomial/Basic.lean b/Mathlib/Algebra/MvPolynomial/Basic.lean
index f1c838c583594..dd9248b0bbdf0 100644
--- a/Mathlib/Algebra/MvPolynomial/Basic.lean
+++ b/Mathlib/Algebra/MvPolynomial/Basic.lean
@@ -839,9 +839,8 @@ theorem constantCoeff_X (i : σ) : constantCoeff (X i : MvPolynomial σ R) = 0 :
   simp [constantCoeff_eq]
 
 variable {R}
-/- porting note: increased priority because otherwise `simp` time outs when trying to simplify
-the left-hand side. `simpNF` linter indicated this and it was verified. -/
-@[simp 1001]
+
+@[simp]
 theorem constantCoeff_smul {R : Type*} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) :
     constantCoeff (a • f) = a • constantCoeff f :=
   rfl
diff --git a/Mathlib/Algebra/Ring/Semiconj.lean b/Mathlib/Algebra/Ring/Semiconj.lean
index 8b20e68a71a06..0ec9636ddebc6 100644
--- a/Mathlib/Algebra/Ring/Semiconj.lean
+++ b/Mathlib/Algebra/Ring/Semiconj.lean
@@ -61,13 +61,9 @@ section
 
 variable [MulOneClass R] [HasDistribNeg R]
 
--- Porting note: `simpNF` told me to remove `simp` attribute
-theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) :=
-  (one_right a).neg_right
+theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) := by simp
 
--- Porting note: `simpNF` told me to remove `simp` attribute
-theorem neg_one_left (x : R) : SemiconjBy (-1) x x :=
-  (SemiconjBy.one_left x).neg_left
+theorem neg_one_left (x : R) : SemiconjBy (-1) x x := by simp
 
 end
 
diff --git a/Mathlib/Algebra/Star/Subsemiring.lean b/Mathlib/Algebra/Star/Subsemiring.lean
index 8ef2bdd8fdd39..707ac11a068a8 100644
--- a/Mathlib/Algebra/Star/Subsemiring.lean
+++ b/Mathlib/Algebra/Star/Subsemiring.lean
@@ -53,7 +53,6 @@ instance starRing (s : StarSubsemiring R) : StarRing s :=
 instance semiring (s : StarSubsemiring R) : NonAssocSemiring s :=
   s.toSubsemiring.toNonAssocSemiring
 
-@[simp, nolint simpNF]
 theorem mem_carrier {s : StarSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s :=
   Iff.rfl
 
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
index 22365ec289413..2533459ec4771 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
@@ -129,7 +129,6 @@ open Submodule Submodule.IsPrincipal
 theorem spanSingleton_inv (x : K) : (spanSingleton R₁⁰ x)⁻¹ = spanSingleton _ x⁻¹ :=
   one_div_spanSingleton x
 
--- @[simp] -- Porting note: not in simpNF form
 theorem spanSingleton_div_spanSingleton (x y : K) :
     spanSingleton R₁⁰ x / spanSingleton R₁⁰ y = spanSingleton R₁⁰ (x / y) := by
   rw [div_spanSingleton, mul_comm, spanSingleton_mul_spanSingleton, div_eq_mul_inv]
@@ -1058,7 +1057,6 @@ variable [IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J)
 
 /-- The bijection between ideals of `R` dividing `I` and the ideals of `A` dividing `J` induced by
   an isomorphism `f : R/I ≅ A/J`. -/
--- @[simps] -- Porting note: simpNF complains about the lemmas generated by simps
 def idealFactorsEquivOfQuotEquiv : { p : Ideal R | p ∣ I } ≃o { p : Ideal A | p ∣ J } := by
   have f_surj : Function.Surjective (f : R ⧸ I →+* A ⧸ J) := f.surjective
   have fsym_surj : Function.Surjective (f.symm : A ⧸ J →+* R ⧸ I) := f.symm.surjective
@@ -1101,7 +1099,6 @@ theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFact
 
 /-- The bijection between the sets of normalized factors of I and J induced by a ring
     isomorphism `f : R/I ≅ A/J`. -/
--- @[simps apply] -- Porting note: simpNF complains about the lemmas generated by simps
 def normalizedFactorsEquivOfQuotEquiv (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     { L : Ideal R | L ∈ normalizedFactors I } ≃ { M : Ideal A | M ∈ normalizedFactors J } where
   toFun j :=
@@ -1379,7 +1376,6 @@ variable [NormalizationMonoid R]
 
 /-- The bijection between the (normalized) prime factors of `r` and the (normalized) prime factors
     of `span {r}` -/
--- @[simps] -- Porting note: simpNF complains about the lemmas generated by simps
 noncomputable def normalizedFactorsEquivSpanNormalizedFactors {r : R} (hr : r ≠ 0) :
     { d : R | d ∈ normalizedFactors r } ≃
       { I : Ideal R | I ∈ normalizedFactors (Ideal.span ({r} : Set R)) } := by