diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 69669470e2..5c244d087d 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -10,3 +10,4 @@ import Lean.Elab.Tactic.Induction
 import Lean.Elab.Tactic.Generalize
 import Lean.Elab.Tactic.Injection
 import Lean.Elab.Tactic.Match
+import Lean.Elab.Tactic.Binders
diff --git a/src/Lean/Elab/Tactic/Binders.lean b/src/Lean/Elab/Tactic/Binders.lean
new file mode 100644
index 0000000000..295156ff12
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Binders.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Tactic.Basic
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+private def liftTermBinderSyntax : Macro :=
+fun stx => do
+  hole ← `(?_);
+  match stx.getKind with
+  | Name.str (Name.str p "Tactic" _) s _ =>
+    let kind := mkNameStr (mkNameStr p "Term") s;
+    let termStx := Syntax.node kind (stx.getArgs ++ #[mkAtomFrom stx "; ", hole]);
+    `(tactic| refine $termStx)
+  | _ => Macro.throwError stx "unexpected binder syntax"
+
+@[builtinMacro Lean.Parser.Tactic.have] def expandHaveTactic : Macro := liftTermBinderSyntax
+@[builtinMacro Lean.Parser.Tactic.let] def expandLetTactic : Macro := liftTermBinderSyntax
+@[builtinMacro Lean.Parser.Tactic.«let!»] def expandLetBangTactic : Macro := liftTermBinderSyntax
+@[builtinMacro Lean.Parser.Tactic.suffices] def expandSufficesTactic : Macro := liftTermBinderSyntax
+
+@[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro :=
+fun stx =>
+  let type := stx.getArg 1;
+  `(tactic| refine (show $type from ?_))
+
+end Tactic
+end Elab
+end Lean
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 5088f93f5d..dc9c0094ad 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -11,3 +11,36 @@ begin
   clear x y;
   exact z
 end
+
+theorem ex3 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
+begin
+  have y = z from h₂.symm;
+  apply Eq.trans;
+  exact h₁;
+  assumption
+end
+
+theorem ex4 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
+begin
+  let h₃ : y = z := h₂.symm;
+  apply Eq.trans;
+  exact h₁;
+  exact h₃
+end
+
+theorem ex5 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
+begin
+  let! h₃ : y = z := h₂.symm;
+  apply Eq.trans;
+  exact h₁;
+  exact h₃
+end
+
+theorem ex6 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : id (x + 0 = z) :=
+begin
+  show x = z;
+  let! h₃ : y = z := h₂.symm;
+  apply Eq.trans;
+  exact h₁;
+  exact h₃
+end