diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean
index b8f411312f..54cbcfef7c 100644
--- a/tests/lean/run/typeclass_coerce.lean
+++ b/tests/lean/run/typeclass_coerce.lean
@@ -14,7 +14,7 @@ class HasCoerce (a b : Type) :=
 def coerce {a b : Type} [HasCoerce a b] : a → b :=
 @HasCoerce.coerce a b _
 
-instance coerceTrans {a b c : Type} [HasCoerce b c] [HasCoerce a b] : HasCoerce a c :=
+instance coerceTrans {a b c : Type} [HasCoerce a b] [HasCoerce b c] : HasCoerce a c :=
 ⟨fun x => coerce (coerce x : b)⟩
 
 instance coerceBoolToProp : HasCoerce Bool Prop :=
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 33e30a0f2f..a3a7f2aca3 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -1,4 +1,4 @@
-sanitychecks.lean:1:0: error: fail to show termination for
+sanitychecks.lean:1:8: error: fail to show termination for
   unsound
 with errors
 structural recursion cannot be used