feat: generate instantiate only [...] at finish?

[leodemoura]

This PR improves the grind tactic generated by the instantiate action in tracing mode. It also updates the syntax for the instantiate tactic, making it similar to simp. For example:

• instantiate only [thm1, thm2] instantiates only theorems thm1 and thm2.
• instantiate [thm1, thm2] instantiates theorems marked with the @[grind] attribute and theorems thm1 and thm2.

The action produces instantiate only [...] tactics. Example:

/--
info: Try this:
  [apply] ⏎
    instantiate only [= Array.getElem_set]
    instantiate only [= Array.getElem_set]
-/
#guard_msgs in
example (as bs cs : Array α) (v₁ v₂ : α)
        (i₁ i₂ j : Nat)
        (h₁ : i₁ < as.size)
        (h₂ : bs = as.set i₁ v₁)
        (h₃ : i₂ < bs.size)
        (h₄ : cs = bs.set i₂ v₂)
        (h₅ : i₁ ≠ j ∧ i₂ ≠ j)
        (h₆ : j < cs.size)
        (h₇ : j < as.size) :
    cs[j] = as[j] := by
  grind => finish?

Recall that finish? replays generated tactics before suggesting them.

The instantiate action inspects the generated proof term to decide which theorems to include as parameters in the instantiate only [...] tactic. However, in some cases, a theorem contributes only by adding a term to the state. In such cases, the generated tactic cannot be fully replayed, and the action uses
instantiate approx [<thms instantiated>] to indicate which parts of the tactic script are approximate. The approx is just a hint for users.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-10-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-20 00:15:12)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-20 00:15:14)