diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index f4418f983..7936d3bf7 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -194,7 +194,6 @@ static void erase_local_binder_info(buffer<expr> & ps) {
 
 environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private, bool is_protected) {
     lean_assert(!(is_theorem && !is_opaque));
-    lean_assert(!(is_private && !is_opaque));
     lean_assert(!(is_private && is_protected));
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;