diff --git a/stage0/src/library/compiler/csimp.cpp b/stage0/src/library/compiler/csimp.cpp
index d0c017b56e..14c91bc408 100644
--- a/stage0/src/library/compiler/csimp.cpp
+++ b/stage0/src/library/compiler/csimp.cpp
@@ -1149,7 +1149,8 @@ class csimp_fn {
         // Example: `fun {a} => ReaderT.pure`
         if (!is_join_point_def && !top) {
             expr new_e = eta_reduce(e);
-            if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
+           // Remark: we should not eta-reduce auxiliary match applications.
+            if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_matcher_app(env(), new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
                 return visit(new_e, true);
         }
         buffer<expr> binding_fvars;
diff --git a/stage0/src/library/compiler/util.h b/stage0/src/library/compiler/util.h
index f3fc259c6f..31672107bb 100644
--- a/stage0/src/library/compiler/util.h
+++ b/stage0/src/library/compiler/util.h
@@ -204,6 +204,11 @@ inline bool is_matcher(environment const & env, name const & n) {
     return lean_is_matcher(env.to_obj_arg(), n.to_obj_arg());
 }
 
+inline bool is_matcher_app(environment const & env, expr const & e) {
+  expr const & f = get_app_fn(e);
+  return is_constant(f) && is_matcher(env, const_name(f));
+}
+
 void initialize_compiler_util();
 void finalize_compiler_util();
 }