diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index 0521154c43..4021bc08e5 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -59,11 +59,11 @@ end
 
 private lemma sub_nat_nat_of_sub_eq_zero {m n : ℕ} (h : n - m = 0) :
   sub_nat_nat m n = of_nat (m - n) :=
-begin unfold sub_nat_nat, rw [h, sub_nat_nat._match_1.equations.eqn_1] end
+begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1, reflexivity end
 
 private lemma sub_nat_nat_of_sub_eq_succ {m n k : ℕ} (h : n - m = succ k) :
   sub_nat_nat m n = -[1+ k] :=
-begin unfold sub_nat_nat, rw [h, sub_nat_nat._match_1.equations.eqn_2] end
+begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1, reflexivity end
 
 protected def neg : ℤ → ℤ
 | (of_nat n) := neg_of_nat n
@@ -276,7 +276,7 @@ protected lemma mul_comm : ∀ a b : ℤ, a * b = b * a
 private lemma of_nat_mul_neg_of_nat (m : ℕ) :
    ∀ n, of_nat m * neg_of_nat n = neg_of_nat (m * n)
 | 0        := rfl
-| (succ n) := by simp [neg_of_nat.equations.eqn_2]
+| (succ n) := begin unfold neg_of_nat, simp end
 
 private lemma neg_of_nat_mul_of_nat (m n : ℕ) :
     neg_of_nat m * of_nat n = neg_of_nat (m * n) :=
@@ -285,7 +285,7 @@ begin rw int.mul_comm, simp [of_nat_mul_neg_of_nat] end
 private lemma neg_succ_of_nat_mul_neg_of_nat (m : ℕ) :
   ∀ n, -[1+ m] * neg_of_nat n = of_nat (succ m * n)
 | 0        := rfl
-| (succ n) := by simp [neg_of_nat.equations.eqn_2]
+| (succ n) := begin unfold neg_of_nat, simp end
 
 private lemma neg_of_nat_mul_neg_succ_of_nat (m n : ℕ) :
   neg_of_nat n * -[1+ m] = of_nat (n * succ m) :=
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index b9fe9d91f8..960e8a9717 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -514,8 +514,7 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
     environment new_env = env;
     unsigned i = 1;
     while (true) {
-        name eqn_suffix = name({"equations", "eqn"}).append_after(i);
-        name eqn_name = const_name(fn) + eqn_suffix;
+        name eqn_name = mk_equation_name(const_name(fn), i);
         optional<declaration> eqn_decl = env.find(eqn_name);
         if (!eqn_decl) break;
         unsigned num_eqn_levels = eqn_decl->get_num_univ_params();
@@ -548,7 +547,7 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
                     return none_expr();
             });
         new_eqn_type = locals.mk_pi(new_eqn_type);
-        name new_eqn_name    = d_name + eqn_suffix;
+        name new_eqn_name    = mk_equation_name(d_name, i);
         expr new_eqn_value;
         new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args);
         new_eqn_value = locals.mk_lambda(new_eqn_value);
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 0916e62e45..d1e7c17b91 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -532,8 +532,8 @@ static expr prove_eqn_lemma(type_context & ctx, buffer<expr> const & Hs, expr co
     return ctx.mk_lambda(Hs, body);
 }
 
-static name mk_equation_name(name const & f_name, unsigned eqn_idx) {
-    return name(name(f_name, "equations"), "eqn").append_after(eqn_idx);
+name mk_equation_name(name const & f_name, unsigned eqn_idx) {
+    return name(name(f_name, "equations"), "_eqn").append_after(eqn_idx);
 }
 
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h
index d43bbfa230..c594b58fa8 100644
--- a/src/library/equations_compiler/util.h
+++ b/src/library/equations_compiler/util.h
@@ -97,6 +97,8 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
    This function is used to make sure we have equations for all definitions. */
 environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity);
 
+name mk_equation_name(name const & f_name, unsigned eqn_idx);
+
 void initialize_eqn_compiler_util();
 void finalize_eqn_compiler_util();
 }
diff --git a/src/library/tactic/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp
index 904437bed2..65797ee9d5 100644
--- a/src/library/tactic/eqn_lemmas.cpp
+++ b/src/library/tactic/eqn_lemmas.cpp
@@ -12,7 +12,11 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/constants.h"
 #include "library/module.h"
+#include "library/vm/vm_name.h"
+#include "library/vm/vm_list.h"
+#include "library/equations_compiler/util.h"
 #include "library/tactic/eqn_lemmas.h"
+#include "library/tactic/tactic_state.h"
 
 namespace lean {
 struct eqn_lemmas_ext : public environment_extension {
@@ -96,10 +100,9 @@ void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_o
 }
 
 void get_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result) {
-    name base(name(cname, "equations"), "eqn");
     unsigned idx = 1;
     while (true) {
-        name eqn = base.append_after(idx);
+        name eqn = mk_equation_name(cname, idx);
         if (env.find(eqn)) {
             result.push_back(eqn);
             idx++;
@@ -128,6 +131,16 @@ void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer<
     }
 }
 
+vm_obj tactic_get_eqn_lemmas_for(vm_obj const & all, vm_obj const & n, vm_obj const & s) {
+    buffer<name> result;
+    if (to_bool(all)) {
+        get_ext_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result);
+    } else {
+        get_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result);
+    }
+    return mk_tactic_success(to_obj(result), to_tactic_state(s));
+}
+
 bool has_eqn_lemmas(environment const & env, name const & cname) {
     eqn_lemmas_ext const & ext = get_extension(env);
     return ext.m_lemmas.contains(cname);
@@ -136,6 +149,7 @@ bool has_eqn_lemmas(environment const & env, name const & cname) {
 void initialize_eqn_lemmas() {
     g_ext            = new eqn_lemmas_ext_reg();
     eqn_lemmas_modification::init();
+    DECLARE_VM_BUILTIN(name({"tactic", "get_eqn_lemmas_for"}), tactic_get_eqn_lemmas_for);
 }
 
 void finalize_eqn_lemmas() {
diff --git a/tests/lean/def_inaccessible_issue.lean b/tests/lean/def_inaccessible_issue.lean
index 8d01315540..b29bccf0a5 100644
--- a/tests/lean/def_inaccessible_issue.lean
+++ b/tests/lean/def_inaccessible_issue.lean
@@ -14,4 +14,4 @@ definition map2 : ∀ {n}, bv n → bv n → bv n
 | 0     nil            nil             := nil
 | (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
 
-check map2.equations.eqn_2
+check map2.equations._eqn_2
diff --git a/tests/lean/def_inaccessible_issue.lean.expected.out b/tests/lean/def_inaccessible_issue.lean.expected.out
index e08ab8c4b6..5599ccc6b4 100644
--- a/tests/lean/def_inaccessible_issue.lean.expected.out
+++ b/tests/lean/def_inaccessible_issue.lean.expected.out
@@ -1,3 +1,3 @@
-map2.equations.eqn_2 :
+map2.equations._eqn_2 :
   ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
     map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)
diff --git a/tests/lean/run/def_complete_bug.lean b/tests/lean/run/def_complete_bug.lean
index 7fe14e656a..2fe87a919c 100644
--- a/tests/lean/run/def_complete_bug.lean
+++ b/tests/lean/run/def_complete_bug.lean
@@ -1,4 +1,3 @@
-
 definition g : list nat → list nat → nat
 | []          (y::ys)  := y
 | []           ys      := 0
@@ -6,9 +5,9 @@ definition g : list nat → list nat → nat
 | (x::xs)      (y::ys) := g xs ys + y
 | (x::xs)      []      := g xs []
 
-print g._main.equations.eqn_1
-print g._main.equations.eqn_2
-print g._main.equations.eqn_3
-print g._main.equations.eqn_4
-print g._main.equations.eqn_5
-print g._main.equations.eqn_6
+print g._main.equations._eqn_1
+print g._main.equations._eqn_2
+print g._main.equations._eqn_3
+print g._main.equations._eqn_4
+print g._main.equations._eqn_5
+print g._main.equations._eqn_6
diff --git a/tests/lean/run/def_ite_value.lean b/tests/lean/run/def_ite_value.lean
index 6f12d2ef97..f551f1fcc0 100644
--- a/tests/lean/run/def_ite_value.lean
+++ b/tests/lean/run/def_ite_value.lean
@@ -1,4 +1,3 @@
-
 inductive bv : nat → Type
 | nil  : bv 0
 | cons : Π n, bool → bv n → bv (n+1)
@@ -12,9 +11,9 @@ definition f : ∀ n : nat, bv n → nat → nat
 
 set_option pp.binder_types true
 
-check @f._main.equations.eqn_1
-check @f._main.equations.eqn_2
-check @f._main.equations.eqn_3
+check @f._main.equations._eqn_1
+check @f._main.equations._eqn_2
+check @f._main.equations._eqn_3
 
 example (n : nat) (b : bool) (v : bv n) (x : nat) : x ≠ 1000000 → f (n+1) (cons n b v) x = f n v (x + 1) :=
-assume H, f._main.equations.eqn_3 n b v x H
+assume H, f._main.equations._eqn_3 n b v x H
diff --git a/tests/lean/run/equation_with_values.lean b/tests/lean/run/equation_with_values.lean
index 8cd7fe3406..99cd5d4f94 100644
--- a/tests/lean/run/equation_with_values.lean
+++ b/tests/lean/run/equation_with_values.lean
@@ -6,12 +6,12 @@ def f : char → nat
 | #"e" := 4
 | _    := 5
 
-check f.equations.eqn_1
-check f.equations.eqn_2
-check f.equations.eqn_3
-check f.equations.eqn_4
-check f.equations.eqn_5
-check f.equations.eqn_6
+check f.equations._eqn_1
+check f.equations._eqn_2
+check f.equations._eqn_3
+check f.equations._eqn_4
+check f.equations._eqn_5
+check f.equations._eqn_6
 
 def g : nat → nat
 | 100000 := 0
@@ -20,11 +20,11 @@ def g : nat → nat
 | 400000 := 3
 | _      := 5
 
-check g.equations.eqn_1
-check g.equations.eqn_2
-check g.equations.eqn_3
-check g.equations.eqn_4
-check g.equations.eqn_5
+check g.equations._eqn_1
+check g.equations._eqn_2
+check g.equations._eqn_3
+check g.equations._eqn_4
+check g.equations._eqn_5
 
 def h : string → nat
 | "hello" := 0
@@ -33,19 +33,19 @@ def h : string → nat
 | "boo"   := 3
 | _       := 5
 
-check h.equations.eqn_1
-check h.equations.eqn_2
-check h.equations.eqn_3
-check h.equations.eqn_4
-check h.equations.eqn_5
+check h.equations._eqn_1
+check h.equations._eqn_2
+check h.equations._eqn_3
+check h.equations._eqn_4
+check h.equations._eqn_5
 
 def r : string × string → nat
 | ("hello", "world") := 0
 | ("world", "hello") := 1
 | _                  := 2
 
-check r.equations.eqn_1
-check r.equations.eqn_2
-check r.equations.eqn_3
-check r.equations.eqn_4
-check r.equations.eqn_5
+check r.equations._eqn_1
+check r.equations._eqn_2
+check r.equations._eqn_3
+check r.equations._eqn_4
+check r.equations._eqn_5
diff --git a/tests/lean/run/lift_nested_rec.lean b/tests/lean/run/lift_nested_rec.lean
index 7bdce4497d..3a59050642 100644
--- a/tests/lean/run/lift_nested_rec.lean
+++ b/tests/lean/run/lift_nested_rec.lean
@@ -1,4 +1,3 @@
-
 definition f : nat → (nat × nat) → nat
 | 0      m := m.1
 | (n+1)  m :=
@@ -6,6 +5,6 @@ definition f : nat → (nat × nat) → nat
   | (a, b) := (f n (b, a + 1)) + (f n (a, b))
   end
 
-check @f._main.equations.eqn_1
-check @f._main.equations.eqn_2
-check @f._match_1.equations.eqn_1
+check @f._main.equations._eqn_1
+check @f._main.equations._eqn_2
+check @f._match_1.equations._eqn_1
diff --git a/tests/lean/run/pack_unpack1.lean b/tests/lean/run/pack_unpack1.lean
index 01ab870370..b552e302b5 100644
--- a/tests/lean/run/pack_unpack1.lean
+++ b/tests/lean/run/pack_unpack1.lean
@@ -1,4 +1,3 @@
-
 inductive tree_core (A : Type*) : bool → Type*
 | leaf'    : A → tree_core ff
 | node'    : tree_core tt → tree_core ff
@@ -66,8 +65,8 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
 | (tree.leaf a) := mk1 a
 | (tree.node l) := mk2 l
 
-check bla._main.equations.eqn_1
-check bla._main.equations.eqn_2
+check bla._main.equations._eqn_1
+check bla._main.equations._eqn_2
 
 definition foo {A : Type*} : nat → tree A → nat
 | 0     _                   := 0
@@ -75,7 +74,7 @@ definition foo {A : Type*} : nat → tree A → nat
 | (n+1) (tree.node [])      := foo n (tree.node [])
 | (n+1) (tree.node (x::xs)) := foo n x
 
-check @foo._main.equations.eqn_1
-check @foo._main.equations.eqn_2
-check @foo._main.equations.eqn_3
-check @foo._main.equations.eqn_4
+check @foo._main.equations._eqn_1
+check @foo._main.equations._eqn_2
+check @foo._main.equations._eqn_3
+check @foo._main.equations._eqn_4
diff --git a/tests/lean/run/pack_unpack2.lean b/tests/lean/run/pack_unpack2.lean
index 8c34e49fb1..eef0c57bb1 100644
--- a/tests/lean/run/pack_unpack2.lean
+++ b/tests/lean/run/pack_unpack2.lean
@@ -16,8 +16,8 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
 | (tree.leaf a) := mk1 a
 | (tree.node l) := mk2 l
 
-check bla._main.equations.eqn_1
-check bla._main.equations.eqn_2
+check bla._main.equations._eqn_1
+check bla._main.equations._eqn_2
 
 noncomputable definition foo {A : Type*} : nat → tree A → nat
 | 0     _                   := sorry
@@ -25,7 +25,7 @@ noncomputable definition foo {A : Type*} : nat → tree A → nat
 | (n+1) (tree.node [])      := foo n (tree.node [])
 | (n+1) (tree.node (x::xs)) := foo n x
 
-check @foo._main.equations.eqn_1
-check @foo._main.equations.eqn_2
-check @foo._main.equations.eqn_3
-check @foo._main.equations.eqn_4
+check @foo._main.equations._eqn_1
+check @foo._main.equations._eqn_2
+check @foo._main.equations._eqn_3
+check @foo._main.equations._eqn_4
diff --git a/tests/lean/run/pack_unpack3.lean b/tests/lean/run/pack_unpack3.lean
index 4beaced584..8fa55f6188 100644
--- a/tests/lean/run/pack_unpack3.lean
+++ b/tests/lean/run/pack_unpack3.lean
@@ -16,14 +16,14 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
 | (tree.leaf a) := mk1 a
 | (tree.node n xs) := mk2 n xs
 
-check bla._main.equations.eqn_1
-check bla._main.equations.eqn_2
+check bla._main.equations._eqn_1
+check bla._main.equations._eqn_2
 
 noncomputable definition foo {A : Type*} : nat → tree A → nat
 | 0     _                                     := sorry
 | (n+1) (tree.leaf a)                         := 0
 | (n+1) (tree.node m xs)                      := foo n (tree.node m xs)
 
-check @foo._main.equations.eqn_1
-check @foo._main.equations.eqn_2
-check @foo._main.equations.eqn_3
+check @foo._main.equations._eqn_1
+check @foo._main.equations._eqn_2
+check @foo._main.equations._eqn_3