fix: drop stale .reverse in MePo premise selector (#13747)

This PR fixes the MePo premise selector returning its lowest-scoring
premises instead of its best ones.

Since https://github.com/leanprover/lean4/pull/10917 `mepo` returns
suggestions in score-descending order, but `mepoSelector` still applied
a `.reverse` that predated that change. The `.reverse` flipped the order
to score-ascending, so the subsequent `.take config.maxSuggestions` kept
the `maxSuggestions` worst premises.

Thanks to Xavier Généreux for the report.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/LibrarySuggestions/MePo.lean

@@ -78,6 +78,5 @@ public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4)
     pure <| unweightedScore
   let accept := fun ci => return !isDeniedPremise env ci.name
   let suggestions ← mepo constants score accept config.maxSuggestions p c
-  let suggestions := suggestions
-    |>.reverse  -- we favor constants that appear at the end of `env.constants`
+  -- `mepo` already returns suggestions in score-descending order.
   return suggestions.take config.maxSuggestions

tests/elab/library_suggestions_mepo_order.lean

@@ -0,0 +1,25 @@
+import Lean.LibrarySuggestions.MePo
+
+/-!
+Regression test: the MePo premise selector must return suggestions in
+score-descending order.
+
+A stale `.reverse` in `mepoSelector` (left over from before the selector was
+made score-sorting) flipped the order to score-ascending, so `.take` returned
+the lowest-scoring premises instead of the best ones.
+-/
+
+open Lean Lean.Elab.Tactic Lean.LibrarySuggestions
+
+example (a b : Int) : a + b = b + a := by
+  run_tac do
+    let sel : Selector := mepoSelector (useRarity := false)
+    let s ← sel (← getMainGoal) {}
+    let mut prev? : Option Float := none
+    for x in s do
+      if let some prev := prev? then
+        unless prev ≥ x.score do
+          throwError "MePo suggestions are not score-descending: \
+            score {prev} precedes score {x.score}"
+      prev? := some x.score
+  sorry

tests/elab/library_suggestions_mepo_order.lean.out.expected

@@ -0,0 +1 @@
+library_suggestions_mepo_order.lean:14:0-14:7: warning: declaration uses `sorry`