chore: adaptations for nightly-2026-02-17

[mathlib-nightly-testing]

No description provided.

[github-actions]

Commit Verification Summary

Warning

Some verifications failed. See details below.

Commits to Review (242)

• 1a27131: Update lean-toolchain for testing fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• 385bc88: Update lean-toolchain for testing feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• ed4d276: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 54ab9ec: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 674d49e: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 96790a2: fix clashes with standard library
• ab90fb0: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 2975ae5: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 074ad7a: remove simp annotation for sum_reverse
• 11cf943: Update lean-toolchain for feat: lemmas about sums of lists/arrays/vectors leanprover/lean4#11994
• 4c4d894: Update lean-toolchain for testing feat: @[instance_reducible] part 2 leanprover/lean4#12263
• 0981a21: lake update
• 2d1f297: fixes to @[to_additive] for leanprover#lean4#12263
• 29691de: add an expose
• b5b5223: chore: manual fix the script can't handle
• 54d256b: first attempt at automation
• b8876c2: first batch of automated fixes
• 5d5b2f9: looking good on first 5 errors
• d759d3a: more fixes
• 387d109: more automated fixes
• 6631a9b: more automated fixes
• ea80331: more automated fixes
• bfb40c7: manual fix
• 340ce1c: ah, the script doesn't do cross-file fixes yet
• 5e361fc: more
• 1e53d4e: the rest
• 1e299ca: delete script, not that useful in the end
• 589f7d0: adaptation note
• 75d0c8d: Merge master into nightly-testing
• 30d31c7: chore: adaptations for nightly-2026-02-02
• 21013aa: Merge branch 'bump/nightly-2026-02-02' into nightly-testing
• d7a1160: fix Archive
• 7197c73: nolint exceptions for docBlame linter
• f1b37ec: chore: bump to nightly-2026-02-03
• 8772c6b: merge lean-pr-testing-11994
• d704942: merge lean-pr-testing-12263
• b176a0b: Update lean-toolchain for testing chore: shake core leanprover/lean4#12276
• 2d208fe: lake update
• 552d82f: lake update
• f62bb72: fix test
• a5610de: fix tests
• af64404: cleanup
• 3b56b25: Merge master into nightly-testing
• 699df81: Merge branch 'master' into nightly-testing
• a2e6d91: Merge commit 'af644042004d5987dfcae257cca071a495d2348a' into bump/nightly-2026-02-03
• 933cbd6: chore: adaptations for nightly-2026-02-03
• e95a8cb: Auto-resolved conflicts in lean-toolchain and lake-manifest.json
• 226d511: chore: bump to nightly-2026-02-04
• 8096cc4: Merge master into nightly-testing
• 489d547: lake update
• 094bfc7: deps
• 74a7a62: lake update
• f34d93a: add instance_reducible
• 4bcadff: fixes
• dfdea35: Merge commit 'f34d93a9c1211ef00e6d473c7ce3eb99d1d1de35' into bump/nightly-2026-02-04
• 1bcf34d: chore: adaptations for nightly-2026-02-04
• bb8dff3: fixes
• 695752f: fixes
• 42c7b01: fixes
• 8d4e724: fixes for fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• d28ca26: fixes for fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• aa41720: fixes
• 0126ea7: chore: bump to nightly-2026-02-05
• 79c166e: merge lean-pr-testing-12244
• 9c2f7b1: chore: remove lemmas now in Lean core
• 4ac60fc: lake update
• 9faca84: .
• 3690cf4: Merge master into nightly-testing
• 32620cc: fix
• 20c4c4b: fix: remove simp from le_refl (now handled by Std.le_refl)
• f1180c4: Merge commit '20c4c4b3d8a0ec5aabc72aa3d247f2838d829759' into bump/nightly-2026-02-05
• c8b024a: chore: adaptations for nightly-2026-02-05
• da5be3b: Update lean-toolchain for testing feat: some unification hints leanprover/lean4#12341
• 125088f: Merge master into nightly-testing
• 63d3445: chore: bump to nightly-2026-02-07
• 139c7c0: merge lean-pr-testing-12276
• 2c1bf04: address comments in [Merged by Bors] - chore: adaptations for nightly-2026-02-04 #173
• 9f9b361: Merge master into nightly-testing
• 93c7ab9: lake update
• 5453b7c: lake update
• 0c12c51: lake update importGraph
• afbbb48: chore: bump to nightly-2026-02-08
• ed6aae0: fix merge
• 7b50c4c: Merge branch 'nightly-testing' of github.com:leanprover-community/mathlib4-nightly-testing into nightly-testing
• a9c6d41: lake update
• 9ea620f: Merge master into nightly-testing
• 248e419: fix: restore Basic.lean from after [Merged by Bors] - refactor(CategoryTheory): remove HasForget mathlib4#34741 to fix duplicate declarations
• 5584ab1: adaptations for feat: some unification hints leanprover/lean4#12341
• d915007: adaptations for feat: some unification hints leanprover/lean4#12341
• 2b9cf93: chore: update FindSyntax test for reduced syntax count
• 7bba664: fix(MathlibTest/push): adapt to unification hints from lean4#12341
• 7abfa4b: fixes for feat: some unification hints leanprover/lean4#12341
• 8e0a887: fixes for feat: some unification hints leanprover/lean4#12341
• c1ea32a: merge
• 7f45853: chore: bump to nightly-2026-02-09
• 5fb8301: merge lean-pr-testing-12341
• 3e0af02: fix(GCongr): try syntactic relation matching before whnf
• fb8ff80: fix(GCongr): handle @[reducible] HasSSubset.SSubset in hypothesis classification and tactic
• 7968b3b: fix: adapt proofs to @[reducible] HasEquiv.Equiv and HasSSubset.SSubset
• 64498e1: Merge master into nightly-testing
• 3578f95: chore: remove unnecessary show
• 5db4d63: fix(GCongr): handle @[reducible] HasSSubset.SSubset in whnfR for _Implies goals
• 6b5e9c7: Update lean-toolchain for testing fix: type class resolution cache leanprover/lean4#12286
• c2701d5: lake update aesop
• eb94767: lake update aesop
• 0faf545: fixes for fix: type class resolution cache leanprover/lean4#12286
• 193e4ce: chore: bump to nightly-2026-02-10
• 9d23085: Update lean-toolchain for testing feat: upstream Rat.abs and Int/Rat lemmas from human-eval-lean leanprover/lean4#12412
• d3dafc7: Merge master into nightly-testing
• d29d506: Update lean-toolchain for fix: type class resolution cache leanprover/lean4#12286
• cb59205: fixes for fix: type class resolution cache leanprover/lean4#12286
• 27cc943: Merge branch 'lean-pr-testing-12286' of github.com:leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12286
• 56a490b: cleanup
• 2713b48: Update lean-toolchain for fix: type class resolution cache leanprover/lean4#12286
• 64c738a: Merge branch 'lean-pr-testing-12286' of github.com:leanprover-community/mathlib4-nightly-testing into lean-pr-testing-12286
• e4ee153: fixes
• 0d0e16f: fixes, hopefully revertible later
• 5848b9f: cleanup
• d987a9c: upstream Rat.eq_iff_mul_eq_mul, 'lt_iff_le_not_le' -> 'lt_iff_le_and_not_ge'
• ae9f47a: Update lean-toolchain for feat: upstream Rat.abs and Int/Rat lemmas from human-eval-lean leanprover/lean4#12412
• 2bfb0fe: .
• e2bb437: bad merge
• 2b8e4e8: raise maxHeartbeats
• 441c429: fix
• 0963585: Merge master into nightly-testing
• 24405c0: empty commit for CI for fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• b1bac8b: chore: bump to nightly-2026-02-12
• d5dd8c0: merge lean-pr-testing-12412
• 8dcf318: chore: adaptations for nightly-2026-02-10
• a13fce1: Auto-resolved conflicts in lean-toolchain and lake-manifest.json
• a3b8430: fix test outputs
• d0bd09f: fix bad merge
• 3a3bec8: Merge branch 'bump/nightly-2026-02-10' into nightly-testing
• 75a55da: revert changes to GCongr
• 176e60b: fix tests output again
• 53b834e: fix
• d6b100d: maxheartbeats
• 8d8fab1: fix
• 5eab67a: Update lean-toolchain for fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• 3f80f7b: chore: bump to nightly-2026-02-12
• 7da5050: merge lean-pr-testing-12412
• d647089: Merge master into nightly-testing
• 305026d: bump toolchain (early today, oops!)
• 85a1946: fix lakefile and lake update
• d487a14: remove upstreamed
• ac1deab: Merge remote-tracking branch 'nightly-testing/bump/nightly-2026-02-10' into nightly-testing
• 9d0e1e6: restore a simp
• fa64ca5: remove upstreamed and deprecation
• 7c18a1d: deprecation
• 5b9b3ca: clarify adaptation note
• 7006a01: Merge remote-tracking branch 'nightly-testing/bump/nightly-2026-02-10' into nightly-testing
• 820ed60: lake update
• d7bf79b: fix for fix: disable order and funCC modules in NoopConfig leanprover/lean4#11744
• 7f5579b: fix indentation
• 139e385: Update lean-toolchain for fix: type class resolution cache leanprover/lean4#12286
• bd8f964: chore: bump to nightly-2026-02-13-rev1
• 8889baa: chore: bump to nightly-2026-02-13-rev2
• 88d55d6: fix test
• b9312d5: fix test
• 7523c34: Merge branch 'lean-pr-testing-11744' of github.com:leanprover-community/mathlib4-nightly-testing into lean-pr-testing-11744
• 2535e4c: Merge master into nightly-testing
• 32ff989: nice, most workarounds not needed with univ_out_params
• efb5b53: chore: bump to nightly-2026-02-14
• f5578e3: merge lean-pr-testing-11744
• 9ca1e39: chore: update batteries for List.reverse_singleton fix
• 8edfc65: .
• 0781dca: Merge master into nightly-testing
• aec008a: add @[univ_out_params] where universe params are not determined by inputs
• 2a27ec7: add #adaptation_note for @[univ_out_params] annotations
• d61b93d: add library note on universe output parameters, update adaptation notes
• 082d63c: convert #adaptation_note to -- comments for univ_out_params annotations
• ec04327: fix
• e1835ce: fix
• 8f7035d: fix
• f5364bb: fix
• 47811c9: empty commit to retrigger CI
• 3922e3d: chore: bump to nightly-2026-02-15
• d5f7a05: merge lean-pr-testing-12286
• 27844eb: lake update
• 8cdd715: chore: bump to nightly-2026-02-15-rev1
• d635d93: lake update
• a054c5e: chore: adaptations for nightly-2026-02-15-rev1
• 6120ee2: Merge master into nightly-testing
• d14e64c: chore: bump to nightly-2026-02-16
• 0c55f79: Update lean-toolchain for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• 855b095: fix_backward_defeq script
• 0e83417: lake update batteries
• 9fcbcf0: non-local set_option, added manually
• a0ac8ca: manual fixes, script confused by absence of blank lines
• 711c715: times out without manual fix
• e91d3cc: norm_num tests
• f26fb38: reduce_mod_char
• 6d2f2e8: fix test output
• 59db9db: set_option globally in RingTheory.SimpleModule.Isotypic
• e2c1174: set_option globally in RingTheory.Adjoin.Dimension
• 102945f: set_option a section of LinearAlgebra.FiniteDimensional.Basic
• 65af295: set_option globally in Algebra.Homology.BifunctorAssociator
• 85d85cb: set_option in section in Algebra.Homology.BifunctorHomotopy
• 8dd2ddb: set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
• 7687cfd: set_option globally in Algebra.Homology.BifunctorShift
• 946645b: set_option in section in Geometry.Manifold.Riemannian.Basic
• b39e1e4: set_option in section in NumberTheoryCyclotomic.Basic
• 9e6efa5: set_option in section in Analysis.Distribution.SchwartzSpace.Fourier
• 494f517: global set_option in RingTheory.DedekindDomain.LinearDisjoint
• 56f63e0: manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed
• 3515f91: manual fixes for CategoryTheory.Sites.Descent.IsStack
• f1067a3: manual fixes for Algebra.Homology.DifferentialObject
• a984ac8: manual fixes for Geometry.RingedSpace.PresheafedSpace
• 8767b74: manual fixes for CategoryTheory.Triangulated.Opposite.Functor
• e39a78d: manual fixes in Algebra.Homology.HomotopyCategory.ShortExact
• 32020da: manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing
• 8438a58: manual fixes to CategoryTheory.Sites.Descent.DescentData
• d6bae81: manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string
• 294d68c: adaptation_note
• 1eba589: set_option linter.style.longFile
• 5c1be55: remove unused simp args
• e5979cc: remove noop tactic
• 66671e7: lake update
• 9c203d6: optimistic linter fixes
• 2fddd34: patch and adaptation note
• 08e1756: slightly more care with the linter
• c3dc66b: still getting it right
• b881aee: fix test
• 769144c: chore: adaptations for nightly-2026-02-16
• 3d209fb: fix warning
• 09d194d: fix
• 9cf4e11: fix properly
• c0b8018: Merge master into nightly-testing
• 15d45d5: chore: bump to nightly-2026-02-16-rev1
• b4dcc3c: Merge remote-tracking branch 'nightly-testing/lean-pr-testing-12179' into nightly-testing
• c1044a8: move batteries back to nightly-testing
• 175349b: lake update
• a5c9272: final fixes for Dependent pattern matching bug leanprover/lean4#1279
• 0e4ce36: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• c7c2d56: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• b7cf1d3: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• fff082e: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• 6a1724a: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• dc17606: fix for feat: backward.isDefEq.respectTransparency leanprover/lean4#12179
• 3f3ce2c: chore: adaptations for nightly-2026-02-16-rev1
• d5b4e1e: chore: bump to nightly-2026-02-17
• 00c0601: chore: adaptations for nightly-2026-02-17

View PR diff

\u274c Automated commits (2) - 0/2 verified

Commit	Command	Status
7a5bb90	x: ./fix_backward_defeq.py	❌ Command failed with exit code 1
69f02e0	x: ./fix_backward_defeq.py	❌ Command failed with exit code 1

---

Generated by commit verification CI

[jcommelin]

Please remove this script.