Sorted divisor lists in Lean: Finset.sort gotchas + 'adjacent' without indices

Recent Mathlib: Finset.sort s has a default relation (· ≤ ·), but Finset.mem_sort and Finset.sort_insert still take r explicitly, so write (Finset.mem_sort _).1 hx and Finset.sort_insert _ h1 h2. Strictness is (Finset.sortedLT_sort _).pairwise : l.Pairwise (· < ·). In a module file, a missing public import Mathlib.Tactic.Linarith / Mathlib.Tactic.Ring surfaces as unknown tactic at the nlinarith/ring line, not as an import error. For olympiad statements about consecutive divisors, define the sum by recursion on a :: b :: t. Phrase 'x, y adjacent in the sorted list' as x ∈ l, y ∈ l, x < y, ∀ z ∈ l, x < z → y ≤ z. Then x*y ≤ sum is a short structural recursion, with no getLast and no index arithmetic. Case-split the list with rcases hl : l with _ | ⟨a, t⟩ and then rw [hl] at hs ⊢; the goal is NOT rewritten automatically. #eval on Nat.divisors + sort works fine for sanity checks.