chore: remove redudant nolint simpNF (leanprover-community#40680)

felixpernegger · ReemMelamed · commit 63dd3c95da66 · 2026-06-20T15:20:05.000+03:00
Remove the attribute whenever its redundant. Some of this comes from leanprover-community#23201, not sure about why others work. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
diff --git a/Mathlib/Algebra/Group/Subgroup/Map.lean b/Mathlib/Algebra/Group/Subgroup/Map.lean
@@ -158,11 +158,7 @@ theorem mem_map_equiv {f : G ≃* N} {K : Subgroup G} {x : N} :
     x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K :=
   Set.mem_image_equiv
 
--- The simpNF linter says that the LHS can be simplified via `Subgroup.mem_map`.
--- However this is a higher priority lemma.
--- It seems the side condition `hf` is not applied by `simpNF`.
--- https://github.com/leanprover/std4/issues/207
-@[to_additive (attr := simp 1100, nolint simpNF)]
+@[to_additive (attr := simp 1100)]
 theorem mem_map_iff_mem {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
     f x ∈ K.map f ↔ x ∈ K :=
   hf.mem_set_image
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -235,11 +235,7 @@ theorem apply_coe_mem_map (f : F) (S : Submonoid M) (x : S) : f x ∈ S.map f :=
 theorem map_map (g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f) :=
   SetLike.coe_injective <| image_image _ _ _
 
--- The simpNF linter says that the LHS can be simplified via `Submonoid.mem_map`.
--- However this is a higher priority lemma.
--- It seems the side condition `hf` is not applied by `simpNF`.
--- https://github.com/leanprover/std4/issues/207
-@[to_additive (attr := simp 1100, nolint simpNF)]
+@[to_additive (attr := simp 1100)]
 theorem mem_map_iff_mem {f : F} (hf : Function.Injective f) {S : Submonoid M} {x : M} :
     f x ∈ S.map f ↔ x ∈ S :=
   hf.mem_set_image
diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -70,20 +70,16 @@ the category `C` -/
 def ιPaths (X : C) : Paths (LocQuiver W) :=
   ⟨X⟩
 
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
 /-- The morphism in the path category associated to a morphism in the original category. -/
-@[simp, nolint simpNF]
+@[simp]
 def ψ₁ {X Y : C} (f : X ⟶ Y) : ιPaths W X ⟶ ιPaths W Y := (Paths.of _).map (Sum.inl f)
 
 #adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
 Assistance investigating this would be appreciated. -/
 attribute [nolint simpNF] ψ₁.eq_1
 
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
 /-- The morphism in the path category corresponding to a formal inverse. -/
-@[simp, nolint simpNF]
+@[simp]
 def ψ₂ {X Y : C} (w : X ⟶ Y) (hw : W w) : ιPaths W Y ⟶ ιPaths W X :=
   (Paths.of _).map (Sum.inr ⟨w, hw⟩)
 
diff --git a/Mathlib/CategoryTheory/PathCategory/Basic.lean b/Mathlib/CategoryTheory/PathCategory/Basic.lean
@@ -247,11 +247,9 @@ def pathComposition : Paths C ⥤ C where
 -- the `HomRel` for the kernel of any functor.
 -- Indeed, this should be part of an equivalence between congruence relations on a category `C`
 -- and full, essentially surjective functors out of `C`.
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
 /-- The canonical relation on the path category of a category:
 two paths are related if they compose to the same morphism. -/
-@[simp, nolint simpNF]
+@[simp]
 def pathsHomRel : HomRel (Paths C) := fun _ _ p q =>
   (pathComposition C).map p = (pathComposition C).map q
 
diff --git a/Mathlib/CategoryTheory/WithTerminal/Basic.lean b/Mathlib/CategoryTheory/WithTerminal/Basic.lean
@@ -83,10 +83,8 @@ def id : ∀ X : WithTerminal C, Hom X X
   | of _ => 𝟙 _
   | star => PUnit.unit
 
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
 /-- Composition of morphisms for `WithTerminal C`. -/
-@[simp, nolint simpNF]
+@[simp]
 def comp : ∀ {X Y Z : WithTerminal C}, Hom X Y → Hom Y Z → Hom X Z
   | of _X, of _Y, of _Z => fun f g => f ≫ g
   | of _X, _, star => fun _f _g => PUnit.unit
diff --git a/Mathlib/Data/Multiset/MapFold.lean b/Mathlib/Data/Multiset/MapFold.lean
@@ -142,11 +142,7 @@ theorem map_eq_cons [DecidableEq α] (f : α → β) (s : Multiset α) (t : Mult
     refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
     rw [Multiset.erase_cons_head, h]
 
--- The simpNF linter says that the LHS can be simplified via `Multiset.mem_map`.
--- However this is a higher priority lemma.
--- It seems the side condition `H` is not applied by `simpNF`.
--- https://github.com/leanprover/std4/issues/207
-@[simp 1100, nolint simpNF]
+@[simp 1100]
 theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} :
     f a ∈ map f s ↔ a ∈ s :=
   Quot.inductionOn s fun _l => List.mem_map_of_injective H
diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean
@@ -47,11 +47,7 @@ theorem coe_def : (fun a ↦ ↑a : α → Option α) = some :=
 
 theorem mem_map {f : α → β} {y : β} {o : Option α} : y ∈ o.map f ↔ ∃ x ∈ o, f x = y := by simp
 
--- The simpNF linter says that the LHS can be simplified via `Option.mem_def`.
--- However this is a higher priority lemma.
--- It seems the side condition `H` is not applied by `simpNF`.
--- https://github.com/leanprover/std4/issues/207
-@[simp 1100, nolint simpNF]
+@[simp 1100]
 theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {o : Option α} :
     f a ∈ o.map f ↔ a ∈ o := by
   aesop
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -287,14 +287,14 @@ protected theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := b
 @[simp] theorem rank_bot' : Module.rank (⊥ : IntermediateField F E) E = Module.rank F E := by
   rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
 
-@[simp, nolint simpNF] -- `simpNF` hits a (deterministic) timeout at `typeclass`
+@[simp]
 theorem finrank_bot' : finrank (⊥ : IntermediateField F E) E = finrank F E :=
   congr(Cardinal.toNat $(rank_bot'))
 
 @[simp] protected theorem rank_top : Module.rank (⊤ : IntermediateField F E) E = 1 :=
   Subalgebra.bot_eq_top_iff_rank_eq_one.mp <| top_le_iff.mp fun x _ ↦ ⟨⟨x, trivial⟩, rfl⟩
 
-@[simp, nolint simpNF] -- `simpNF` hits a (deterministic) timeout at `typeclass`
+@[simp]
 protected theorem finrank_top : finrank (⊤ : IntermediateField F E) E = 1 :=
   rank_eq_one_iff_finrank_eq_one.mp IntermediateField.rank_top
 
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
@@ -346,13 +346,11 @@ theorem changeFormEquiv_symm :
 
 variable (Q)
 
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
 /-- The module isomorphism to the exterior algebra.
 
 Note that this holds more generally when `Q` is divisible by two, rather than only when `1` is
 divisible by two; but that would be more awkward to use. -/
-@[simp, nolint simpNF]
+@[simp]
 def equivExterior [Invertible (2 : R)] : CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M :=
   changeFormEquiv changeForm.associated_neg_proof
 
diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean
@@ -135,7 +135,7 @@ language. -/
 @[simps] def orderLHom : Language.order →ᴸ L where
   onRelation | _, .le => leSymb
 
-@[simp, nolint simpNF]
+@[simp]
 theorem orderLHom_leSymb :
     (orderLHom L).onRelation leSymb = (leSymb : L.Relations 2) :=
   rfl
diff --git a/Mathlib/Order/Filter/Map.lean b/Mathlib/Order/Filter/Map.lean
@@ -60,11 +60,7 @@ theorem mem_map' : t ∈ map m f ↔ { x | m x ∈ t } ∈ f :=
 theorem image_mem_map (hs : s ∈ f) : m '' s ∈ map m f :=
   f.sets_of_superset hs <| subset_preimage_image m s
 
--- The simpNF linter says that the LHS can be simplified via `Filter.mem_map`.
--- However this is a higher priority lemma.
--- It seems the side condition `hf` is not applied by `simpNF`.
--- https://github.com/leanprover/std4/issues/207
-@[simp 1100, nolint simpNF]
+@[simp 1100]
 theorem image_mem_map_iff (hf : Injective m) : m '' s ∈ map m f ↔ s ∈ f :=
   ⟨fun h => by rwa [← preimage_image_eq s hf], image_mem_map⟩
 
diff --git a/Mathlib/RingTheory/Extension/Generators.lean b/Mathlib/RingTheory/Extension/Generators.lean
@@ -639,18 +639,14 @@ lemma ker_naive {σ : Type*} {I : Ideal (MvPolynomial σ R)}
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
--- FIXME: `simpNF` times out synthesizing
--- `FaithfulSMul (Algebra.Generators.ofAlgHom f h).toExtension.Ring S`.
-@[simp, nolint simpNF]
+@[simp]
 lemma ker_ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f) :
     (ofAlgHom f h).ker = RingHom.ker f.toRingHom := by
   change RingHom.ker _ = _
   congr
   exact MvPolynomial.ringHom_ext (by simp) (by simp [ofAlgHom])
 
--- FIXME: `simpNF` times out synthesizing
--- `FaithfulSMul (P.ofAlgEquiv e).toExtension.Ring T`.
-@[simp, nolint simpNF]
+@[simp]
 lemma ker_ofAlgEquiv (P : Generators R S ι) {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
     (P.ofAlgEquiv e).ker = P.ker := by
   rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
diff --git a/Mathlib/Topology/MetricSpace/Snowflaking.lean b/Mathlib/Topology/MetricSpace/Snowflaking.lean
@@ -84,7 +84,7 @@ theorem toSnowflaking.sizeOf_spec [SizeOf X] (x : X) :
     sizeOf (toSnowflaking x : Snowflaking X α hα₀ hα₁) = 1 + sizeOf x :=
   rfl
 
-attribute [nolint simpNF] mk.injEq mk.sizeOf_spec
+attribute [nolint simpNF] mk.injEq
 
 /-- This definition makes `cases x` and `induction x` use `toSnowflaking` instead of `mk`. -/
 @[elab_as_elim, cases_eliminator, induction_eliminator]
