diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index f87663e719..e817d726e1 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -45,6 +45,8 @@ def usingRec : Parser := optional (" using " >> ident)
 def generalizingVars := optional (" generalizing " >> many1 ident)
 @[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
 @[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
+def withIds : Parser := optional (" with " >> many1 ident')
+@[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
 @[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"