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