chore(tests/lean): fix tests

tests/lean/record_rec_protected.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)

tests/lean/run/coe6.lean

@@ -1,4 +1,4 @@
-import data.unit
+-- import data.unit
 open unit
 namespace play
 constant int : Type.{1}

tests/lean/run/confuse_ind.lean

@@ -1,4 +1,4 @@
-import logic data.prod data.unit
+import logic data.prod
 
 definition mk_arrow (A : Type) (B : Type) :=
 A → A → B

tests/lean/run/decidable.lean

@@ -1,4 +1,4 @@
-import logic data.unit data.bool
+import logic  data.bool
 open bool unit decidable
 
 constants a b c : bool

tests/lean/run/group3.lean

@@ -8,7 +8,7 @@
 -- Various structures with 1, *, inv, including groups.
 
 import logic.eq
-import data.unit data.sigma data.prod
+import data.sigma data.prod
 import algebra.binary
 
 open eq

tests/lean/run/record1.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 
 structure point (A : Type) (B : Type) :=

tests/lean/run/record2.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 set_option pp.universes true
 

tests/lean/run/record3.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 
 structure point (A : Type) (B : Type) :=

tests/lean/run/record4.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 set_option structure.eta_thm true
 

tests/lean/run/record5.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)

tests/lean/run/record6.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)

tests/lean/run/record7.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)