diff --git a/tests/lean/487.hlean.expected.out b/tests/lean/487.hlean.expected.out
index bc54dc13f..e084b8555 100644
--- a/tests/lean/487.hlean.expected.out
+++ b/tests/lean/487.hlean.expected.out
@@ -5,7 +5,7 @@ f : A → B,
 g : B → A,
 ε : Π (b : B), f (g b) = b,
 b b' : B
-⊢ (ε b)⁻¹ ⬝ refl (f (g b)) ⬝ ε b = refl b
+⊢ (ε b)⁻¹ ⬝ ε b = refl b
 487.hlean:19:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (B : Type) (f : …) (g : …) (ε : …) (b b' : B),
diff --git a/tests/lean/run/rewrite8.lean b/tests/lean/run/rewrite8.lean
index 3818cb050..c398f6d3c 100644
--- a/tests/lean/run/rewrite8.lean
+++ b/tests/lean/run/rewrite8.lean
@@ -3,4 +3,4 @@ open nat
 constant f : nat → nat
 
 theorem tst1 (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
-by rewrite [▸* at H1, ^add at H1, ^nat.rec_on at H1, ^of_num at H1, H1]
+by rewrite [▸* at H1, ^add at H1, H1]