fix: count let-bound variables in induction … with correctly (#5117)

This fixes #5058 and is a follow-up to #3505.

src/Lean/Elab/Tactic/Induction.lean

@@ -220,8 +220,14 @@ private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : Tacti
 private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do
   let target ← altMVarId.getType
   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
-    return bis.foldl (init := 0) fun r bi => if bi.isExplicit then r + 1 else r
+    let numImplicits := (bis.filter (!·.isExplicit)).size
+    return numFields - numImplicits
 
 private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TermElabM Unit :=
   withSaveInfoContext <| altMVarId.withContext do

tests/lean/run/indUsingLet.lean

@@ -12,3 +12,9 @@ example (n : Nat) : n = n := by
   case zero => rfl
   case succ n _h _m _IH =>
     rfl
+
+example (n : Nat) : n = n := by
+  induction n using some_induction with
+  | zero => rfl
+  | succ n _h _m _IH =>
+    rfl