fix: make tests be aware of new instance names (#3936)

#3089 caused the stage0 update to cause a number of tests to start
failing because they were using the old instance names.

tests/lean/2220.lean.expected.out

@@ -1,18 +1,16 @@
-@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
-  (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
+@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
     (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
     (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
-  (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
+@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
 2220.lean:25:19-25:24: error: failed to synthesize instance
   HPow Nat Nat Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 2220.lean:26:12-26:17: error: failed to synthesize instance
   HPow Nat Nat Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
+@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int

tests/lean/366.lean.expected.out

@@ -1,6 +1,6 @@
 [Meta.synthInstance] ✅ Inhabited Nat
   [Meta.synthInstance] new goal Inhabited Nat
-    [Meta.synthInstance.instances] #[@instInhabited, instInhabitedNat]
+    [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
   [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
     [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
   [Meta.synthInstance] result instInhabitedNat

tests/lean/decreasing_by.lean.expected.out

@@ -15,17 +15,17 @@ Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
 decreasing_by.lean:81:0-81:13: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:91:0-91:22: error: unsolved goals
 case a
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
@@ -35,7 +35,7 @@ The arguments relate at each recursive call as follows:
 Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:110:0-113:17: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)

tests/lean/defInst.lean.expected.out

@@ -9,4 +9,4 @@ false
 true
 true
 def instMMonad : Monad M :=
-ReaderT.instMonadReaderT
+ReaderT.instMonad

tests/lean/issue2981.lean.expected.out

@@ -3,9 +3,10 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only once, in most general context)
 n : Nat
-⊢ (invImage (fun x => x) instWellFoundedRelation).1 n n.succ
+⊢ (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 n n.succ
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ sizeOf n < sizeOf n.succ
-n m : Nat ⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩
+n m : Nat
+⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelationOfSizeOf).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩

tests/lean/run/PPTopDownAnalyze.lean

@@ -344,7 +344,7 @@ set_option pp.analyze.trustSubtypeMk true in
 #testDelabN Lean.Xml.parse
 #testDelabN Add.noConfusionType
 #testDelabN List.filterMapM.loop
-#testDelabN instMonadReaderOf
+#testDelabN instMonadReaderOfOfMonadLift
 #testDelabN instInhabitedPUnit
 #testDelabN Lean.Syntax.getOptionalIdent?
 #testDelabN Lean.Meta.ppExpr

tests/lean/run/simpGround1.lean

@@ -43,7 +43,7 @@ example (h : xs = [6, 7, 8]) : f4 [1, 2, 3] 5 = xs := by
   simp (config := { ground := true })
   rw [h]
 
-#check List.instAppendList
+#check List.instAppend
 
 example (h : xs = [4, 3, 2]) : ([1, 2, 3].map (· + 1) |>.reverse) = xs := by
   simp (config := { ground := true })

tests/lean/unifHintAndTC.lean.expected.out

@@ -1,4 +1,4 @@
 (100, 400)
 (49, 576, 576)
 def g : Int → Int → Int :=
-fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMulInt) x y
+fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMul) x y