feat: extract_goal preserves explicit foralls (#31342)

* feat: extract_goal preserves explicit foralls

* fix: update goalSignature call for new return type

The goalSignature function now returns a 4-tuple including a boolean
for hasOriginalForalls. Update the destructuring pattern in
TacticAnalysis/Declarations.lean to account for this new field.

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

Co-Authored-By: Claude <noreply@anthropic.com>

---------

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

Author: kim-em

Mathlib/Tactic/ExtractGoal.lean

@@ -143,10 +143,19 @@ The return values are:
 * A formatted piece of `MessageData`, like `m!"myTheorem (a b : Nat) : a + b = b + a"`.
 * The full type of the declaration, like `∀ a b, a + b = b + a`.
 * The imports needed to state this declaration, as an array of module names.
+* A boolean indicating whether the original goal type had top-level foralls.
 -/
-def goalSignature (name : Name) (g : MVarId) : TermElabM (MessageData × Expr × Array Name) :=
+def goalSignature (name : Name) (g : MVarId) : TermElabM (MessageData × Expr × Array Name × Bool) :=
   withoutModifyingEnv <| withoutModifyingState do
     let (g, _) ← g.renameInaccessibleFVars
+    -- Check if the original goal has foralls before reverting
+    -- We only consider it to have "original foralls" if it has a named forall,
+    -- not just implications (which have anonymous or internal hygienic names)
+    let originalTy ← instantiateMVars (← g.getType)
+    let hasOriginalForalls :=
+      originalTy.isForall &&
+      !originalTy.bindingName!.isAnonymous &&
+      !originalTy.bindingName!.isInternal
     let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
     let ty ← instantiateMVars (← g.getType)
     if ty.hasExprMVar then
@@ -179,7 +188,7 @@ def goalSignature (name : Name) (g : MVarId) : TermElabM (MessageData × Expr ×
       if !fins.contains new then fins := fins.insert new
     let tot := Mathlib.Command.MinImports.getIrredundantImports (← getEnv) (fins.erase .anonymous)
     let fileNames := tot.toArray.qsort Name.lt
-    return (sig, ty, fileNames)
+    return (sig, ty, fileNames, hasOriginalForalls)
 
 elab_rules : tactic
   | `(tactic| extract_goal $cfg:config $[using $name?]?) => do
@@ -200,9 +209,15 @@ elab_rules : tactic
           -- Note: `getFVarIds` does `withMainContext`
           g.cleanup (toPreserve := (← getFVarIds fvars)) (indirectProps := false)
         | _ => throwUnsupportedSyntax
-      let (sig, ty, _) ← goalSignature name g
+      let (sig, ty, _, hasOriginalForalls) ← goalSignature name g
       let cmd := if ← Meta.isProp ty then "theorem" else "def"
-      pure m!"{cmd} {sig} := sorry"
+      let msg ← if hasOriginalForalls then
+        -- Preserve foralls: format as "theorem name : ty := sorry"
+        pure m!"{cmd} {name} : {ty} := sorry"
+      else
+        -- Convert foralls to parameters: format using signature
+        pure m!"{cmd} {sig} := sorry"
+      pure msg
     logInfo msg
 
 end Mathlib.Tactic.ExtractGoal

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -64,7 +64,7 @@ def terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind :
     catch _e =>
       let name ← mkAuxDeclName `extracted
       -- Rerun in the original tactic context, since `omega` changes the state.
-      let ((sig, _, modules), _) ← ctxI.runTactic i goal (fun goal =>
+      let ((sig, _, modules, _), _) ← ctxI.runTactic i goal (fun goal =>
         (Mathlib.Tactic.ExtractGoal.goalSignature name goal).run)
       let imports := modules.toList.map (s!"import {·}")
       return .error tac m!"{"\n".intercalate imports}\n\ntheorem {sig} := by\n  fail_if_success {tac}\n  {stx}"

MathlibTest/ExtractGoal.lean

@@ -175,3 +175,19 @@ example : ∀ n, n < n + 1 := by
   have : m < _ := Nat.lt_succ_of_lt (Nat.lt_add_one m)
   extract_goal
   sorry
+
+/--
+info: theorem foralls_variants.extracted_1_1 : ∀ (n : ℕ), n + 0 = n → n + 1 + 0 = n + 1 := sorry
+---
+info: theorem foralls_variants.extracted_1_3 (n : ℕ) : n + 0 = n → n + 1 + 0 = n + 1 := sorry
+-/
+#guard_msgs in
+theorem foralls_variants : ∀ (n : Nat), n + 0 = n := by
+  intro n
+  have step1 : ∀ n, n + 0 = n → (n + 1) + 0 = n + 1 := by
+    extract_goal
+    simp
+  have step2 : n + 0 = n → (n + 1) + 0 = n + 1 := by
+    extract_goal
+    simp
+  simp