fix tests

Author: kim-em

src/Init/Data/Fin/Lemmas.lean

@@ -1137,6 +1137,7 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
+@[deprecated val_mul (since := "2025-10-26")]
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 

tests/lean/run/symbolFrequency.lean

@@ -7,4 +7,4 @@ open Lean PremiseSelection
 #guard_msgs in
 run_meta do
   let f ← symbolFrequency `Nat
-  logInfo m!"{decide (10000 < f)}"
+  logInfo m!"{decide (5000 < f)}"

tests/lean/run/symbolFrequency_foldRelevantConsts.lean

@@ -9,19 +9,19 @@ open Lean PremiseSelection
 #guard_msgs in
 run_meta do
   let ci ← getConstInfo `List.append_assoc
-  let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
+  let consts ← ci.type.foldRelevantConstants (init := #[]) (fun n ns => return ns.push n)
   logInfo m!"{consts}"
 
 /-- info: [List, Ne, HAppend.hAppend, List.nil, Eq, List.head] -/
 #guard_msgs in
 run_meta do
   let ci ← getConstInfo `List.head_append_right
-  let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
+  let consts ← ci.type.foldRelevantConstants (init := #[]) (fun n ns => return ns.push n)
   logInfo m!"{consts}"
 
 /-- info: [Array, Nat, LT.lt, Array.size, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/
 #guard_msgs in
 run_meta do
   let ci ← getConstInfo `Array.eraseIdx.induct
-  let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
+  let consts ← ci.type.foldRelevantConstants (init := #[]) (fun n ns => return ns.push n)
   logInfo m!"{consts}"