feat(library/init/meta/interactive): add interactive tactic subst_vars

doc/changes.md

@@ -100,6 +100,8 @@ master branch (aka work in progress branch)
 * `subst` and `subst_vars` now support heterogeneous equalities that are actually homogeneous
    (i.e., `@heq α a β b` where `α` and `β` are definitionally equal).
 
+* Add interactive `subst_vars` tactic.
+
 *Changes*
 
 * Replace `inout` modifier in type class declarations with `out_param` modifier.

library/init/meta/interactive.lean

@@ -1297,6 +1297,12 @@ Given hypothesis `h : x = t` or `h : t = x`, where `x` is a local constant, `sub
 meta def subst (q : parse texpr) : tactic unit :=
 i_to_expr q >>= tactic.subst >> try (tactic.reflexivity reducible)
 
+/--
+Apply `subst` to all hypotheses of the form `h : x = t` or `h : t = x`.
+-/
+meta def subst_vars : tactic unit :=
+tactic.subst_vars
+
 /--
 `clear h₁ ... hₙ` tries to clear each hypothesis `hᵢ` from the local context.
 -/

tests/lean/run/subst_heq.lean

@@ -2,3 +2,8 @@ example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
 begin
   subst h
 end
+
+example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
+begin
+  subst_vars
+end