diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d2089c5cd9..d4dc428793 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2349,14 +2349,14 @@ void initialize_elaborator() {
 
     register_system_attribute(
         elaborator_strategy_proxy_attribute(
-            "elab_default",
+            "elab_simple",
             "instructs elaborator that the arguments of the function application (f ...) "
             "should be elaborated from left to right, and without propagating information from the expected type "
             "to its arguments",
             elaborator_strategy::Default));
 
-    register_incompatible("elab_default", "elab_with_expected_type");
-    register_incompatible("elab_default", "elab_as_eliminator");
+    register_incompatible("elab_simple", "elab_with_expected_type");
+    register_incompatible("elab_simple", "elab_as_eliminator");
     register_incompatible("elab_with_expected_type", "elab_as_eliminator");
 }