grind? drops inj params

grind? [inj thm] proves the goal but suggests plain grind only, which fails on paste.

`
def f (n : Nat) := n + 3

theorem f_inj : Function.Injective f := by
intro a b h
simp [f] at h
omega

-- Closes the goal, but suggests grind only — the inj f_inj parameter is dropped:
example (a b : Nat) (h : f a = f b) : a = b := by grind? [inj f_inj]

-- Pasting the suggestion fails:
example (a b : Nat) (h : f a = f b) : a = b := by grind only
`

Start by running the two reproducer examples in the issue, comparing the successful grind? [inj f_inj] invocation with the failing suggested grind only. Trace the grind? suggestion entry point and verify that the completed suggestion preserves the inj f_inj parameter and can be pasted successfully.