`grind?+suggestions` suggests using subproofs of other theorems with module system

Prerequisites

• [ X] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ X] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ X] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following grind+suggestions and consequently try? will suggest to use

info: Try these:
  [apply] grind only [lemma_with_subproof._proof_1_1]
  [apply] grind => instantiate only [lemma_with_subproof._proof_1_1]

module -- leaving out module will produce a `[apply] grind => sorry` at the `grind`+suggestions` instead (as expected)
public import Lean.LibrarySuggestions.Default

inductive Leq : Nat → Nat → Prop where
  | refl : Leq n n
  | step : Leq n m → Leq n (m + 1)

theorem lemma_with_subproof : Leq 2 0 → Leq 3 0  := by
  have : True := by solve_by_elim
  intro h2_0
  have : False := by
    have : Leq 1 0 := by
      cases h2_0
    grind [Leq]
  exact False.elim this

/-- info: lemma_with_subproof._proof_1_1 (this : Leq 1 0) : False -/
#guard_msgs in
#check lemma_with_subproof._proof_1_1



/--
info: Try these:
  [apply] grind only [lemma_with_subproof._proof_1_1]
  [apply] grind => instantiate only [lemma_with_subproof._proof_1_1]
-/
#guard_msgs in
theorem l : Leq 1 0 → False := by
  intro h
  grind?+suggestions



/--
info: Lean 4.29.0
Target: x86_64-unknown-linux-gnu
-/
#guard_msgs in
#version

I have also similarily seen mytheorem._simp_1_5 be suggested

Context

Also see https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Proof-dependant.20grind.20proofs/with/582789828

Having proofs depend on subproofs of other theorems is very brittle and should not be suggested.
Sometimes the used subproofs are trivial but try? is content with what it found, shortcuircits and doesn't find the otherwise trivial (non-brittle) proof.

However sometimes the used subproofs are also interesting as they might suggest that a lemma is missing.
It is much more important that these subproofs aren't suggested if a better proof can be found by trying a bit longer, but in the case this fails it would be interesting to report something like

try? found the following bad (proof dependent) proof:
....
It is using the subproofs:
...
Maybe one of these is an interesting lemma you are missing?

Versions

Lean 4.29.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the self-contained module example with grind?+suggestions and try?, then inspect the suggestion path used by Lean.LibrarySuggestions.Default. Trace how generated subproofs such as lemma_with_subproof._proof_1_1 and mytheorem._simp_1_5 enter suggestions. Done means proof-dependent subproofs are no longer suggested, while the reported behavior matches the issue's intended handling of potentially useful missing lemmas.