diff --git a/library/init/meta/smt_tactic.lean b/library/init/meta/smt_tactic.lean
index 3b87b963db..3722ed3d9e 100644
--- a/library/init/meta/smt_tactic.lean
+++ b/library/init/meta/smt_tactic.lean
@@ -83,8 +83,13 @@ meta instance : alternative smt_tactic :=
  map     := @fmap _ _}
 
 namespace smt_tactic
-meta constant intros    : smt_tactic unit
-meta constant close     : smt_tactic unit
+/-- (intros_core fresh_names), if fresh_names is tt, then create fresh names for new hypotheses.
+    Otherwise, it just uses the given names. -/
+meta constant intros_core : bool → smt_tactic unit
+meta constant close       : smt_tactic unit
+
+meta def intros : smt_tactic unit :=
+intros_core tt
 
 meta def try {α : Type} (t : smt_tactic α) : smt_tactic unit :=
 λ ss ts, tactic_result.cases_on (t ss ts)
@@ -146,6 +151,39 @@ do (s::ss, t::ts) ← get_goals | failed,
    (new_ss, new_ts) ← get_goals,
    set_goals (new_ss ++ ss) (new_ts ++ ts)
 
+meta def swap : smt_tactic unit :=
+do (ss, ts) ← get_goals,
+   match ss, ts with
+   | (s₁ :: s₂ :: ss), (t₁ :: t₂ :: ts) := set_goals (s₂ :: s₁ :: ss) (t₂ :: t₁ :: ts)
+   | _,                _                := failed
+   end
+
+/- (assert h t), adds a new goal for t, and the hypothesis (h : t) in the current goal. -/
+meta def assert (h : name) (t : expr) : smt_tactic unit :=
+tactic.assert_core h t >> swap >> intros_core ff >> swap >> try close
+
+/- (assertv h t v), adds the hypothesis (h : t) in the current goal if v has type t. -/
+meta def assertv (h : name) (t : expr) (v : expr) : smt_tactic unit :=
+tactic.assertv_core h t v >> intros_core ff >> return ()
+
+/- (define h t), adds a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
+meta def define  (h : name) (t : expr) : smt_tactic unit :=
+tactic.define_core h t >> swap >> intros_core ff >> swap >> try close
+
+/- (definev h t v), adds the hypothesis (h : t := v) in the current goal if v has type t. -/
+meta def definev (h : name) (t : expr) (v : expr) : smt_tactic unit :=
+tactic.definev_core h t v >> intros_core ff >> return ()
+
+/- Add (h : t := pr) to the current goal -/
+meta def pose (h : name) (pr : expr) : smt_tactic unit :=
+do t ← tactic.infer_type pr,
+   definev h t pr
+
+/- Add (h : t) to the current goal, given a proof (pr : t) -/
+meta def note (n : name) (pr : expr) : smt_tactic unit :=
+do t ← tactic.infer_type pr,
+   assertv n t pr
+
 meta def destruct (e : expr) : smt_tactic unit :=
 smt_tactic.seq (tactic.destruct e) smt_tactic.intros
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 26a5f536d0..e0b8d14d4b 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -305,14 +305,14 @@ meta constant mk_instance   : expr → tactic expr
 /- Change the target of the main goal.
    The input expression must be definitionally equal to the current target. -/
 meta constant change        : expr → tactic unit
-/- (assert H T), adds a new goal for T, and the hypothesis (H : T) in the current goal. -/
-meta constant assert        : name → expr → tactic unit
-/- (assertv H T P), adds the hypothesis (H : T) in the current goal if P has type T. -/
-meta constant assertv       : name → expr → expr → tactic unit
-/- (define H T), adds a new goal for T, and the hypothesis (H : T := ?M) in the current goal. -/
-meta constant define        : name → expr → tactic unit
-/- (definev H T P), adds the hypothesis (H : T := P) in the current goal if P has type T. -/
-meta constant definev       : name → expr → expr → tactic unit
+/- (assert_core H T), adds a new goal for T, and change target to (T -> target). -/
+meta constant assert_core   : name → expr → tactic unit
+/- (assertv_core H T P), change target to (T -> target) if P has type T. -/
+meta constant assertv_core  : name → expr → expr → tactic unit
+/- (define_core H T), adds a new goal for T, and change target to  (let H : T := ?M in target) in the current goal. -/
+meta constant define_core   : name → expr → tactic unit
+/- (definev_core H T P), change target to (Let H : T := P in target) if P has type T. -/
+meta constant definev_core  : name → expr → expr → tactic unit
 /- rotate goals to the left -/
 meta constant rotate_left   : nat → tactic unit
 meta constant get_goals     : tactic (list expr)
@@ -393,16 +393,6 @@ get_goals >>= set_goals
 meta def step {α : Type u} (t : tactic α) : tactic unit :=
 t >>[tactic] cleanup
 
-/- Add (H : T := pr) to the current goal -/
-meta def pose (n : name) (pr : expr) : tactic unit :=
-do t ← infer_type pr,
-   definev n t pr
-
-/- Add (H : T) to the current goal, given a proof (pr : T) -/
-meta def note (n : name) (pr : expr) : tactic unit :=
-do t ← infer_type pr,
-   assertv n t pr
-
 meta def is_prop (e : expr) : tactic bool :=
 do t ← infer_type e,
    return (to_bool (t = expr.prop))
@@ -537,6 +527,32 @@ do gs ← get_goals,
    | e                := skip
    end
 
+/- (assert h t), adds a new goal for t, and the hypothesis (h : t) in the current goal. -/
+meta def assert (h : name) (t : expr) : tactic unit :=
+assert_core h t >> swap >> intro h >> swap
+
+/- (assertv h t v), adds the hypothesis (h : t) in the current goal if v has type t. -/
+meta def assertv (h : name) (t : expr) (v : expr) : tactic unit :=
+assertv_core h t v >> intro h >> return ()
+
+/- (define h t), adds a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
+meta def define  (h : name) (t : expr) : tactic unit :=
+define_core h t >> swap >> intro h >> swap
+
+/- (definev h t v), adds the hypothesis (h : t := v) in the current goal if v has type t. -/
+meta def definev (h : name) (t : expr) (v : expr) : tactic unit :=
+definev_core h t v >> intro h >> return ()
+
+/- Add (h : t := pr) to the current goal -/
+meta def pose (h : name) (pr : expr) : tactic unit :=
+do t ← infer_type pr,
+   definev h t pr
+
+/- Add (h : t) to the current goal, given a proof (pr : t) -/
+meta def note (n : name) (pr : expr) : tactic unit :=
+do t ← infer_type pr,
+   assertv n t pr
+
 /- Return the number of goals that need to be solved -/
 meta def num_goals     : tactic nat :=
 do gs ← get_goals,
diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp
index d8a775b4b8..bdc7c212a9 100644
--- a/src/library/tactic/assert_tactic.cpp
+++ b/src/library/tactic/assert_tactic.cpp
@@ -8,9 +8,10 @@ Author: Leonardo de Moura
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
+#include "library/tactic/intro_tactic.h"
 
 namespace lean {
-vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_state const & s) {
+vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic_state const & s) {
     optional<metavar_decl> g = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception(s);
     type_context ctx     = mk_type_context_for(s);
@@ -24,31 +25,30 @@ vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_stat
     local_context lctx   = g->get_context();
     metavar_context mctx = ctx.mctx();
     expr new_M_1         = mctx.mk_metavar_decl(lctx, t);
-    expr l;
-    if (is_assert)
-        l = lctx.mk_local_decl(n, t);
-    else
-        l = lctx.mk_local_decl(n, t, new_M_1);
-    expr new_M_2         = mctx.mk_metavar_decl(lctx, g->get_type());
-    expr new_val;
-    if (is_assert)
-        new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M_2, mlocal_name(l))), new_M_1);
-    else
-        new_val = mk_let(n, t, new_M_1, mk_delayed_abstraction(new_M_2, mlocal_name(l)));
+    expr new_M_2, new_val;
+    if (is_assert) {
+        expr new_target  = mk_pi(n, t, g->get_type());
+        new_M_2          = mctx.mk_metavar_decl(lctx, new_target);
+        new_val          = mk_app(new_M_2, new_M_1);
+    } else {
+        expr new_target  = mk_let(n, t, new_M_1, g->get_type());
+        new_M_2          = mctx.mk_metavar_decl(lctx, new_target);
+        new_val          = new_M_2;
+    }
     mctx.assign(head(s.goals()), new_val);
     list<expr> new_gs    = cons(new_M_1, cons(new_M_2, tail(s.goals())));
     return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
 }
 
-vm_obj tactic_assert(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
-    return assert_define(true, to_name(n), to_expr(t), to_tactic_state(s));
+vm_obj tactic_assert_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
+    return assert_define_core(true, to_name(n), to_expr(t), to_tactic_state(s));
 }
 
-vm_obj tactic_define(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
-    return assert_define(false, to_name(n), to_expr(t), to_tactic_state(s));
+vm_obj tactic_define_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
+    return assert_define_core(false, to_name(n), to_expr(t), to_tactic_state(s));
 }
 
-vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
+vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
     optional<metavar_decl> g = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception(s);
     type_context ctx     = mk_type_context_for(s);
@@ -67,35 +67,43 @@ vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr cons
     }
     local_context lctx   = g->get_context();
     metavar_context mctx = ctx.mctx();
-    expr l;
-    if (is_assert)
-        l = lctx.mk_local_decl(n, t);
-    else
-        l = lctx.mk_local_decl(n, t, v);
-    expr new_M           = mctx.mk_metavar_decl(lctx, g->get_type());
-    expr new_val;
-    if (is_assert)
-        new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M, mlocal_name(l))), v);
-    else
-        new_val = mk_let(n, t, v, mk_delayed_abstraction(new_M, mlocal_name(l)));
+    expr new_M, new_val;
+    if (is_assert) {
+        expr new_target  = mk_pi(n, t, g->get_type());
+        new_M            = mctx.mk_metavar_decl(lctx, new_target);
+        new_val          = mk_app(new_M, v);
+    } else {
+        expr new_target  = mk_let(n, t, v, g->get_type());
+        new_M            = mctx.mk_metavar_decl(lctx, new_target);
+        new_val          = new_M;
+    }
     mctx.assign(head(s.goals()), new_val);
     list<expr> new_gs    = cons(new_M, tail(s.goals()));
     return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
 }
 
-vm_obj tactic_assertv(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
-    return assertv_definev(true, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
+vm_obj tactic_assertv_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
+    return assertv_definev_core(true, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
 }
 
-vm_obj tactic_definev(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
-    return assertv_definev(false, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
+vm_obj tactic_definev_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
+    return assertv_definev_core(false, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
+}
+
+vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
+    vm_obj r = assertv_definev_core(is_assert, n, t, v, s);
+    if (optional<tactic_state> const & s2 = is_tactic_success(r)) {
+        return intro(n, *s2);
+    } else {
+        return r;
+    }
 }
 
 void initialize_assert_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "assert"}),  tactic_assert);
-    DECLARE_VM_BUILTIN(name({"tactic", "assertv"}), tactic_assertv);
-    DECLARE_VM_BUILTIN(name({"tactic", "define"}),  tactic_define);
-    DECLARE_VM_BUILTIN(name({"tactic", "definev"}), tactic_definev);
+    DECLARE_VM_BUILTIN(name({"tactic", "assert_core"}),  tactic_assert_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "assertv_core"}), tactic_assertv_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "define_core"}),  tactic_define_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "definev_core"}), tactic_definev_core);
 }
 
 void finalize_assert_tactic() {
diff --git a/src/library/tactic/assert_tactic.h b/src/library/tactic/assert_tactic.h
index 8c60869ce4..2073ae1d41 100644
--- a/src/library/tactic/assert_tactic.h
+++ b/src/library/tactic/assert_tactic.h
@@ -7,7 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/tactic/tactic_state.h"
 namespace lean {
-vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_state const & s);
+vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic_state const & s);
+vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s);
 vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s);
 void initialize_assert_tactic();
 void finalize_assert_tactic();
diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h
index 68bb09db7e..d05d7667da 100644
--- a/src/library/tactic/intro_tactic.h
+++ b/src/library/tactic/intro_tactic.h
@@ -23,6 +23,8 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
 optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
                       expr const & mvar, unsigned n);
 
+vm_obj intro(name const & n, tactic_state const & s);
+
 void initialize_intro_tactic();
 void finalize_intro_tactic();
 }
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index 1cbf3aad07..30f65bfb0a 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -152,7 +152,7 @@ tactic_state revert_all(tactic_state const & s) {
     return revert(hs, s);
 }
 
-vm_obj preprocess(tactic_state const & s, smt_pre_config const & cfg) {
+vm_obj preprocess(tactic_state s, smt_pre_config const & cfg) {
     lean_assert(s.goals());
     optional<metavar_decl> g = s.get_main_goal_decl();
     type_context ctx         = mk_type_context_for(s, transparency_mode::Reducible);
@@ -163,28 +163,34 @@ vm_obj preprocess(tactic_state const & s, smt_pre_config const & cfg) {
     simp_lemmas_for eq_lemmas;
     if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
         eq_lemmas = *r;
-    expr new_target          = dsimplify_fn(ctx, max_steps, visit_instances, eq_lemmas)(target);
+    dsimplify_fn dsimp(ctx, max_steps, visit_instances, eq_lemmas);
+    expr new_target          = dsimp(target);
+    ctx.set_env(dsimp.update_defeq_canonizer_state(ctx.env()));
     bool contextual          = false;
     bool lift_eq             = true;
     bool canonize_instances  = true;
     bool canonize_proofs     = false;
     bool use_axioms          = true;
-    simp_result r            = simplify_fn(ctx, cfg.m_simp_lemmas, max_steps,
-                                           contextual, lift_eq, canonize_instances,
-                                           canonize_proofs, use_axioms)(get_eq_name(), new_target);
+    simplify_fn simp(ctx, cfg.m_simp_lemmas, max_steps,
+                     contextual, lift_eq, canonize_instances,
+                     canonize_proofs, use_axioms);
+    simp_result r            = simp(get_eq_name(), new_target);
+    ctx.set_env(simp.update_defeq_canonizer_state(ctx.env()));
     if (!r.has_proof()) {
+        s = set_env(s, ctx.env());
         return change(r.get_new(), s);
     } else {
         expr new_M           = ctx.mk_metavar_decl(ctx.lctx(), r.get_new());
         expr h               = mk_app(ctx, get_eq_mpr_name(), r.get_proof(), new_M);
         metavar_context mctx = ctx.mctx();
         mctx.assign(head(s.goals()), h);
-        tactic_state new_s   = set_mctx_goals(s, mctx, cons(new_M, tail(s.goals())));
+        tactic_state new_s   = set_env_mctx_goals(s, ctx.env(), mctx, cons(new_M, tail(s.goals())));
         return mk_tactic_success(new_s);
     }
 }
 
-expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, smt_goal & s_goal) {
+expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, smt_goal & s_goal,
+            bool use_unused_names) {
     optional<metavar_decl> decl = mctx.get_metavar_decl(mvar);
     lean_assert(decl);
     type_context ctx(env, opts, mctx, decl->get_context(), transparency_mode::Semireducible);
@@ -201,7 +207,8 @@ expr intros(environment const & env, options const & opts, metavar_context & mct
         }
         if (is_pi(target)) {
             expr type = instantiate_rev(binding_domain(target), to_inst.size(), to_inst.data());
-            name n    = ctx.get_unused_name(binding_name(target));
+            name n    = binding_name(target);
+            if (use_unused_names) n = ctx.get_unused_name(n);
             expr h    = locals.push_local(n, type);
             to_inst.push_back(h);
             new_Hs.push_back(h);
@@ -211,7 +218,8 @@ expr intros(environment const & env, options const & opts, metavar_context & mct
         } else if (is_let(target)) {
             expr type  = instantiate_rev(let_type(target), to_inst.size(), to_inst.data());
             expr value = instantiate_rev(let_value(target), to_inst.size(), to_inst.data());
-            name n     = ctx.get_unused_name(let_name(target));
+            name n     = let_name(target);
+            if (use_unused_names) n = ctx.get_unused_name(n);
             expr h     = locals.push_let(n, type, value);
             to_inst.push_back(h);
             new_Hs.push_back(h);
@@ -257,7 +265,8 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
     s = to_tactic_state(get_tactic_result_state(r));
 
     metavar_context mctx = s.mctx();
-    expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), new_goal);
+    bool use_unused_names = true;
+    expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), new_goal, use_unused_names);
     s = set_mctx_goals(s, mctx, cons(new_M, tail(s.goals())));
     return mk_tactic_success(mk_vm_cons(to_obj(new_goal), mk_vm_nil()), s);
 }
@@ -560,7 +569,7 @@ vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) {
     return mk_tactic_exception("smt_tactic.close failed", ts);
 }
 
-vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & _ts) {
+vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss, vm_obj const & _ts) {
     tactic_state ts = to_tactic_state(_ts);
     if (is_nil(ss))
         return mk_smt_state_empty_exception(ts);
@@ -573,7 +582,8 @@ vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & _ts) {
     ts = to_tactic_state(get_tactic_result_state(r));
 
     metavar_context mctx = ts.mctx();
-    expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), new_sgoal);
+    expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), new_sgoal,
+                           to_bool(use_unused_names));
 
     tactic_state new_ts = set_mctx_goals(ts, mctx, cons(new_mvar, tail(ts.goals())));
     vm_obj new_ss    = mk_vm_cons(to_obj(new_sgoal), tail(ss));
@@ -588,7 +598,7 @@ void initialize_smt_state() {
     DECLARE_VM_BUILTIN(name({"smt_state", "to_format"}),      smt_state_to_format);
     DECLARE_VM_BUILTIN("tactic_to_smt_tactic",                tactic_to_smt_tactic);
     DECLARE_VM_BUILTIN(name({"smt_tactic", "close"}),         smt_tactic_close);
-    DECLARE_VM_BUILTIN(name({"smt_tactic", "intros"}),        smt_tactic_intros);
+    DECLARE_VM_BUILTIN(name({"smt_tactic", "intros_core"}),   smt_tactic_intros_core);
 }
 
 void finalize_smt_state() {
diff --git a/tests/lean/run/smt_assert_define.lean b/tests/lean/run/smt_assert_define.lean
new file mode 100644
index 0000000000..09397e2cc6
--- /dev/null
+++ b/tests/lean/run/smt_assert_define.lean
@@ -0,0 +1,22 @@
+open smt_tactic
+
+example (a b c : nat) : a = b + 0 → a + c = b + c :=
+by using_smt $ do
+  pr ← tactic.to_expr `(add_zero b),
+  note `h pr,
+  trace_state, return ()
+
+constant p : nat → nat → Prop
+constant f : nat → nat
+axiom pf (a : nat) : p (f a) (f a) → p a a
+
+example (a b c : nat) : a = b → p (f a) (f b) → p a b :=
+by using_smt $ do
+  t ← tactic.to_expr `(p (f a) (f a)),
+  assert `h t,  -- assert automatically closed the new goal
+  trace_state,
+  tactic.trace "-----",
+  pr ← tactic.to_expr `(pf _ h),
+  note `h2 pr,
+  trace_state,
+  return ()