diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index d61953466..0da0a0342 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/expr_pair.h"
 #include "library/hop_match.h"
+#include "library/expr_lt.h"
 #include "library/simplifier/rewrite_rule_set.h"
 
 #ifndef LEAN_SIMPLIFIER_PROOFS
@@ -477,6 +478,14 @@ class simplifier_fn {
         return true;
     }
 
+    bool sorted_args(unsigned num, expr const * args) {
+        for (unsigned i = 1; i < num; i++) {
+            if (!is_lt(args[i-1], args[i], false))
+                return false;
+        }
+        return true;
+    }
+
     /**
        \brief Auxiliary function used by m_match_fn, it tries to match the given rule and
        the expression in the temporary field \c m_target.
@@ -491,6 +500,8 @@ class simplifier_fn {
             m_new_args.clear();
             m_new_args.resize(num+1);
             if (found_all_args(num)) {
+                if (rule.is_permutation() && sorted_args(num, m_new_args.begin()+1))
+                    return false;
                 // easy case: all arguments found
                 m_new_rhs   = instantiate(rule.get_rhs(), num, m_new_args.data() + 1);
                 if (m_proofs_enabled) {
diff --git a/tests/lean/simp6.lean b/tests/lean/simp6.lean
new file mode 100644
index 000000000..313cf358e
--- /dev/null
+++ b/tests/lean/simp6.lean
@@ -0,0 +1,8 @@
+variables a b : Nat
+rewrite_set simple
+add_rewrite Nat::add_comm eq_id : simple
+
+(*
+local t = parse_lean("a + b = b + a")
+print(simplify(t, 'simple'))
+*)
\ No newline at end of file
diff --git a/tests/lean/simp6.lean.expected.out b/tests/lean/simp6.lean.expected.out
new file mode 100644
index 000000000..aa1e36a65
--- /dev/null
+++ b/tests/lean/simp6.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+⊤	trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b))