feat: add reprove command for re-proving theorems with a specified tactic (#10434)

This PR adds `reprove N by T`, which effectively elaborates `example
type_of% N := by T`. It supports multiple identifiers. This is useful
for testing tactics.


🤖 Generated with [Claude Code](https://claude.ai/code)

---------

Co-authored-by: Claude <noreply@anthropic.com>

src/Lean/Util.lean

@@ -38,5 +38,6 @@ public import Lean.Util.NumObjs
 public import Lean.Util.NumApps
 public import Lean.Util.FVarSubset
 public import Lean.Util.SortExprs
+public import Lean.Util.Reprove
 
 public section

src/Lean/Util/Reprove.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public meta import Lean.Elab.Command
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Term
+
+/-!
+# The `reprove` command
+
+This command reproves a list of declarations with a given tactic sequence.
+It is useful for testing tactics.
+-/
+
+public section
+
+namespace Lean.Elab.Command
+
+open Meta
+
+/-- Reproving a declaration with a given tactic sequence -/
+meta def reproveDecl (declName : Name) (tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq) : CommandElabM Unit := do
+  let some info := (← getEnv).find? declName
+    | throwError "unknown declaration '{declName}'"
+
+  let uniqueName ← liftCoreM <| mkFreshUserName `reprove_example
+
+  let value ← liftTermElabM do
+    Term.withDeclName uniqueName do
+      let goal ← mkFreshExprMVar info.type
+      let goalMVar := goal.mvarId!
+      let _goals ← Tactic.run goalMVar do
+        Tactic.evalTactic tacticSeq
+      instantiateMVars goal
+
+  let decl := Declaration.defnDecl {
+    name := uniqueName
+    type := info.type
+    value := value
+    levelParams := info.levelParams
+    hints := ReducibilityHints.opaque
+    safety := DefinitionSafety.safe
+  }
+
+  liftCoreM <| addAndCompile decl
+
+/--
+Reproves a list of declarations with a given tactic sequence.
+
+```lean
+reprove theorem1 theorem2 theorem3 by simp
+```
+-/
+syntax (name := reprove) "reprove " ident+ " by " tacticSeq : command
+
+@[command_elab «reprove»]
+meta def elabReprove : CommandElab := fun stx => do
+  let identStxs := stx[1].getArgs
+  let tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨stx[3]⟩
+  for identStx in identStxs do
+    let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo identStx
+    reproveDecl declName tacticSeq
+
+end Lean.Elab.Command

tests/lean/run/reprove.lean

@@ -0,0 +1,109 @@
+import Lean.Util.Reprove
+
+-- Test successful reprove
+theorem simpleTheorem : 1 + 1 = 2 := rfl
+
+reprove simpleTheorem by rfl
+
+theorem withTactics : ∀ n : Nat, n + 0 = n := by
+  intro n
+  rw [Nat.add_zero]
+
+reprove withTactics by
+  intro n
+  simp
+
+reprove List.append_nil by
+  intro l
+  simp
+
+-- Test failed reprove - wrong tactic
+/--
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+reprove simpleTheorem by
+  sorry
+
+-- Test failed reprove - incomplete proof
+/-- error: (kernel) declaration has metavariables 'reprove_example✝' -/
+#guard_msgs in
+reprove withTactics by
+  intro n
+
+-- Test unknown declaration
+/--
+error: Unknown constant `nonExistentTheorem`
+-/
+#guard_msgs in
+reprove nonExistentTheorem by
+  simp
+
+-- Test with a non-propositional type (creates example that succeeds)
+def natValue : Nat := 42
+
+reprove natValue by
+  exact 42
+
+-- Test with wrong proof
+/--
+error: Type mismatch
+  "hello"
+has type
+  String
+but is expected to have type
+  Nat
+-/
+#guard_msgs in
+reprove natValue by
+  exact "hello"
+
+-- Test complex type with implicit arguments
+theorem hasImplicits {α : Type} (xs : List α) : xs.length ≥ 0 := by simp
+
+reprove hasImplicits by simp
+
+-- Test multiple declarations in one command
+theorem theorem1 : 2 + 2 = 4 := by simp
+theorem theorem2 : 3 + 3 = 6 := by simp
+theorem theorem3 : 4 + 4 = 8 := by simp
+
+reprove theorem1 theorem2 theorem3 by simp
+
+-- Test namespace functionality
+namespace Test
+
+theorem namespaceTheorem : 5 + 5 = 10 := by simp
+
+end Test
+
+open Test
+
+reprove namespaceTheorem by simp
+
+-- Test multiple declarations where one fails due to unknown name
+/--
+error: Unknown constant `unknownTheorem`
+-/
+#guard_msgs in
+reprove
+  theorem1
+  unknownTheorem
+  theorem2
+by simp
+
+-- Test multiple declarations where tactic fails for one
+theorem needsIntro : ∀ n : Nat, n = n := fun _ => rfl
+theorem simpleEq : 1 = 1 := rfl
+
+/--
+error: Tactic `rfl` failed: Expected the goal to be a binary relation
+
+Hint: Reflexivity tactics can only be used on goals of the form `x ~ x` or `R x x`
+
+⊢ ∀ (n : Nat), n = n
+-/
+#guard_msgs in
+reprove simpleEq needsIntro simpleTheorem by rfl
+
+reprove Array.attach_empty by grind