diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean
index a340d18f2..87e1becb6 100644
--- a/hott/algebra/precategory/yoneda.hlean
+++ b/hott/algebra/precategory/yoneda.hlean
@@ -20,18 +20,18 @@ namespace yoneda
     (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
       : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
   calc
-        _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc
-      ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : assoc
-      ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : assoc
-      ... = _ : assoc
+        _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5     : by rewrite -assoc
+      ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5   : by rewrite -assoc
+      ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
+      ... = _                          : by rewrite (assoc f2 f3 f4)
 
   --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop
   definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
   functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2)
              (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
-             proof
-               (λ(x : Cᵒᵖ ×c C), eq_of_homotopy (λ(h : homset x.1 x.2), !id_left ⬝ !id_right))
-             qed
+             begin
+               intro x, apply eq_of_homotopy, intro h, exact (!id_left ⬝ !id_right)
+             end
              begin
                intros (x, y, z, g, f), apply eq_of_homotopy, intro h,
                exact (representable_functor_assoc g.2 f.2 h f.1 g.1),
@@ -48,22 +48,23 @@ namespace functor
   functor.mk (λd, F (c,d))
              (λd d' g, F (id, g))
              (λd, !respect_id)
-             (λd₁ d₂ d₃ g' g, proof calc
+             (λd₁ d₂ d₃ g' g, calc
                F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : {(id_comp c)⁻¹}
                  ... = F ((id,g') ∘ (id, g)) : idp
-                 ... = F (id,g') ∘ F (id, g) : respect_comp F qed)
+                 ... = F (id,g') ∘ F (id, g) : by rewrite (respect_comp F))
+
   local abbreviation Fob := @functor_curry_ob
 
   definition functor_curry_hom ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' :=
   nat_trans.mk (λd, F (f, id))
-               (λd d' g, proof calc
+               (λd d' g, calc
                  F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F
-                   ... = F (f, g ∘ id) : {id_left f}
-                   ... = F (f, g) : {id_right g}
-                   ... = F (f ∘ id, g) : {(id_right f)⁻¹}
-                   ... = F (f ∘ id, id ∘ g) : {(id_left g)⁻¹}
-                   ... = F (f, id) ∘ F (id, g) :  (respect_comp F (f, id) (id, g))⁻¹ᵖ
-            qed)
+                   ... = F (f, g ∘ id)      : by rewrite id_left
+                   ... = F (f, g)           : by rewrite id_right
+                   ... = F (f ∘ id, g)      : by rewrite id_right
+                   ... = F (f ∘ id, id ∘ g) : by rewrite id_left
+                   ... = F (f, id) ∘ F (id, g) :  (respect_comp F (f, id) (id, g))⁻¹ᵖ)
+
   local abbreviation Fhom := @functor_curry_hom
 
   definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) :
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index 776a8bf01..46026758a 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -97,9 +97,9 @@ theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
   λ A B f g,
     let eq_to_f := (λ g' x, f = g') in
     let sim2path := homotopy_ind f eq_to_f idp in
-    have t1 : sim2path f (homotopy.refl f) = idp,
+    assert t1 : sim2path f (homotopy.refl f) = idp,
       proof homotopy_ind_comp f eq_to_f idp qed,
-    have t2 : apD10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
+    assert t2 : apD10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
       proof ap apD10 t1 qed,
     have sect : apD10 ∘ (sim2path g) ∼ id,
       proof (homotopy_ind f (λ g' x, apD10 (sim2path g' x) = x) t2) g qed,
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 990c2b0b9..7f93527b3 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -5,7 +5,7 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
 begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
-coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp
+coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
 parse_tactic_location.cpp parse_rewrite_tactic.cpp
 type_util.cpp elaborator_exception.cpp)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index e726adda8..b76f8acaa 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -271,8 +271,9 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
 }
 
 static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
-    expr r = p.save_pos(mk_proof_qed_annotation(p.parse_expr()), pos);
+    expr r = p.parse_expr();
     p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
+    r      = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos);
     return r;
 }
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index a4adb7f96..9d4579998 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -46,7 +46,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/proof_qed_elaborator.h"
 #include "frontends/lean/calc_proof_elaborator.h"
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/begin_end_ext.h"
@@ -287,8 +286,6 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra
         return visit_by(e, some_expr(t), cs);
     } else if (is_calc_annotation(e)) {
         return visit_calc_proof(e, some_expr(t), cs);
-    } else if (is_proof_qed_annotation(e)) {
-        return visit_proof_qed(e, some_expr(t), cs);
     } else {
         return visit(e, cs);
     }
@@ -336,20 +333,6 @@ expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, cons
     return m;
 }
 
-expr elaborator::visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
-    lean_assert(is_proof_qed_annotation(e));
-    info_manager * im = nullptr;
-    if (infom())
-        im = &m_pre_info_data;
-    pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
-    expr m                         = m_full_context.mk_meta(m_ngen, t, e.get_tag());
-    register_meta(m);
-    constraint c                   = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config,
-                                                        im, m_relax_main_opaque);
-    cs += c;
-    return m;
-}
-
 static bool is_implicit_pi(expr const & e) {
     if (!is_pi(e))
         return false;
@@ -1329,8 +1312,6 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
         return visit_by(e, none_expr(), cs);
     } else if (is_calc_annotation(e)) {
         return visit_calc_proof(e, none_expr(), cs);
-    } else if (is_proof_qed_annotation(e)) {
-        return visit_proof_qed(e, none_expr(), cs);
     } else if (is_no_info(e)) {
         flet<bool> let(m_no_info, true);
         return visit(get_annotation_arg(e), cs);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index e30227ac0..4437f434d 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -111,7 +111,6 @@ class elaborator : public coercion_info_manager {
     expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
     expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
-    expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr add_implict_args(expr e, constraint_seq & cs, bool relax);
     pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp
deleted file mode 100644
index f405a1769..000000000
--- a/src/frontends/lean/proof_qed_elaborator.cpp
+++ /dev/null
@@ -1,57 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/unifier.h"
-#include "library/reducible.h"
-#include "library/metavar_closure.h"
-#include "frontends/lean/util.h"
-#include "frontends/lean/info_manager.h"
-namespace lean {
-/** \brief Create a "choice" constraint that postpone the
-    solving the constraints <tt>(cs union (m =?= e))</tt>.
-*/
-constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
-                              constraint_seq const & cs, unifier_config const & cfg,
-                              info_manager * im, bool relax) {
-    justification j         = mk_failed_to_synthesize_jst(env, m);
-    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
-                         name_generator const & _ngen) {
-        name_generator ngen(_ngen);
-        type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax));
-        pair<expr, constraint_seq> tcs = tc->infer(e);
-        expr e_type                    = tcs.first;
-        justification new_j            = mk_type_mismatch_jst(e, e_type, meta_type);
-        pair<bool, constraint_seq> dcs = tc->is_def_eq(e_type, meta_type, new_j);
-        if (!dcs.first)
-            throw unifier_exception(new_j, s);
-        constraint_seq new_cs          = cs + tcs.second + dcs.second;
-        buffer<constraint> cs_buffer;
-        new_cs.linearize(cs_buffer);
-        metavar_closure cls(meta);
-        cls.add(meta_type);
-        cls.mk_constraints(s, j, relax, cs_buffer);
-        cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
-
-        unifier_config new_cfg(cfg);
-        new_cfg.m_discard    = false;
-        unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg);
-        auto p = seq.pull();
-        lean_assert(p);
-        substitution new_s     = p->first.first;
-        constraints  postponed = map(p->first.second,
-                                     [&](constraint const & c) {
-                                         // we erase internal justifications
-                                         return update_justification(c, j);
-                                     });
-        if (im)
-            im->instantiate(new_s);
-        constraints r = cls.mk_constraints(new_s, j, relax);
-        return append(r, postponed);
-    };
-    bool owner = false;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
-}
-}
diff --git a/src/frontends/lean/proof_qed_elaborator.h b/src/frontends/lean/proof_qed_elaborator.h
deleted file mode 100644
index 6d1febf4d..000000000
--- a/src/frontends/lean/proof_qed_elaborator.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/unifier.h"
-#include "frontends/lean/info_manager.h"
-
-namespace lean {
-/** \brief Create a "choice" constraint that postpone the
-    solving the constraints <tt>(cs union (m =?= e))</tt>.
-
-    \remark A proof-qed block may instantiate meta-variables in the
-    info_manager. Thus, we provide the info_manager to make sure
-    this assignments are reflected on it.
-*/
-constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
-                              constraint_seq const & cs, unifier_config const & cfg,
-                              info_manager * im, bool relax);
-}
diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp
index c905254be..0973359f5 100644
--- a/src/library/annotation.cpp
+++ b/src/library/annotation.cpp
@@ -125,14 +125,11 @@ expr copy_annotations(expr const & from, expr const & to) {
 
 static name * g_have = nullptr;
 static name * g_show = nullptr;
-static name * g_proof_qed = nullptr;
 
 expr mk_have_annotation(expr const & e) { return mk_annotation(*g_have, e); }
 expr mk_show_annotation(expr const & e) { return mk_annotation(*g_show, e); }
-expr mk_proof_qed_annotation(expr const & e) { return mk_annotation(*g_proof_qed, e); }
 bool is_have_annotation(expr const & e) { return is_annotation(e, *g_have); }
 bool is_show_annotation(expr const & e) { return is_annotation(e, *g_show); }
-bool is_proof_qed_annotation(expr const & e) { return is_annotation(e, *g_proof_qed); }
 
 void initialize_annotation() {
     g_annotation = new name("annotation");
@@ -140,11 +137,9 @@ void initialize_annotation() {
     g_annotation_macros = new annotation_macros();
     g_have = new name("have");
     g_show = new name("show");
-    g_proof_qed = new name("proof-qed");
 
     register_annotation(*g_have);
     register_annotation(*g_show);
-    register_annotation(*g_proof_qed);
 
     register_macro_deserializer(get_annotation_opcode(),
                                 [](deserializer & d, unsigned num, expr const * args) {
@@ -157,7 +152,6 @@ void initialize_annotation() {
 }
 
 void finalize_annotation() {
-    delete g_proof_qed;
     delete g_show;
     delete g_have;
     delete g_annotation_macros;
diff --git a/src/library/annotation.h b/src/library/annotation.h
index d6c124e2c..2d874f275 100644
--- a/src/library/annotation.h
+++ b/src/library/annotation.h
@@ -57,14 +57,10 @@ expr copy_annotations(expr const & from, expr const & to);
 expr mk_have_annotation(expr const & e);
 /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */
 expr mk_show_annotation(expr const & e);
-/** \brief Tag \c e as a 'proof-qed'-expression. 'proof-qed' is a pre-registered annotation. */
-expr mk_proof_qed_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_have_annotation. */
 bool is_have_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_show_annotation. */
 bool is_show_annotation(expr const & e);
-/** \brief Return true iff \c e was created using #mk_proof_qed_annotation. */
-bool is_proof_qed_annotation(expr const & e);
 
 /** \brief Return the serialization 'opcode' for annotation macros. */
 std::string const & get_annotation_opcode();
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 6cc938d20..e03c137c6 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -74,7 +74,7 @@ nat.case_strong_induction_on m
     show f' (succ m) x = restrict default measure f (succ m) x, from
       by_cases -- (measure x < succ m)
         (assume H1 : measure x < succ m,
-          have H2a : ∀z, measure z < measure x → f' m z = f z,
+          assert H2a : ∀z, measure z < measure x → f' m z = f z,
           proof
             take z,
               assume Hzx : measure z < measure x,
@@ -90,7 +90,7 @@ nat.case_strong_induction_on m
                 ... = rec_val x f : rec_decreasing (f' m) f x H2a
           ∎,
           let m' := measure x in
-          have H3a : ∀z, measure z < m' → f' m' z = f z,
+          assert H3a : ∀z, measure z < m' → f' m' z = f z,
           proof
             take z,
               assume Hzx : measure z < measure x,
diff --git a/tests/lean/run/proof_qed_nested_tac.lean b/tests/lean/run/proof_qed_nested_tac.lean
new file mode 100644
index 000000000..c27e731cf
--- /dev/null
+++ b/tests/lean/run/proof_qed_nested_tac.lean
@@ -0,0 +1,6 @@
+example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) :=
+assert h : a = c, from eq.trans H₁ H₂,
+proof
+  calc f (f a a) (f b b) = f (f c c) (f b b) : by rewrite h
+                   ...   = f (f c c) (f c c) : by rewrite H₂
+qed