From 7b8e51e025b887135ae4e9080753807b4ae9df9f Mon Sep 17 00:00:00 2001
From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com>
Date: Mon, 15 Dec 2025 12:23:25 -0500
Subject: [PATCH] fix: missing word in inductionWithNoAlts error message
 (#11684)

This PR adds a missing word ("be") to the error message catching
natural-numbers-game-like uses of induction that was introduced in
#11347.
---
 src/Lean/Elab/Tactic/Induction.lean                | 2 +-
 tests/lean/notNaturalNumbersGame.lean.expected.out | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 443490300a..a7fb99d70a 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -665,7 +665,7 @@ def checkForInductionWithNoAlts (tacticKind : String) (optInductionAlts : Syntax
     -- Usually errors are suppressed for syntax containing `.missing` nodes, but this named error is
     -- listed in `Lean.Core.getAndEmptySnapshotTasks` as an error that ignores suppression.
     throwNamedErrorAt optInductionAlts lean.inductionWithNoAlts
-      m!"Invalid syntax for {tacticKind} tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `{var}`."
+      m!"Invalid syntax for {tacticKind} tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `{var}`."
 
 /--
 Separate out the optional `with` tactics from the rest of the alternates
diff --git a/tests/lean/notNaturalNumbersGame.lean.expected.out b/tests/lean/notNaturalNumbersGame.lean.expected.out
index 1df70b8e83..fcd42c748e 100644
--- a/tests/lean/notNaturalNumbersGame.lean.expected.out
+++ b/tests/lean/notNaturalNumbersGame.lean.expected.out
@@ -1,7 +1,7 @@
 notNaturalNumbersGame.lean:6:20: error: unknown tactic
-notNaturalNumbersGame.lean:6:14-6:20: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
+notNaturalNumbersGame.lean:6:14-6:20: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
 notNaturalNumbersGame.lean:13:16: error: unknown tactic
-notNaturalNumbersGame.lean:13:10-13:16: error(lean.inductionWithNoAlts): Invalid syntax for case analysis tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
+notNaturalNumbersGame.lean:13:10-13:16: error(lean.inductionWithNoAlts): Invalid syntax for case analysis tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
 notNaturalNumbersGame.lean:22:2-22:11: error: Alternative `zero` has not been provided
 notNaturalNumbersGame.lean:22:2-22:11: error: Alternative `succ` has not been provided
 notNaturalNumbersGame.lean:25:2-25:7: error: Alternative `zero` has not been provided