fix: fun_induction rejecting names for all hypotheses with let and generalizing (#14475)

This PR fixes a spurious "Too many variable names provided" error from
`fun_induction` (and `induction`/`cases`) when an alternative had a
`let`-bound field, so that all hypotheses of such an alternative can now
be named.

The error came from `getNumExplicitFields`, which counted nameable
fields with a telescope that reduces `let` bindings away and then
over-reads into later binders, disagreeing with the `introN` that
actually names them. It now introduces the fields via the same `introN`
path and counts the explicit (and `let`-bound) ones, so the count and
the naming can no longer diverge.

Fixes: #14472

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

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

Author: nomeata

src/Lean/Elab/Tactic/Induction.lean

@@ -311,20 +311,19 @@ def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit
       else
         throwOrLogErrorAt altStx m!"Invalid alternative name `{altName}`: {msg}"
 
-/-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
-    return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can
-    be named by the user. -/
-def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do
-  let target ← altMVarId.getType
+/-- Given the goal `altMVarId` for an alternative that introduces `numFields` new variables, return
+    how many the user can name when the `@` modifier is absent: the explicit and the `let`-bound
+    ones (`introN` names `let`-bound binders as explicit). -/
+def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat :=
   withoutModifyingState do
-    -- The `numFields` count includes explicit, implicit and let-bound variables.
-    -- `forallMetaBoundTelescope` will reduce let-bindings, so we don't just count how many
-    -- explicit binders are in `bis`, but how many implicit ones.
-    -- If this turns out to be insufficient, then the real (and complicated) logic for which
-    -- arguments are explicit or implicit can be found in `introNImp`,
-    let (_, bis, _) ← forallMetaBoundedTelescope target numFields
-    let numImplicits := (bis.filter (!·.isExplicit)).size
-    return numFields - numImplicits
+    -- Introduce the fields as the subsequent `introN` will, so the two agree on which are nameable.
+    let (fvarIds, altMVarId) ← altMVarId.introN numFields
+    altMVarId.withContext do
+      let mut numExplicit := 0
+      for fvarId in fvarIds do
+        if (← fvarId.getDecl).binderInfo.isExplicit then
+          numExplicit := numExplicit + 1
+      return numExplicit
 
 def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TermElabM Unit :=
   withSaveInfoContext <| altMVarId.withContext do

tests/elab/issue14472.lean

@@ -0,0 +1,38 @@
+/-!
+Tests that `fun_induction` allows naming all hypotheses of an alternative when the
+combination of a `generalizing` clause, a `let` binding in the pattern, and structural
+recursion previously caused a spurious "Too many variable names provided" error (#14472).
+-/
+
+def f (x : Nat) : Nat :=
+  match x with
+  | 0 => 0
+  | n + 1 =>
+    let i := 0
+    f (n + i)
+
+-- Naming all three fields (`n`, the `let`-bound `i`, and the induction hypothesis `ih`) is
+-- accepted; each name refers to the expected hypothesis in the reported state.
+/--
+trace: case case2
+n : Nat
+i : Nat := 0
+ih : ∀ {y : Nat}, f n = 0
+y : Nat
+⊢ f (n + i) = 0
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+example {x y : Nat} : f x = 0 := by
+  fun_induction f generalizing y with
+  | case1 => simp
+  | case2 n i ih => trace_state; sorry
+
+-- Providing more names than there are fields is still rejected, now with the correct count.
+/-- error: Too many variable names provided at alternative `case2`: 4 provided, but 3 expected -/
+#guard_msgs in
+example {x y : Nat} : f x = 0 := by
+  fun_induction f generalizing y with
+  | case1 => simp
+  | case2 n i ih extra => sorry