diff --git a/tests/lean/608.hlean.expected.out b/tests/lean/608.hlean.expected.out
index 704c6fbad1..cfe04c3477 100644
--- a/tests/lean/608.hlean.expected.out
+++ b/tests/lean/608.hlean.expected.out
@@ -1,9 +1,9 @@
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
 λ (ob : Type) (C : precategory ob) (a : ob), ID a
 definition function.id [reducible] : Π {A : Type}, A → A
-is_typeof
+λ (A : Type) (a : A), a
 -----------
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
 λ (ob : Type) (C : precategory ob) (a : ob), ID a
 definition function.id [reducible] : Π {A : Type}, A → A
-is_typeof
+λ (A : Type) (a : A), a
diff --git a/tests/lean/626b.hlean.expected.out b/tests/lean/626b.hlean.expected.out
index cf173cb72d..8d718f68b7 100644
--- a/tests/lean/626b.hlean.expected.out
+++ b/tests/lean/626b.hlean.expected.out
@@ -3,7 +3,7 @@ x : S¹
 ⊢ bool
 626b.hlean:4:50: error: don't know how to synthesize placeholder
 x : S¹
-⊢ eq.transport (λ (a : S¹), bool) loop ?M_1 = ?M_1
+⊢ eq.pathover (λ (a : S¹), bool) ?M_1 loop ?M_1
 626b.hlean:4:32: error: failed to add declaration 'f' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (x : S¹),
diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out
index ea7e7e8189..0c3a8eb3d8 100644
--- a/tests/lean/abbrev1.lean.expected.out
+++ b/tests/lean/abbrev1.lean.expected.out
@@ -3,4 +3,4 @@ definition tst : ℕ
 definition tst : ℕ
 foo ℕ
 definition tst1 : num
-is_typeof num 10
+(λ (A : Type₁) (a : A), a) num 10
diff --git a/tests/lean/extra/616b.hlean b/tests/lean/extra/616b.hlean
index 82bc0f39ed..257e176c77 100644
--- a/tests/lean/extra/616b.hlean
+++ b/tests/lean/extra/616b.hlean
@@ -5,5 +5,5 @@ definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P)
 begin
   induction x,
     exact (Pc a),
-    refine (!tr_constant ⬝ Pp H)
+    refine (pathover_of_eq (Pp H))
 end
diff --git a/tests/lean/extra/616c.hlean b/tests/lean/extra/616c.hlean
index 1ac3d79d87..2527a4eb55 100644
--- a/tests/lean/extra/616c.hlean
+++ b/tests/lean/extra/616c.hlean
@@ -4,5 +4,5 @@ definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P)
 begin
   induction x,
     exact (Pc a),
-    refine (!tr_constant ⬝ Pp H)
+    refine (pathover_of_eq (Pp H))
 end
diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean
index 16ad87e564..5a8c224722 100644
--- a/tests/lean/hott/433.hlean
+++ b/tests/lean/hott/433.hlean
@@ -86,7 +86,7 @@ namespace pi
   (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
   definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
     (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
-    (Π(b : B a), (sigma.sigma_eq p idp) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
+    (Π(b : B a), (sigma.sigma_eq p !pathover_tr) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
   eq.rec_on p (λg, !equiv.refl) g
   end
 
diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean
index c61c1a8261..bd35214793 100644
--- a/tests/lean/hott/614.hlean
+++ b/tests/lean/hott/614.hlean
@@ -1,6 +1,6 @@
 import hit.circle
 
-open circle eq int
+open circle eq int pi
 
 attribute circle.rec [recursor]
 
@@ -8,18 +8,14 @@ protected definition my_decode {x : circle} (c : circle.code x) : base = x :=
 begin
   induction x,
   { revert c, exact power loop },
-  { apply eq_of_homotopy, intro a,
-    refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
-    rewrite [transport_code_loop_inv,power_con,succ_pred]
-  }
+  { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
+    rewrite [power_con,transport_code_loop]},
 end
 
 protected definition my_decode' {x : circle} : circle.code x → base = x :=
 begin
   induction x,
   { exact power loop},
-  { apply eq_of_homotopy, intro a,
-    refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
-    rewrite [transport_code_loop_inv,power_con,succ_pred]
-  }
+  { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
+    rewrite [power_con,transport_code_loop]},
 end
diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean
index d712a7debc..128910e8ed 100644
--- a/tests/lean/hott/615.hlean
+++ b/tests/lean/hott/615.hlean
@@ -1,6 +1,6 @@
 -- HoTT
 import hit.circle
-open circle eq int
+open circle eq int pi
 
 attribute circle.rec circle.elim [recursor 4]
 
@@ -12,10 +12,9 @@ begin
 end
 
 protected definition my_decode {x : circle} : my_code x → base = x :=
-begin
-  induction x,
-  { exact power loop},
-  { apply eq_of_homotopy, intro a,
-    refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
-    rewrite [transport_code_loop_inv,power_con,succ_pred]}
-end
+  begin
+    induction x,
+    { exact power loop},
+    { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
+      rewrite [power_con,transport_code_loop]},
+  end
diff --git a/tests/lean/hott/ind_tac3.hlean b/tests/lean/hott/ind_tac3.hlean
index ea604357f8..40370f87d9 100644
--- a/tests/lean/hott/ind_tac3.hlean
+++ b/tests/lean/hott/ind_tac3.hlean
@@ -1,5 +1,4 @@
-import cubical.pathover
-open cubical
+open eq
 
 set_option pp.implicit true
 set_option pp.universes true