diff --git a/tests/lean/apply_tac_bug.lean b/tests/lean/apply_tac_bug.lean
index 32787ea262..fe5bb8224e 100644
--- a/tests/lean/apply_tac_bug.lean
+++ b/tests/lean/apply_tac_bug.lean
@@ -1,4 +1,3 @@
-import heq
 import macros
 import tactic
 
@@ -7,4 +6,3 @@ theorem my_proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
        H1_eq_H1b : H1 == H1b             := hsymm (cast_heq (by simp) H1),
        H1b_eq_H2 : H1b == H2             := to_heq (proof_irrel H1b H2)
    in  htrans H1_eq_H1b H1b_eq_H2
-
diff --git a/tests/lean/apply_tac_bug.lean.expected.out b/tests/lean/apply_tac_bug.lean.expected.out
index 2832fadc15..115f78ce72 100644
--- a/tests/lean/apply_tac_bug.lean.expected.out
+++ b/tests/lean/apply_tac_bug.lean.expected.out
@@ -1,6 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'heq'
   Imported 'macros'
   Imported 'tactic'
   Proved: my_proof_irrel
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index a8c4741ae4..d37d59b1c1 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -1,4 +1,3 @@
-import heq
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
index 871de95c35..13a6976637 100644
--- a/tests/lean/eq3.lean.expected.out
+++ b/tests/lean/eq3.lean.expected.out
@@ -1,6 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'heq'
   Assumed: Vector
   Assumed: n
   Assumed: v1
diff --git a/tests/lean/simp20.lean b/tests/lean/simp20.lean
index 3e33da300e..f6cd3e759e 100644
--- a/tests/lean/simp20.lean
+++ b/tests/lean/simp20.lean
@@ -1,4 +1,3 @@
-import heq
 rewrite_set simple
 
 set_option pp::implicit true
diff --git a/tests/lean/simp20.lean.expected.out b/tests/lean/simp20.lean.expected.out
index d754b383e9..674a86c71f 100644
--- a/tests/lean/simp20.lean.expected.out
+++ b/tests/lean/simp20.lean.expected.out
@@ -1,6 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'heq'
   Set: lean::pp::implicit
   Assumed: g
   Assumed: B