diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index db29c7e76..a5d2841be 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -644,8 +644,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
         apply rat.le.trans,
         apply rat.mul_le_mul_of_nonneg_right,
         apply pceil_helper Hn,
-        repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos),
-        --repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos),
+        repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos),
         apply rat.le_of_lt,
         apply rat.add_pos,
         apply rat.mul_pos,
@@ -654,7 +653,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
         repeat apply inv_pos,
         apply rat.mul_pos,
         apply rat.add_pos,
-        apply inv_pos,apply inv_pos, -- repeat apply inv_pos,
+        repeat apply inv_pos,
         apply rat_of_pnat_is_pos,
         have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin
           apply rat.ne_of_gt,
@@ -693,7 +692,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
     apply rat.le_of_lt,
     apply rat.mul_pos,
     apply rat.add_pos,
-    apply inv_pos,apply inv_pos, -- repeat apply inv_pos,
+    repeat apply inv_pos,
     apply rat_of_pnat_is_pos,
     apply rat.le_of_lt,
     apply inv_pos
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 8a4a1e7c9..1e4f041f1 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1498,7 +1498,13 @@ struct unifier_fn {
             set_conflict(j);
             return false;
         }
-        expr meta = *m_tc->is_stuck(pr_args[mkidx]);
+        auto stuck_it = m_tc->is_stuck(pr_args[mkidx]);
+        if (!stuck_it) {
+            // TODO(Lean): normalize, and try is_stuck again?
+            // We don't do it because it seems there is very little gain, and it may negatively affect performance.
+            return false;
+        }
+        expr meta = *stuck_it;
         lean_assert(is_meta(meta));
         buffer<expr> meta_args;
         expr const & mvar      = get_app_args(meta, meta_args);