feat: add grind option abstractProof (#9574)

This PR adds the option `abstractProof` to control whether `grind`
automatically creates an auxiliary theorem for the generated proof or
not.

src/Init/Grind/Tactics.lean

@@ -120,6 +120,10 @@ structure Config where
   the characteristic of a ring.
   -/
   exp : Nat := 2^20
+  /--
+  When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
+  -/
+  abstractProof := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Lean/Elab/Tactic/Grind.lean

@@ -161,8 +161,10 @@ def grind
     if result.hasFailed then
       throwError "`grind` failed\n{← result.toMessageData}"
     trace[grind.debug.proof] "{← instantiateMVars mvar'}"
-    -- `grind` proofs are often big
-    let e ← if (← isProp type) then
+    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
+    let e ← if !config.abstractProof then
+      instantiateMVarsProfiling mvar'
+    else if (← isProp type) then
       mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
     else
       let auxName ← Term.mkAuxName `grind