feat: substs tactic (leanprover#314)

Added the substs tactic, which just applies subst to multiple hypotheses at once.

This is my first PR to mathlib; let me know what needs to change!

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

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

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;]*))