feat: do not report metaprogramming declarations via exact? and rw?

src/Lean/Data/Name.lean

@@ -184,6 +184,11 @@ def anyS (n : Name) (f : String → Bool) : Bool :=
   | .num p _ => p.anyS f
   | _ => false
 
+/-- Return true if the name is in a namespace associated to metaprogramming.-/
+def isMetaprogramming (n : Name) : Bool :=
+  let components := n.components
+  components.head? == `Lean || (components.any fun n => n == `Tactic || n == `Linter)
+
 end Name
 end Lean
 

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -71,12 +71,14 @@ open LazyDiscrTree (InitEntry findMatches)
 
 private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × DeclMod))) :=
+  -- Don't report lemmas from metaprogramming namespaces.
+  if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do
     let e ← InitEntry.fromExpr type (name, DeclMod.none)
     let a := #[e]
     if e.key == .const ``Iff 2 then
-      let a := a.push (←e.mkSubEntry 0 (name, DeclMod.mp))
-      let a := a.push (←e.mkSubEntry 1 (name, DeclMod.mpr))
+      let a := a.push (← e.mkSubEntry 0 (name, DeclMod.mp))
+      let a := a.push (← e.mkSubEntry 1 (name, DeclMod.mpr))
       pure a
     else
       pure a

src/Lean/Meta/Tactic/Rewrites.lean

@@ -44,11 +44,11 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
   if constInfo.isUnsafe then return #[]
   if !allowCompletion (←getEnv) name then return #[]
   -- We now remove some injectivity lemmas which are not useful to rewrite by.
-  if name matches .str _ "injEq" then return #[]
-  if name matches .str _ "sizeOf_spec" then return #[]
   match name with
-  | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
+  | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
   | _ => pure ()
+  -- Don't report lemmas from metaprogramming namespaces.
+  if name.isMetaprogramming then return #[]
   withNewMCtxDepth do withReducible do
     forallTelescopeReducing constInfo.type fun _ type => do
       match type.getAppFnArgs with

tests/lean/librarySearch.lean

@@ -275,3 +275,9 @@ error: apply? didn't find any relevant lemmas
 -/
 #guard_msgs in
 example {α : Sort u} (x y : α) : Eq x y := by apply?
+
+-- If this lemmas is added later to the library, please update this `#guard_msgs`.
+-- The point of this test is to ensure that `Lean.Grind.not_eq_prop` is not reported to users.
+/-- error: `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/
+#guard_msgs in
+example (p q : Prop) : (¬ p = q) = (p = ¬ q) := by exact?