diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index cf7b0ad70d..92f1fb77bf 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -46,6 +46,7 @@ Author: Leonardo de Moura
 #include "library/constructions/projection.h"
 #include "library/constructions/no_confusion.h"
 #include "library/constructions/injective.h"
+#include "library/equations_compiler/util.h"
 #include "library/inductive_compiler/add_decl.h"
 #include "library/tactic/elaborator_exception.h"
 #include "frontends/lean/parser.h"
@@ -952,6 +953,7 @@ struct structure_cmd_fn {
                 declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls,
                                                                        decl_type, decl_value, reducibility_hints::mk_abbreviation());
                 m_env = module::add(m_env, check(m_env, new_decl));
+                m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), m_modifiers.m_is_private, decl_name, args.size());
                 m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
             }
         }
diff --git a/tests/lean/run/unfold_default_values.lean b/tests/lean/run/unfold_default_values.lean
new file mode 100644
index 0000000000..a615009621
--- /dev/null
+++ b/tests/lean/run/unfold_default_values.lean
@@ -0,0 +1,10 @@
+structure S  :=
+(x : nat)
+(y : nat := 10)
+
+example (a : nat) (h : 10 = a) : {S . x := 10}^.y = a :=
+begin
+  simp [S.y._default],
+  guard_target 10 = a,
+  exact h
+end