diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
index de9da6ceed..7df176e76c 100644
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -14,6 +14,11 @@ context:
 x✝¹ : Nat
 x✝ : [] ≠ []
 ⊢ Nat
+hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
+context:
+a b x✝¹ : Nat
+x✝ : [a, b] ≠ []
+⊢ Nat
 hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
 x✝¹ : Nat
@@ -25,11 +30,6 @@ x✝² : List Nat
 x✝¹ : Nat
 x✝ : x✝² ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
-context:
-a b x✝¹ : Nat
-x✝ : [a, b] ≠ []
-⊢ Nat
 case inl
 p q : Prop
 h✝ : p
diff --git a/tests/lean/lcnfTypes.lean b/tests/lean/lcnfTypes.lean
index e69e077ddc..4477bdafc8 100644
--- a/tests/lean/lcnfTypes.lean
+++ b/tests/lean/lcnfTypes.lean
@@ -106,25 +106,14 @@ def weird1 (c : Bool) : (cond c List Array) Nat :=
 
 #eval test ``weird1
 
-def compatible (declName₁ declName₂ : Name) : MetaM Unit := do
-  let type₁ ← LCNF.getOtherDeclBaseType declName₁ []
-  let type₂ ← LCNF.getOtherDeclBaseType declName₂ []
-  unless LCNF.compatibleTypesQuick type₁ type₂ do
-    throwError "{declName₁} : {← ppExpr type₁}\ntype is not compatible with\n{declName₂} : {← ppExpr type₂}"
-
 axiom monadList₁.{u} : Monad List.{u}
 axiom monadList₂.{u} : Monad (fun α : Type u => List α)
 
--- set_option pp.all true
-#eval compatible ``monadList₁ ``monadList₂
-
 axiom lamAny₁ (c : Bool) : Monad (fun α : Type => cond c (List α) (Array α))
 axiom lamAny₂ (c : Bool) : Monad (cond c List.{0} Array.{0})
 #eval test ``lamAny₁
 #eval test ``lamAny₂
 
-#eval compatible ``lamAny₁ ``lamAny₂
-
 def testMono (declName : Name) : MetaM Unit := do
   let base ← LCNF.getOtherDeclBaseType declName []
   let mono ← LCNF.toMonoType base
diff --git a/tests/lean/lcnfTypes.lean.expected.out b/tests/lean/lcnfTypes.lean.expected.out
index f12ba8dded..ca005aa514 100644
--- a/tests/lean/lcnfTypes.lean.expected.out
+++ b/tests/lean/lcnfTypes.lean.expected.out
@@ -37,10 +37,8 @@ Lean.Elab.Term.elabTerm : Lean.Syntax →
 Nat.add : Nat → Nat → Nat
 Magma.mul : Magma → ◾ → ◾ → ◾
 weird1 : Bool → ◾
-
 lamAny₁ : Bool → Monad ◾
 lamAny₂ : Bool → Monad ◾
-
 Term.constFold : List Ty → Ty → Term ◾ ◾ → Term ◾ ◾
 Term.denote : List Ty → Ty → Term ◾ ◾ → HList Ty ◾ ◾ → ◾
 HList.get : ◾ → ◾ → List ◾ → ◾ → HList ◾ ◾ ◾ → Member ◾ ◾ ◾ → ◾
diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
index f83e52a17c..627be6e06d 100644
--- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out
+++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -13,12 +13,6 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
-syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
-context:
-α β : Type
-x : Fam2 α β
-n a : Nat
-⊢ Nat
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
@@ -26,3 +20,9 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
+syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
+context:
+α β : Type
+x : Fam2 α β
+n a : Nat
+⊢ Nat