diff --git a/tests/lean/rateval.lean.expected.out b/tests/lean/rateval.lean.expected.out
index 5527fa0894..5406259023 100644
--- a/tests/lean/rateval.lean.expected.out
+++ b/tests/lean/rateval.lean.expected.out
@@ -1 +1 @@
-quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) prerat.one))
+quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) (prerat.of_int 1)))
diff --git a/tests/lean/run/new_obtain3.lean b/tests/lean/run/new_obtain3.lean
index a75dfda508..54466897fe 100644
--- a/tests/lean/run/new_obtain3.lean
+++ b/tests/lean/run/new_obtain3.lean
@@ -8,8 +8,8 @@ setext (take z,
   iff.intro
     (assume Hz : z ∈ (f ∘ g) '[a],
       obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
-      have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl,
-      show z ∈ f '[g '[a]], from in_image Hgx Hx₂)
+      have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
+      show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
     (assume Hz : z ∈ f '[g '[a]],
       obtain y [x (Hz₁ : x ∈ a) (Hz₂ : g x = y)] (Hy₂ : f y = z), from Hz,
-      show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
+      show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean/run/new_obtain4.lean
index 326c2e3039..034a09c47d 100644
--- a/tests/lean/run/new_obtain4.lean
+++ b/tests/lean/run/new_obtain4.lean
@@ -8,7 +8,7 @@ setext (take z,
   iff.intro
     (assume Hz,
       obtain x Hx₁ Hx₂, from Hz,
-      by repeat (apply in_image | assumption | reflexivity))
+      by repeat (apply mem_image | assumption | reflexivity))
     (assume Hz,
       obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
-      by repeat (apply in_image | assumption | esimp [compose] | rewrite Hz₂)))
+      by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))