False positives for `tryAtEachStep` linter and `grind +suggestions` tactic

Sometimes when I run tryAtEachStep linter to identify which steps (or multiple subsequent steps) in the proof can be performed by grind +suggestions I encounter false positives: the linter says I can replace a proof step with the tactic, but when I actually replace, the proof does not pass. I think I observed it only for grind +suggestions , other tactics (including grind) do not result in such false positives.

An example: let's say we use Lean and mathlib 4.28.0 and have example.lean with this content:

import Mathlib

set_option linter.tacticAnalysis.tryAtEachStep.selfReplacements false
set_option linter.tacticAnalysis.tryAtEachStepFromEnv true

theorem Munkres_exercise_17_4 {X : Type*} [TopologicalSpace X]
  (U A : Set X) (hU : IsOpen U) (hA : IsClosed A) :
  IsOpen (U \ A) ∧ IsClosed (A \ U) := by
  have h1 : IsOpen (U \ A) := by
    exact IsOpen.inter hU (isOpen_compl_iff.mpr hA)
  have h2 : IsClosed (A \ U) := by
    exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)
  exact ⟨h1, h2⟩

when I run

export TRY_AT_EACH_STEP_TACTIC=grind+suggestions
lake env lean --json example.lean | jq .

I get info with multiple replacement suggestions, in particular :

{
  ...
  "caption": "",
  "data": "`exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)` can be replaced with `grind+suggestions` (76ms)",
  "endPos": {
    "column": 55,
    "line": 12
  },
  "fileName": "example.lean",
  "isSilent": false,
  "keepFullRange": false,
  "kind": "[anonymous]",
  "pos": {
    "column": 4,
    "line": 12
  },
  "severity": "information"
  ...
}

This is saying that the proof of h2 statement may be done just by grind+suggestions. However, when I actually replace this proof step in the file with grind+suggestions, it does not work:

import Mathlib

set_option linter.tacticAnalysis.tryAtEachStep.selfReplacements false
set_option linter.tacticAnalysis.tryAtEachStepFromEnv true

theorem Munkres_exercise_17_4 {X : Type*} [TopologicalSpace X]
  (U A : Set X) (hU : IsOpen U) (hA : IsClosed A) :
  IsOpen (U \ A) ∧ IsClosed (A \ U) := by
  have h1 : IsOpen (U \ A) := by
    exact IsOpen.inter hU (isOpen_compl_iff.mpr hA)
  have h2 : IsClosed (A \ U) := by grind +suggestions
    --exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)
  exact ⟨h1, h2⟩

▼ 11:36-11:54: error:
`grind` failed
case grind.1.1.1.1.1.1.1
X : Type u_1
inst : TopologicalSpace X
U A : Set X
hU : IsOpen U
hA : IsClosed A
h1 : IsOpen (U \ A)
h : ¬IsClosed (A \ U)
w : X
h_2 : ¬∀ (F : Filter X), F.NeBot → F ≤ Filter.principal (A \ U) → F ≤ nhds w → w ∈ A \ U
w_1 : X
h_4 : ¬((∃ᶠ (y : X) in nhds w_1, y ∈ A \ U) → w_1 ∈ A \ U)
w_2 : X
left : ∀ a ∈ nhds w_2, (a ∩ (A \ U)).Nonempty
right : w_2 ∉ A \ U
w_3 : Filter X
h_8 : ¬(w_3.NeBot → w_3 ≤ Filter.principal (A \ U) → w_3 ≤ nhds w → w ∈ A \ U)
w_4 : X
h_10 : ¬(w_4 ∈ closure (A \ U) → w_4 ∈ A \ U)
h_11 : w_1 ∉ A
h_12 : w_2 ∉ A
h_13 : w ∉ A
w_5 : Set X
h_14 : ¬(w_5 ∈ nhds w → (w_5 ∩ A).Nonempty)
w_6 : X
h_15 : (w_6 ∈ closure (A \ U)) = (w_6 ∉ A \ U)
w_7 : Set X
h_16 : ¬(w_7 ∈ nhds w_1 → (w_7 ∩ A).Nonempty)
w_8 : Set X
h_17 : ¬(w_8 ∈ nhds w_2 → (w_8 ∩ A).Nonempty)
h_18 : w_4 ∉ A
left_1 : w_6 ∈ closure (A \ U)
right_1 : w_6 ∉ A \ U
left_2 : A \ U ⊆ A \ U
right_2 : ∀ (x : X), True
w_9 : Set X
h_21 : ¬(w_9 ∈ nhds w_4 → (w_9 ∩ A).Nonempty)
h_22 : w_6 ∉ A
w_10 : Set X
h_23 : ¬(w_10 ∈ nhds w_6 → (w_10 ∩ A).Nonempty)
⊢ False

Any help here would be much appreciated!

Reproduce the report with the provided example.lean, TRY_AT_EACH_STEP_TACTIC=grind+suggestions, and lake env lean --json command, then inspect the tryAtEachStep linter and grind+suggestions behavior. Done means the linter no longer reports a replacement that fails when applied to the h2 proof.