diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out
index 6b465d023ce7..6d86058b2e5d 100644
--- a/tests/lean/ppMotives.lean.expected.out
+++ b/tests/lean/ppMotives.lean.expected.out
@@ -4,7 +4,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match x_2, x with
         | a, Nat.zero => fun x => a
-        | a, b.succ => fun x => (x.fst.fst a).succ)
+        | a, b.succ => fun x => (x.1 a).succ)
         f)
     x
 protected def Nat.add : Nat → Nat → Nat :=
@@ -13,7 +13,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
         | a, Nat.zero => fun x => a
-        | a, b.succ => fun x => (x.fst.fst a).succ)
+        | a, b.succ => fun x => (x.1 a).succ)
         f)
     x
 theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
diff --git a/tests/lean/run/diagRec.lean b/tests/lean/run/diagRec.lean
index dd386bc45daa..c37833531dbc 100644
--- a/tests/lean/run/diagRec.lean
+++ b/tests/lean/run/diagRec.lean
@@ -12,11 +12,9 @@ info: [reduction] unfolded declarations (max: 407, num: 3):
   ⏎
   Or.rec ↦ 144
   ⏎
-  Acc.rec ↦ 108[reduction] unfolded reducible declarations (max: 352, num: 3):
+  Acc.rec ↦ 108[reduction] unfolded reducible declarations (max: 352, num: 2):
     Nat.casesOn ↦ 352
-  ⏎
-  Or.casesOn ↦ 144
-   PProd.fst ↦ 126use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+   Or.casesOn ↦ 144use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
index 7408d3dcc9a7..8966ef27fc23 100644
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -8,5 +8,5 @@ fun x =>
       | 0 => fun x => 1
       | n.succ => fun x =>
         let y := 42;
-        2 * x.1.1)
+        2 * x.1)
       f