diff --git a/tests/lean/630.lean.expected.out b/tests/lean/630.lean.expected.out
index 83f80820b..f428f44e7 100644
--- a/tests/lean/630.lean.expected.out
+++ b/tests/lean/630.lean.expected.out
@@ -1,6 +1,5 @@
-inductive pnat.pnat : Type₁
-constructors:
-pnat.pnat.pos : Π (n : ℕ), nat.gt n (nat.of_num 0) → ℕ+
+definition pnat.pnat : Type₁ :=
+{ (n : ℕ)| nat.gt n (nat.of_num 0)}
 inductive prod : Type → Type → Type
 constructors:
 prod.mk : Π {A : Type} {B : Type}, A → B → A × B
diff --git a/tests/lean/rw_set3.lean b/tests/lean/rw_set3.lean
deleted file mode 100644
index f17e7acb8..000000000
--- a/tests/lean/rw_set3.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import data.nat
-
-attribute nat.add.comm [simp]
-
-print [simp]
diff --git a/tests/lean/rw_set3.lean.expected.out b/tests/lean/rw_set3.lean.expected.out
deleted file mode 100644
index f9e6ae968..000000000
--- a/tests/lean/rw_set3.lean.expected.out
+++ /dev/null
@@ -1,33 +0,0 @@
-simplification rules for iff
-#1, ?M_1 ↔ false ↦ ¬?M_1
-#1, ?M_1 ↔ true ↦ ?M_1
-#0, false ↔ true ↦ false
-#0, true ↔ false ↦ false
-#1, ?M_1 ↔ ¬?M_1 ↦ false
-#1, ?M_1 ↔ ?M_1 ↦ true
-#1, false ↔ ?M_1 ↦ ¬?M_1
-#1, true ↔ ?M_1 ↦ ?M_1
-#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3
-#1, ?M_1 ∧ ?M_1 ↦ ?M_1
-#1, false ∧ ?M_1 ↦ false
-#1, ?M_1 ∧ false ↦ false
-#1, true ∧ ?M_1 ↦ ?M_1
-#1, ?M_1 ∧ true ↦ ?M_1
-#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3
-#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1
-#2, ?M_2 == ?M_2 ↦ true
-#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3
-#1, false ∨ ?M_1 ↦ ?M_1
-#1, ?M_1 ∨ false ↦ ?M_1
-#1, true ∨ ?M_1 ↦ true
-#1, ?M_1 ∨ true ↦ true
-#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
-#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
-#2, ?M_2 = ?M_2 ↦ true
-#0, ¬false ↦ true
-#0, ¬true ↦ false
-simplification rules for eq
-#2 perm, nat.add ?M_1 ?M_2 ↦ nat.add ?M_2 ?M_1
-#3, ite false ?M_2 ?M_3 ↦ ?M_3
-#3, ite true ?M_2 ?M_3 ↦ ?M_2
-#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4