diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index e9a219f54..38a2ac26a 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -11,7 +11,6 @@ true_ne_false|¬true = false
 nat.lt_self_iff_false|∀ (n : nat), nat.lt n n ↔ false
 not_of_is_false|is_false ?c → ¬?c
 not_of_iff_false|(?a ↔ false) → ¬?a
-p_ne_false|?p → ?p ≠ false
 is_false|Π (c : Prop) [H : decidable c], Prop
 nat.lt_zero_iff_false|∀ (a : nat), nat.lt a nat.zero ↔ false
 not_of_eq_false|?p = false → ¬?p
@@ -21,6 +20,7 @@ not_false|¬false
 decidable_false|decidable false
 of_not_is_false|¬is_false ?c → ?c
 iff_false_intro|¬?a → (?a ↔ false)
+ne_false_of_self|?p → ?p ≠ false
 nat.succ_le_zero_iff_false|∀ (n : nat), nat.le (nat.succ n) nat.zero ↔ false
 tactic.exfalso|tactic
 -- ENDFINDP
diff --git a/tests/lean/run/new_obtain3.lean b/tests/lean/run/new_obtain3.lean
index 54466897f..0bcae0cd7 100644
--- a/tests/lean/run/new_obtain3.lean
+++ b/tests/lean/run/new_obtain3.lean
@@ -4,7 +4,7 @@ open set function eq.ops
 variables {X Y Z : Type}
 
 lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
-setext (take z,
+ext (take z,
   iff.intro
     (assume Hz : z ∈ (f ∘ g) '[a],
       obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean/run/new_obtain4.lean
index 034a09c47..f6a8c92a3 100644
--- a/tests/lean/run/new_obtain4.lean
+++ b/tests/lean/run/new_obtain4.lean
@@ -4,7 +4,7 @@ open set function eq.ops
 variables {X Y Z : Type}
 
 lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
-setext (take z,
+ext (take z,
   iff.intro
     (assume Hz,
       obtain x Hx₁ Hx₂, from Hz,