diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean
index f8c349a6e9..ea135c5015 100644
--- a/tests/compiler/strictOrSimp.lean
+++ b/tests/compiler/strictOrSimp.lean
@@ -8,4 +8,4 @@ if strictOr (C == 0) (spin b) then "hello"
 else "world"
 
 def main (xs : List String) : IO Unit :=
-IO.println (f xs.head!.toNat)
+IO.println (f 0)
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 213a41dd01..6cf09f3e51 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:11:0: error: type mismatch at application
 term
   m
 has type
-  @PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat Nat.DecidableEq)
+  @PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b))
 but is expected to have type
-  @PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat Nat.DecidableEq)
+  @PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b))
diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean
index f6234d76ae..ec1dba0fe2 100644
--- a/tests/lean/trust0/basic.lean
+++ b/tests/lean/trust0/basic.lean
@@ -62,7 +62,7 @@ def hasDecEq : ∀ (a b : Nat), Decidable (a = b)
     | isFalse xney => isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney))
 
 instance : DecidableEq ℕ :=
-{decEq := hasDecEq}
+hasDecEq
 
 def repeat.{u} {α : Type u} (f : ℕ → α → α) : ℕ → α → α
 | 0,         a => a