chore: adaptations for nightly-2026-02-21#186

Open

mathlib-nightly-testing[bot] wants to merge 10000 commits intobump/v4.30.0from

bump/nightly-2026-02-21

This pull request is big! We're only showing the most recent 250 commits

Commits on Feb 5, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
lake update
kim-em
committed
deps
kim-em
committed
lake update
kim-em
committed
add instance_reducible
kim-em
committed
fixes
kim-em
committed
Merge remote-tracking branch 'upstream/master' into bump/v4.29.0
mathlib4-bot
committed
Merge commit 'f34d93a9c1211ef00e6d473c7ce3eb99d1d1de35' into bump/nightly-2026-02-04
mathlib4-bot
committed
chore: adaptations for nightly-2026-02-04
mathlib4-bot
committed
fixes
kim-em
committed
fixes
kim-em
committed
fixes
kim-em
committed
fixes for leanprover/lean4#11744
kim-em
committed
fixes for leanprover/lean4#11744
kim-em
committed
fixes
kim-em
committed
chore: bump to nightly-2026-02-05
mathlib-nightly-testing[bot]
committed
merge lean-pr-testing-12244
mathlib-nightly-testing[bot]
committed
chore: remove lemmas now in Lean core

kim-em
and
claude
committed
lake update
kim-em
committed
.
kim-em
committed

Commits on Feb 6, 2026

Commits on Feb 8, 2026

Commits on Feb 9, 2026

Commits on Feb 10, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
chore: remove unnecessary show

kim-em
and
claude
committed
fix(GCongr): handle @[reducible] HasSSubset.SSubset in whnfR for _Implies goals

kim-em
and
claude
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12286
leanprover-community-mathlib4-bot
committed
lake update aesop
kim-em
committed
lake update aesop
kim-em
committed
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
mathlib4-bot
committed
fixes for leanprover/lean4#12286
kim-em
committed
chore: bump to nightly-2026-02-10
mathlib-nightly-testing[bot]
committed
Merge remote-tracking branch 'upstream/master' into bump/v4.29.0
mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/12412
leanprover-community-mathlib4-bot
committed

Commits on Feb 11, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12286
leanprover-community-mathlib4-bot
committed
fixes for leanprover/lean4#12286
kim-em
committed
Merge branch 'lean-pr-testing-12286' of github.com:leanprover-community/mathlib4-nightly-testing
kim-em
committed
cleanup
kim-em
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12286
leanprover-community-mathlib4-bot
committed
Merge branch 'lean-pr-testing-12286' of github.com:leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12286
kim-em
committed
fixes
kim-em
committed
fixes, hopefully revertible later
kim-em
committed
cleanup
kim-em
committed
upstream Rat.eq_iff_mul_eq_mul, 'lt_iff_le_not_le' -> 'lt_iff_le_and_not_ge'
datokrat
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/12412
leanprover-community-mathlib4-bot
committed
.
kim-em
committed
bad merge
kim-em
committed
raise maxHeartbeats
kim-em
committed
fix
kim-em
committed

Commits on Feb 12, 2026

Commits on Feb 13, 2026

Commits on Feb 15, 2026

Commits on Feb 16, 2026

Commits on Feb 17, 2026

Commits on Feb 18, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed

Commits on Feb 20, 2026