diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 1ce6b0475..2ee998487 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -164,6 +164,12 @@ void decl_attributes::parse(parser & p) {
 }
 
 environment decl_attributes::apply(environment env, io_state const & ios, name const & d) const {
+    bool forward = m_forward;
+    if (has_pattern_hints(env.get(d).get_type())) {
+        // turn on [forward] if patterns hints have been used in the type.
+        forward = true;
+    }
+
     if (m_is_instance) {
         if (m_priority) {
             #if defined(__GNUC__) && !defined(__CLANG__)
@@ -233,7 +239,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
         else
             env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent);
     }
-    if (m_forward) {
+    if (forward) {
         if (m_priority)
             env = add_hi_lemma(env, ios.get_options(), d, *m_priority, m_persistent);
         else
diff --git a/tests/lean/run/pattern1.lean b/tests/lean/run/pattern1.lean
index 582bee9c8..581b444c7 100644
--- a/tests/lean/run/pattern1.lean
+++ b/tests/lean/run/pattern1.lean
@@ -5,11 +5,10 @@ sorry
 
 print lemma1
 
--- TODO(Leo): remove patterns that are permutations of of other patterns
 definition lemma2 [forward] {a b : nat} : f a b = f b a :=
 sorry
 
-definition lemma3 [forward] {a b : nat} : (:f a b:) = f b a :=
+definition lemma3 {a b : nat} : (:f a b:) = f b a :=
 sorry
 
 print lemma2