diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
index 0261d106b1..6cbb6b016e 100644
--- a/src/Init/Lean/Elab/Tactic.lean
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -9,3 +9,4 @@ import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.Tactic.ElabTerm
 import Init.Lean.Elab.Tactic.Induction
 import Init.Lean.Elab.Tactic.Generalize
+import Init.Lean.Elab.Tactic.Injection
diff --git a/src/Init/Lean/Elab/Tactic/Injection.lean b/src/Init/Lean/Elab/Tactic/Injection.lean
new file mode 100644
index 0000000000..0ce5dc6419
--- /dev/null
+++ b/src/Init/Lean/Elab/Tactic/Injection.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Tactic.Injection
+import Init.Lean.Elab.Tactic.ElabTerm
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+-- optional (" with " >> many1 ident')
+private def getInjectionNewIds (stx : Syntax) : List Name :=
+if stx.isNone then []
+else (stx.getArg 1).getArgs.toList.map Syntax.getId
+
+@[builtinTactic «injection»] def evalInjection : Tactic :=
+fun stx => do
+  -- parser! nonReservedSymbol "injection " >> termParser >> withIds
+  fvarId ← elabAsFVar (stx.getArg 1);
+  let ids := getInjectionNewIds (stx.getArg 2);
+  liftMetaTactic stx $ fun mvarId => do
+    r ← Meta.injection mvarId fvarId ids (!ids.isEmpty);
+    match r with
+    | Meta.InjectionResult.solved             => pure []
+    | Meta.InjectionResult.subgoal mvarId _ _ => pure [mvarId]
+
+end Tactic
+end Elab
+end Lean