fix tests

Author: kim-em

src/Init/Core.lean

@@ -1371,7 +1371,7 @@ set_option linter.missingDocs false in
 @[deprecated exists_of_subtype (since := "2025-04-04")]
 abbrev existsOfSubtype := @exists_of_subtype
 
-variable {α : Type u} {p : α → Prop}
+variable {α : Sort u} {p : α → Prop}
 
 protected theorem ext : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -1393,7 +1393,7 @@ instance {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] : ReflBEq {x : α
 instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x : α // p x} where
   eq_of_beq h := Subtype.ext (eq_of_beq h)
 
-instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
     else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))

tests/lean/run/simp4.lean

@@ -49,7 +49,7 @@ theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  fail_if_success simp [-Nat.add_eq_zero]
+  fail_if_success simp [-Nat.add_eq_zero_iff]
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]

tests/lean/run/simpStar.lean

@@ -20,7 +20,7 @@ h₂ : g x < 5
 -/
 #guard_msgs in
 theorem ex3 (x y : Nat) (h₁ : f x x = g x) (h₂ : f x x < 5) : f x x + f x x = 0 := by
-  simp [*, -Nat.add_eq_zero] at *
+  simp [*, -Nat.add_eq_zero_iff] at *
   trace_state
   have aux₁ : f x x = g x := h₁
   have aux₂ : g x < 5     := h₂