diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 0c0c2d72cd..d751964aaa 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -644,6 +644,14 @@ match q₁, q₂ with
   tactic.define h e
 end >> skip
 
+/--
+This tactic applies to any goal. `suffices h : T` is the same as `have h : T, tactic.swap`.
+It mirrors the `suffices` term in term mode. This tactic can be followed by `from P` to
+prove the subgoal.
+-/
+meta def «suffices» (h : parse ident?) (t : parse (tk ":" *> texpr)?) : tactic unit :=
+«have» h t none >> tactic.swap
+
 
 /--
 This tactic displays the current state in the tracing buffer.
diff --git a/tests/lean/keyword_tactics.lean b/tests/lean/keyword_tactics.lean
index 0e3b549cfc..008d87b722 100644
--- a/tests/lean/keyword_tactics.lean
+++ b/tests/lean/keyword_tactics.lean
@@ -44,3 +44,8 @@ example (f : ℕ → ℕ) : bool :=
 begin
   have : ℕ, by apply f,
 end
+
+example (f : ℕ → ℕ) : bool :=
+begin
+  suffices: ℕ → bool, from this 0,
+end
diff --git a/tests/lean/keyword_tactics.lean.expected.out b/tests/lean/keyword_tactics.lean.expected.out
index b089175ea0..2aef63a644 100644
--- a/tests/lean/keyword_tactics.lean.expected.out
+++ b/tests/lean/keyword_tactics.lean.expected.out
@@ -8,3 +8,7 @@ keyword_tactics.lean:45:15: error: solve1 tactic failed, focused goal has not be
 state:
 f : ℕ → ℕ
 ⊢ ℕ
+keyword_tactics.lean:51:0: error: tactic failed, there are unsolved goals
+state:
+f : ℕ → ℕ
+⊢ ℕ → bool