test: update test output following stage0 update (#4815)

this is a consequenc of #4807 that only shows up once that change made
it to stage0, it seem.

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 :=

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

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