feat: projected minima and maxima #11938

datokrat · 2026-01-08T12:53:05Z

This PR introduces projected minima and maxima, also known as "argmin/argmax", for lists under the names List.minOn and List.maxOn. It also introduces List.minIdxOn and List.maxIdxOn, which return the index of the minimal or maximal element. Moreover, there are variants with ? suffix that return an Option.

datokrat · 2026-01-12T23:38:14Z

!radar

leanprover-radar · 2026-01-12T23:38:18Z

Benchmark results for 95b0a13 against ff87bcb are in! @datokrat

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.8G (+3.1%)
🟥 grind_list2.lean//instructions: +3.3G (+5.0%)
🟥 size/init/.olean.private//bytes: +3MiB (+1.4%)
🟥 size/init/.olean.server//bytes: +112kiB (+1.1%)
🟥 size/init/.olean//bytes: +793kiB (+0.9%)

Medium changes (1🟥)

🟥 sigma iterator//instructions: +5.1G (+12.5%)

Small changes (3✅, 11🟥)

🟥 build/module/Init.Data.List//instructions: +68.1M (+13.9%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -17.3M (-2.2%)
🟥 build/module/Lake.Config.Package//instructions: +14.2M (+0.4%)
✅ build/module/Lean//instructions: -11.4M (-0.6%)
🟥 charactersIn//instructions: +78.4M (+0.2%)
🟥 grind_ring_5.lean//instructions: +18.1M (+0.2%)
🟥 iterators (elab)//instructions: +4.9M (+0.1%)
🟥 language server startup with ileans//instructions: +77.1M (+0.3%)
🟥 size/all/.ilean//bytes: +208kiB (+0.3%)
🟥 size/all/.olean.private//bytes: +3MiB (+0.3%)
🟥 size/all/.olean.server//bytes: +112kiB (+0.4%)
🟥 size/all/.olean//bytes: +793kiB (+0.2%)
✅ unionfind//instructions: -3.0M (-0.0%)

leanprover-bot · 2026-01-13T00:55:07Z

Reference manual CI status:

✅ Reference manual branch lean-pr-testing-11938 has successfully built against this PR. (2026-01-13 00:55:04) View Log
🟡 Reference manual branch lean-pr-testing-11938 build against this PR didn't complete normally. (2026-01-13 00:55:55) View Log
✅ Reference manual branch lean-pr-testing-11938 has successfully built against this PR. (2026-01-13 12:05:14) View Log
🟡 Reference manual branch lean-pr-testing-11938 build against this PR didn't complete normally. (2026-01-13 12:06:29) View Log
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase abed967ded244a582114e95a6052b8c8035b5f39 --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force reference manual CI using the force-manual-ci label. (2026-01-13 13:12:24)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-16 14:12:13)

leanprover-community-bot · 2026-01-13T01:43:40Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-11938 build failed against this PR. (2026-01-13 01:43:39) View Log
💥 Mathlib branch lean-pr-testing-11938 build failed against this PR. (2026-01-13 12:23:41) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase abed967ded244a582114e95a6052b8c8035b5f39 --onto e56351da7ae15673a5bc2b83e7fb70e1fbd988ca. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-13 13:12:22)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase abed967ded244a582114e95a6052b8c8035b5f39 --onto 3dfd125337305c9de6ddcc7c0330c50f0e39fb8e. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-14 16:47:24)
✅ Mathlib branch lean-pr-testing-11938 has successfully built against this PR. (2026-01-16 15:34:47) View Log

datokrat · 2026-01-13T10:32:04Z

I was not able to reproduce the two major runtime changes in grind tests locally using multiple alternating iterations and will run radar again to see whether it could be a fluke.

datokrat · 2026-01-13T10:34:47Z

!radar

leanprover-radar · 2026-01-13T10:34:53Z

Benchmark results for ec5c1a4 against ff87bcb are in! @datokrat

Warnings (2)

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run build has different system configurations between commits.
Runner for run other has different system configurations between commits.

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.8G (+3.1%)
🟥 grind_list2.lean//instructions: +3.3G (+5.0%)
🟥 size/init/.olean.private//bytes: +3MiB (+1.4%)
🟥 size/init/.olean.server//bytes: +112kiB (+1.1%)
🟥 size/init/.olean//bytes: +793kiB (+0.9%)

Medium changes (1🟥)

🟥 sigma iterator//instructions: +5.1G (+12.5%)

Small changes (3✅, 12🟥)

🟥 build/module/Init.Data.List//instructions: +68.1M (+13.9%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -15.5M (-2.0%)
🟥 build/module/Lake.Config.Package//instructions: +13.0M (+0.4%)
✅ build/module/Lean//instructions: -11.6M (-0.6%)
🟥 charactersIn//instructions: +77.8M (+0.2%)
🟥 grind_ring_5.lean//instructions: +20.6M (+0.2%)
🟥 iterators (elab)//instructions: +5.0M (+0.1%)
🟥 iterators (interpreted)//instructions: +4.9M (+0.0%)
🟥 language server startup with ileans//instructions: +76.7M (+0.3%)
🟥 size/all/.ilean//bytes: +208kiB (+0.3%)
🟥 size/all/.olean.private//bytes: +3MiB (+0.3%)
🟥 size/all/.olean.server//bytes: +112kiB (+0.4%)
🟥 size/all/.olean//bytes: +793kiB (+0.2%)
✅ unionfind//instructions: -2.7M (-0.0%)

datokrat · 2026-01-13T12:21:14Z

!radar

leanprover-radar · 2026-01-13T12:21:20Z

Benchmark results for 11b026e against abed967 are in! @datokrat

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.7G (+3.1%)
🟥 grind_list2.lean//instructions: +3.3G (+5.1%)
🟥 size/init/.olean.private//bytes: +2MiB (+0.7%)
🟥 size/init/.olean.server//bytes: +92kiB (+0.9%)
🟥 size/init/.olean//bytes: +660kiB (+0.7%)

Small changes (1✅, 8🟥)

🟥 build/module/Init.Data.List//instructions: +67.7M (+13.8%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -18.3M (-2.3%)
🟥 charactersIn//instructions: +61.8M (+0.2%)
🟥 grind_ring_5.lean//instructions: +20.1M (+0.2%)
🟥 lake build clean//instructions: +13.0G (+0.6%)
🟥 language server startup with ileans//instructions: +54.6M (+0.2%)
🟥 size/all/.ilean//bytes: +159kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +92kiB (+0.3%)

datokrat · 2026-01-14T15:20:07Z

!radar

leanprover-radar · 2026-01-14T15:20:16Z

Benchmark results for f39beb6 against abed967 are in! @datokrat

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.7G (+3.1%)
🟥 grind_list2.lean//instructions: +3.3G (+5.0%)
🟥 size/init/.olean.private//bytes: +2MiB (+0.7%)
🟥 size/init/.olean.server//bytes: +92kiB (+0.9%)
🟥 size/init/.olean//bytes: +649kiB (+0.7%)

Small changes (1✅, 8🟥)

🟥 build/module/Init.Data.List//instructions: +67.6M (+13.7%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -17.4M (-2.2%)
🟥 charactersIn//instructions: +62.1M (+0.2%)
🟥 grind_ring_5.lean//instructions: +19.1M (+0.2%)
🟥 lake build clean//instructions: +10.8G (+0.5%)
🟥 language server startup with ileans//instructions: +55.6M (+0.2%)
🟥 size/all/.ilean//bytes: +158kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +92kiB (+0.3%)

datokrat · 2026-01-15T08:25:48Z

!radar

leanprover-radar · 2026-01-15T08:26:02Z

Benchmark results for 2616136 against abed967 are in! @datokrat

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.7G (+3.1%)
🟥 grind_list2.lean//instructions: +3.2G (+4.9%)
🟥 size/init/.olean.private//bytes: +2MiB (+0.7%)
🟥 size/init/.olean.server//bytes: +92kiB (+0.9%)
🟥 size/init/.olean//bytes: +649kiB (+0.7%)

Small changes (1✅, 8🟥)

🟥 build/module/Init.Data.List//instructions: +66.6M (+13.6%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -17.7M (-2.2%)
🟥 charactersIn//instructions: +62.1M (+0.2%)
🟥 grind_ring_5.lean//instructions: +19.3M (+0.2%)
🟥 lake build clean//instructions: +12.8G (+0.6%)
🟥 language server startup with ileans//instructions: +55.7M (+0.2%)
🟥 size/all/.ilean//bytes: +158kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +92kiB (+0.3%)

datokrat · 2026-01-15T08:26:56Z

!radar

leanprover-radar · 2026-01-15T08:27:19Z

Benchmark results for 32c4071 against abed967 are in! @datokrat

Large changes (4🟥)

🟥 grind_bitvec2.lean//instructions: +6.7G (+3.1%)
🟥 size/init/.olean.private//bytes: +2MiB (+0.7%)
🟥 size/init/.olean.server//bytes: +92kiB (+0.9%)
🟥 size/init/.olean//bytes: +649kiB (+0.7%)

Small changes (1✅, 9🟥)

🟥 build/module/Init.Data.List//instructions: +67.7M (+13.8%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -16.1M (-2.0%)
🟥 charactersIn//instructions: +61.8M (+0.2%)
🟥 grind_ring_5.lean//instructions: +18.3M (+0.2%)
🟥 lake build clean//instructions: +12.9G (+0.6%)
🟥 language server startup with ileans//instructions: +56.7M (+0.2%)
🟥 leanchecker --fresh Init//instructions: +1.8G (+0.4%)
🟥 size/all/.ilean//bytes: +158kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +92kiB (+0.3%)

datokrat · 2026-01-15T09:33:57Z

!radar

leanprover-radar · 2026-01-15T09:34:05Z

Benchmark results for b79ecbe against abed967 are in! @datokrat

Large changes (5🟥)

🟥 grind_bitvec2.lean//instructions: +6.7G (+3.1%)
🟥 grind_list2.lean//instructions: +3.2G (+5.0%)
🟥 size/init/.olean.private//bytes: +2MiB (+0.7%)
🟥 size/init/.olean.server//bytes: +92kiB (+0.9%)
🟥 size/init/.olean//bytes: +649kiB (+0.7%)

Small changes (1✅, 9🟥)

🟥 build/module/Init.Data.List//instructions: +67.1M (+13.6%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -17.9M (-2.3%)
🟥 charactersIn//instructions: +61.8M (+0.2%)
🟥 grind_ring_5.lean//instructions: +18.2M (+0.2%)
🟥 lake build clean//instructions: +12.8G (+0.6%)
🟥 language server startup with ileans//instructions: +54.2M (+0.2%)
🟥 leanchecker --fresh Init//instructions: +1.8G (+0.4%)
🟥 size/all/.ilean//bytes: +158kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +92kiB (+0.3%)

datokrat · 2026-01-16T23:01:35Z

!radar

leanprover-radar · 2026-01-16T23:01:44Z

Benchmark results for 28de00f against 86da5ae are in! @datokrat

Large changes (3🟥)

🟥 size/init/.olean.private//bytes: +2MiB (+0.8%)
🟥 size/init/.olean.server//bytes: +96kiB (+0.9%)
🟥 size/init/.olean//bytes: +675kiB (+0.7%)

Small changes (1✅, 12🟥)

🟥 build/module/Init.Data.List//instructions: +66.3M (+13.5%) (reduced significance based on *//lines)
🟥 build/module/Init.Data.Order//bytes .ilean: +94B (+19.8%)
✅ build/module/Lake.CLI//instructions: -16.8M (-2.1%)
🟥 build/module/Lake.Config.Package//instructions: +12.8M (+0.4%)
🟥 charactersIn//instructions: +64.3M (+0.2%)
🟥 grind_bitvec2.lean//instructions: +463.8M (+0.2%)
🟥 grind_list2.lean//instructions: +179.2M (+0.3%)
🟥 lake build clean//instructions: +12.9G (+0.6%)
🟥 language server startup with ileans//instructions: +61.7M (+0.3%)
🟥 leanchecker --fresh Init//instructions: +1.8G (+0.4%)
🟥 size/all/.ilean//bytes: +169kiB (+0.2%)
🟥 size/all/.olean.server//bytes: +96kiB (+0.3%)
🟥 size/all/.olean//bytes: +675kiB (+0.2%)

datokrat force-pushed the paul/minOn branch from 7695d47 to a756714 Compare January 9, 2026 21:44

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 13, 2026

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11938

4e62d16

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jan 13, 2026

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11938

aaba440

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 13, 2026

Update lean-toolchain for testing leanprover/lean4#11938

9ecf335

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jan 13, 2026

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 13, 2026

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 13, 2026

Update lean-toolchain for leanprover/lean4#11938

f4e4262

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 13, 2026

Update lean-toolchain for leanprover/lean4#11938

1f09214

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 13, 2026

Update lean-toolchain for leanprover/lean4#11938

67668f5

datokrat force-pushed the paul/minOn branch from ec5c1a4 to 11b026e Compare January 13, 2026 12:20

datokrat added the changelog-library Library label Jan 13, 2026

datokrat added 27 commits January 16, 2026 23:54

import modules

2298374

add docstrings

c52089e

squash simps

056d30b

cleanups

7ea6a3f

cleanups; remove left_leaning lemmas

ab06abb

wip

620467f

protect

4a5161e

protect

071045f

fixes

a75c8ad

remove IsLinearOrder parameters

2bf42af

minOn cleanups

39bdc45

simp/grind annotations

f877831

remove four grind annotations

2eb381a

rerun radar

9c0e85e

remove all grind annotation for performance debugging

7626fa3

unfold imports in grind_list_2 explicit

ead6af3

disable new imports

1537a80

import order modules

c312b49

import MinMaxOn again

7486026

optimize instances

283ba8b

import all of Init

b14afb3

make instances local

9c99c53

solve performance issues by unexposing opposite instances?

13753f9

reduce priority of instances

6cf2d62

fix List.List. declarations

d2b2778

set irreducible flag safely

7909eac

typo

28de00f

datokrat force-pushed the paul/minOn branch from 95203df to 28de00f Compare January 16, 2026 23:01

feat: projected minima and maxima #11938

Are you sure you want to change the base?

feat: projected minima and maxima #11938

Uh oh!

Conversation

datokrat commented Jan 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 12, 2026

Uh oh!

leanprover-radar commented Jan 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jan 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot commented Jan 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 13, 2026

Uh oh!

datokrat commented Jan 13, 2026

Uh oh!

leanprover-radar commented Jan 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 13, 2026

Uh oh!

leanprover-radar commented Jan 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 14, 2026

Uh oh!

leanprover-radar commented Jan 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 15, 2026

Uh oh!

leanprover-radar commented Jan 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 15, 2026

Uh oh!

leanprover-radar commented Jan 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 15, 2026

Uh oh!

leanprover-radar commented Jan 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jan 16, 2026

Uh oh!

leanprover-radar commented Jan 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

datokrat commented Jan 8, 2026 •

edited

Loading

leanprover-radar commented Jan 12, 2026 •

edited

Loading

leanprover-bot commented Jan 13, 2026 •

edited

Loading

leanprover-community-bot commented Jan 13, 2026 •

edited

Loading

leanprover-radar commented Jan 13, 2026 •

edited

Loading

leanprover-radar commented Jan 13, 2026 •

edited

Loading

leanprover-radar commented Jan 14, 2026 •

edited

Loading

leanprover-radar commented Jan 15, 2026 •

edited

Loading

leanprover-radar commented Jan 15, 2026 •

edited

Loading

leanprover-radar commented Jan 15, 2026 •

edited

Loading

leanprover-radar commented Jan 16, 2026 •

edited

Loading