diff --git a/tests/lean/run/blast_simp1.lean b/tests/lean/run/blast_simp1.lean
index cb290d523..39fcb27eb 100644
--- a/tests/lean/run/blast_simp1.lean
+++ b/tests/lean/run/blast_simp1.lean
@@ -1,17 +1,17 @@
 example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a :=
-by blast
+by simp
 
 example (a b c : Prop) : a ∧ false ∧ c ↔ false :=
-by blast
+by simp
 
 example (a b c : Prop) : a ∨ false ∨ b ↔ b ∨ a :=
-by blast
+by simp
 
 example (a b c : Prop) : ¬ true ∨ false ∨ b ↔ b :=
-by blast
+by simp
 
 example (a b c : Prop) : if true then a else b ↔ if false then b else a :=
-by blast
+by simp
 
 example (a b : Prop) : a ∧ not a ↔ false :=
-by blast
+by simp
diff --git a/tests/lean/run/blast_simp2.lean b/tests/lean/run/blast_simp2.lean
index 1839a8b73..adbd26971 100644
--- a/tests/lean/run/blast_simp2.lean
+++ b/tests/lean/run/blast_simp2.lean
@@ -1,6 +1,4 @@
-set_option blast.recursor false
-
 definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a :=
-by blast
+by simp
 
 print tst1
diff --git a/tests/lean/run/blast_simp3.lean b/tests/lean/run/blast_simp3.lean
index c83b1dbb2..cbbb6b549 100644
--- a/tests/lean/run/blast_simp3.lean
+++ b/tests/lean/run/blast_simp3.lean
@@ -1,11 +1,3 @@
-set_option blast.simp false
-
 example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ →
  (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) :=
-by blast
-
-set_option blast.simp true
-
-example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ →
- (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) :=
-by blast
+by simp