diff --git a/Mathlib.lean b/Mathlib.lean
index 8bccdc69eab4..519560c2d429 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -116,6 +116,7 @@ import Mathlib.Tactic.Simpa
 import Mathlib.Tactic.Simps
 import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.Spread
+import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
 import Mathlib.Tactic.ToAdditive
diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
index 224e4b035d98..d9bcbe2f95e9 100644
--- a/Mathlib/Mathport/Syntax.lean
+++ b/Mathlib/Mathport/Syntax.lean
@@ -29,6 +29,7 @@ import Mathlib.Tactic.ShowTerm
 import Mathlib.Tactic.Simps
 import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.Trace
+import Mathlib.Tactic.Substs
 import Mathlib.Init.ExtendedBinder
 import Mathlib.Util.WithWeakNamespace
 import Mathlib.Util.Syntax
@@ -244,7 +245,6 @@ end Conv
 /- M -/ syntax (name := injectionsAndClear) "injections_and_clear" : tactic
 
 /- E -/ syntax (name := tryFor) "try_for " term:max tacticSeq : tactic
-/- E -/ syntax (name := substs) "substs" (ppSpace ident)* : tactic
 /- E -/ syntax (name := unfoldCoes) "unfold_coes" (ppSpace location)? : tactic
 /- E -/ syntax (name := unfoldWf) "unfold_wf" : tactic
 /- M -/ syntax (name := unfoldAux) "unfold_aux" : tactic
diff --git a/Mathlib/Tactic/Substs.lean b/Mathlib/Tactic/Substs.lean
new file mode 100644
index 000000000000..74841efdbbbf
--- /dev/null
+++ b/Mathlib/Tactic/Substs.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2022 Evan Lohn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Evan Lohn, Mario Carneiro
+-/
+import Lean
+
+namespace Mathlib.Tactic.Substs
+open Lean Meta Elab
+open Tactic
+
+/--
+Applies the `subst` tactic to all given hypotheses from left to right.
+-/
+syntax (name := substs) "substs" (colGt ppSpace ident)* : tactic
+
+macro_rules
+| `(tactic| substs $xs:ident*) => `(tactic| ($[subst $xs;]*))