chore: adaptations for nightly-2026-05-14#224
Merged
Conversation
…esn't fix IsPrestack yet)
The walk-back heuristic lands on the first blank line above the error, but then needs to advance past non-declaration preamble lines to reach an actual target of `set_option ... in`. Previously the script would insert before `variable`, producing invalid syntax; now it skips past such statements.
…en` lines" This reverts commit a3a71e3288d5a7899b501579a32531b7a207d08a.
Added scripts/fix_unused_simp_args.py which parses the \"This simp argument is unused\" warnings from a lake build log and rewrites the corresponding simp call. For plain arguments it drops them; for \`← X\` arguments it rewrites to \`- X\` (simp's own hint notes the \`←\` form has side effects on the simp set even when the rewrite itself is unused, so the \`-\` form preserves that behavior while silencing the warning).
…' into nightly-testing
The strip commit f46fb25 ("strip all `set_option backward.defeqAttrib.useBackward true`") deleted only the set_option line; for files where it had been inserted between two blank lines (typically right after `@[expose] public section`), the deletion left an extra blank line behind. That orphan blank then surfaces as PR-diff noise on every nightly bump branch forked from those files. Eighteen files still carry this orphan on nightly-testing; remove the extra blank in each. No code change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drop the no-longer-existing `Mathlib.Tactic.Linter.DeprecatedModule` import from two deprecation stubs, and add `set_option backward.defeqAttrib.useBackward true in` to the simps-generated natural transformation in `Nondegenerate.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
fgdorais
pushed a commit
that referenced
this pull request
Jun 5, 2026
* remove `change` tactics flagged by unusedTactics linter
* fix
* fix
* fix
* fix
* fix
* fixes
* fixes
* fixes
* fixes
* adaptation note
* linting
* chore: adaptations for nightly-2026-05-03 (#215)
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13651
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* chore: bump to nightly-2026-05-09
* chore: revert spurious blank-line additions
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: revert remaining spurious blank-line additions
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: undo over-eager blank-line reverts (restore lines from PR base)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: bump to nightly-2026-05-10
* chore(Cache/IO): drop `open private` for now-public `Lake.Glob.ofString?`
`Lake.Glob.ofString?` is now `public` in Lake (nightly-2026-05-10), so the
`open private ... from Lake.Load.Toml in` line fails to elaborate and blocks
`lake exe cache get` from building. The call site uses the fully-qualified
name, so dropping the line is sufficient.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore(Data/String/Lemmas): add `length_toList` to `simp` set in leftpad lemmas
Upstream `simp` no longer normalises `s.toList.length` and `s.length` to a common
form, so `simp [leftpad, ...]` leaves a mixed goal that `Nat.sub_add_eq_max` (and
the prefix reasoning at line 34) cannot match. Passing `String.length_toList`
explicitly unifies the two forms and closes both goals.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore(RingTheory/Bialgebra/TensorProduct): enable `backward.defeqAttrib.useBackward` for `comm`
The `rw [comul a]` inside `comm` no longer matches after upstream changes to
defeq attribute handling. Locally re-enabling the backward behaviour with
`set_option backward.defeqAttrib.useBackward true` restores the previous
elaboration and lets the existing proof go through.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* fix: restore mapFreeIso_hom lemma from #38341
Lost during the master-merge resolution in 7aa60c9cea7. The upstream
refactor in #38341 introduced this lemma; the merge dropped it because
the adaptation branch had reorganised the surrounding declarations.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fix: drop stale Reorder defs re-added during merge
`Reorder.permuteUniv` and `Reorder.isEmpty` (on the pre-#36604 shape of
`Reorder`) were deleted by #36604 when the structure was renamed to
`ArgReorder` and a new `Reorder` wrapper was introduced. They were
accidentally re-added during a merge resolution and reference a
`Reorder` type that is not yet in scope at that point.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: adaptations for nightly-2026-05-07 (#218)
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* Revert "chore: more proof-level `irreducible_def` patches" and predecessor
Revert 6c4ca63236b and 265db6f0b35. The cherry-picked Lean fixes 8741db2872
("store eqn-affecting options at definition time instead of eager generation")
and 3d985fc54b ("use `.local` asyncMode for `eqnOptionsExt`") make the
`@[eqns X_def]` override installed by `irreducible_def` win again, so
`simp [X]` / `rw [X]` no longer leak `wrapped.1`. The `X` → `X_def`
workarounds are therefore unnecessary on the adaptation branch.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: restore module-level `set_option backward.defeqAttrib.useBackward true` on three files
These three files need the option set at module scope for reasons
*unrelated* to the eager-eqn-generation bug that the Lean cherry-picks
(8741db2872, 3d985fc54b) addressed — they contain `@[backward_defeq]`-only
simp lemmas whose simp rewrites only fire with `useBackward = true` via
`useImplicitDefEqProof`. Without the option their proofs no longer check
(e.g. `Module.Basis.det`'s `MultilinearMap.mk'` arguments).
The broader revert 60d49842875 dropped them alongside the now-unnecessary
`rw [X]` → `rw [X_def]` workarounds; restore only the `set_option` lines.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* chore: bump to nightly-2026-04-22
* chore: strip all `set_option backward.defeqAttrib.useBackward true`
Baseline for re-adding the option only where actually needed.
* chore: add scoped \`set_option backward.defeqAttrib.useBackward true\`
only where locally needed
Down from the bulk module-level set in 99.7% of mathlib files to
scoped \`set_option ... true in\` before ~170 specific declarations
across 82 files.
Remaining failures all appear to be non-local (option needed on a
transitive dependency, not the failing module itself):
* Mathlib.Order.JordanHolder
* Mathlib.CategoryTheory.Equivalence
* Mathlib.RingTheory.TensorProduct.Maps
These will be fixed by \`scripts/fix_nonlocal_set_option.py\`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore(scripts): thread --value through fix_nonlocal_set_option.py
Allow `--value true` (matching add_set_option.py). Without this, the
script hard-coded 'false' and was unusable for restoring legacy behavior.
* fix(Order/JordanHolder): restructure `Equivalent.snoc` proof
The original relied on simp reducing an equiv chain inside a `let`:
specifically `((finSuccEquivLast.trans (Functor.mapEquiv Option h)).trans
finSuccEquivLast.symm) (Fin.last _)` to `Fin.last _`. Under the stricter
`inferDefEqAttr` rules, simp no longer fires the needed chain through
the `let`-bound equiv in this particular goal shape.
Rewrite the proof to extract `e_last` and `e_castSucc` auxiliary
equalities explicitly, using tactic mode with `show`/`rw`/`simpa`,
so the proof no longer depends on simp magic inside `let`.
* fix(RingTheory/TensorProduct/Maps): use `simpa` instead of `dsimp; exact`
`dsimp` no longer normalizes the nested `AlgebraTensorModule.curry`
applications down to the `f (_ \u2297\u209c _ \u2297\u209c _)` form `h_mul` expects.
`simpa using h_mul _ _ _ _ _ _` handles it — the simp call it wraps
reduces the curry chains successfully.
* fix(CategoryTheory/Equivalence): module-level \`set_option backward.defeqAttrib.useBackward true\`
The \`@[to_dual existing ...]\` validations fail without this option
because the \`Equivalence\` structure's field types are emitted in a
slightly different binder-order shape under the stricter defeq rules,
so the generated \`to_dual\` expected form no longer matches the
structure-generated one. Setting the option at module level restores
the legacy behavior for elaborating this file's structure and its
\`to_dual\`-tagged theorems.
* chore: 2nd round of scoped `set_option backward.defeqAttrib.useBackward true`
After fixing JordanHolder/Equivalence/TensorProduct.Maps, re-ran
`add_set_option.py --value true`. 99 more modules needed the option
locally (scoped per-declaration). Mostly CategoryTheory (especially
Bicategory and Functor APIs).
* chore: file-level `set_option backward.defeqAttrib.useBackward true` on 8 CategoryTheory files
`add_set_option.py` could not fix these locally because the
failures are in `NatIso.ofComponents` / `@[simps!]` bodies where
`aesop` fails to synthesize naturality fields; the option has to
be module-level so that all structure-field elaboration sees it.
* chore: 3rd iteration of scoped + file-level `set_option` additions
Add option per-declaration to 9 more modules via `add_set_option.py`,
and at module level to 2 more (Adjunction/Basic, Limits/Cones) where
local scoping didn't suffice.
* chore: 4th iteration of scoped `set_option backward.defeqAttrib.useBackward true`
164 modules fixed. 15 remaining need file-level option or proof
restructuring (Mates, Grothendieck, Pseudo, KanExtension, etc.).
* chore: file-level `set_option backward.defeqAttrib.useBackward true` on 13 category theory files
Modules with `@[simps!]` / structure-field elaboration that don't
accept scoped set_option (Mates, KanExtension, Elements, Monoidal,
etc.).
* chore: 5th iteration of scoped `set_option backward.defeqAttrib.useBackward true` (72 modules)
* chore: file-level `set_option backward.defeqAttrib.useBackward true` on 17 more files
* chore: 6th iteration scoped set_option additions (27 modules)
* fix(Tactic/Simps): run projection-lemma normalization with \`useBackward=true\`
The \`@[simps!]\` pipeline normalizes the RHS via \`dsimp\` then \`simp\`
to produce the cleanest possible body for the generated projection
lemma. With the stricter \`inferDefEqAttr\` rules, many \`@[simps]\`-generated
lemmas from upstream structures are tagged \`@[backward_defeq]\` only —
without \`useBackward=true\` the \`dsimp\` step doesn't pick them up, the
RHS no longer reduces to a rfl-shape, and the projection lemma ends up
with a compound proof (\`congrArg …\`). \`inferDefEqAttr\` then fails to
tag it, which cascades: every downstream \`@[simps!]\` that relied on
this lemma being rfl also gets a compound proof, and so on.
Forcing \`useBackward=true\` inside \`addProjection\` keeps \`@[simps!]\`'s
dsimp normalization as aggressive as before, so rfl-shaped projections
stay rfl-shaped and \`inferDefEqAttr\` can tag them.
* chore: add scoped `set_option backward.defeqAttrib.useBackward true`
After the `Tactic.Simps.Basic` fix (`@[simps!]` now runs normalization
with `useBackward=true`), many previously-broken downstream files now
only need the option scoped per-declaration. Run `add_set_option.py`
to add it where needed — 409 modules fixed this round.
* chore: file-level `set_option backward.defeqAttrib.useBackward true` on 8 files where scoped failed
* fix(Tactic/DSimpPercent): elaborate `dsimp%` with `useBackward=true`
`dsimp%` runs at definition time and the result is stored in the
theorem's signature. If the defining file doesn't have
`backward.defeqAttrib.useBackward=true`, the stored form differs from
what a use site with the option enabled expects, so `rw`/`simp` match
fails.
Wrap the elaborator in `withOptions (fun opts => ...useBackward.set opts true)`
so `dsimp%` always normalizes under the permissive rules, matching
pre-stricter-inference `dsimp` behavior. This is analogous to the fix
applied to `@[simps!]`'s projection generator.
* Revert "fix(Tactic/DSimpPercent): elaborate `dsimp%` with `useBackward=true`"
This reverts commit dc5c3e65f15867bf3107206a36cb5377f6c063e1.
* fix: scope useBackward=true around `extendRestrictScalarsAdj_counit_app_apply_one_tmul`
This lemma uses `dsimp%` in its type, and since `dsimp%` normalizes at
elaboration time, the stored form depends on `useBackward`. Downstream
users (e.g. `ModuleCat/Monoidal/Adjunction.lean`) set `useBackward=true`
and expect the pre-stricter-inference normal form, so the definition
site must agree.
* fix: proof-level adaptations for 2 files under stricter defeq
For files where `useBackward=true` cannot restore pre-PR behavior because
the stored forms of imported lemmas (generated via `dsimp%`, `@[reassoc]`,
`@[elementwise]` etc. at elaboration time without `useBackward=true`)
differ from use-site expectations, adapt the proofs:
- `RelativeCellComplex.lean`: replace `dsimp; rw [Cell.map_app_objEquiv_symm_δ_index]`
with `exact c.map_app_objEquiv_symm_δ_index`, avoiding dsimp through
`Subcomplex.lift_app_coe` whose `dsimp%` stored form differs.
- `Ext/Map.lean`: reorder and augment the rewrite chain in
`DerivedCategory.map_triangleOfSESδ` so that intermediate forms match
the stored reassoc lemmas; replace a trailing `simp` chain with explicit
simp lemmas that cancel the inserted `commShiftIso.hom ≫ inv` pair.
* fix: add `id_comp` to simp list in `CoGrothendieck.map.map_comp`
Under the stricter defeq inference, the prior `simp only` chain no longer
reduces some `𝟙 _ ≫ ...` residues because the `eqToHom`-from-compound
proofs leave identity morphisms in left-composition position. Adding
`id_comp` to the simp list (alongside the existing `comp_id`) cancels
them and closes the goal.
* fix: spell out `ofIso`'s `s'_comp_ε` and `s₀_comp_δ₁` proofs
The previous `simpa` / `simp` closings relied on `w₀` (whose type contains
`dsimp%`) and the reassoc-generated `s'_comp_ε_assoc` / `s₀_comp_δ₁_assoc`
taking a particular normalized form. Under stricter defeq inference those
stored forms no longer match the use-site goal, so replace the one-line
closers with explicit rewrite chains that apply `w₀`, `ed.s'_comp_ε_assoc`,
and `ed.s₀_comp_δ₁` step by step.
* fix: adapt `colimitLimitToLimitColimit_injective`/`_surjective` proofs
Under stricter defeq inference the stored form of
`ι_colimitLimitToLimitColimit_π_apply` (generated by
`@[elementwise (attr := simp)]`) and `Limit.π_mk` (involving `dsimp%` and
proof-dependent shapes) no longer match through plain `simp`/`rw`. Replace
`simpa using ...` with an explicit `simp only [...]; exact ...`, and
replace the final `rw [← dsimp% e j, dsimp% Limit.π_mk _ _ h]` with
`erw [ι_colimitLimitToLimitColimit_π_apply]; generalize_proofs ...;
erw [Limit.π_mk (h := p6), ← e j]`. The `erw` lets the residual
universe/def-equality differences on the outer namespace be resolved.
Also adapt the intermediate naturality step via an explicit `change` +
`ι_colimMap` rewrite.
* chore: add `set_option backward.defeqAttrib.useBackward true` scoped to failing decls (round 7)
* chore: add useBackward to failing decls (round 8)
* chore: add useBackward to failing decls (round 9, partial)
* fix: add useBackward to fix remaining failures in round 9
* chore: add useBackward to failing decls (round 10)
* chore: add useBackward to failing decls (round 11)
* chore: add useBackward to failing decls (round 12)
* chore: add useBackward to failing decls (round 13)
* chore: partial adds in round 14 (4 files still need manual fix)
* fix: scope useBackward at more decl sites (round 14 manual fixes)
* chore: useBackward on mapComp'_inv_naturality and pullHom_pullHom (doesn't fix IsPrestack yet)
* chore: partial attempts in IsPrestack (remains broken)
* chore: add useBackward to failing decls (round 15)
* fix: Stalk.lean needs useBackward on 4 decls
* chore: add useBackward to failing decls (round 16)
* fix: add useBackward to mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom and variants
* chore: round 17 partial (DescentData still broken)
* chore: partial useBackward on DescentData (still broken)
* chore: partial DescentData fixes (still has cascading issues)
* chore: file-level useBackward on DescentData, minor proof edits
* chore: OpenImmersion.lean useBackward
* chore: partial DescentData - line 352 still has metavar issue
* fix: DescentData + useBackward on mapComp'₀₂₃_hom
* chore: round 18 partial
* fix: Precoverage.lean file-level useBackward
* chore: round 20
* fix: `add_set_option.py` skip `variable`/`include`/`omit`/`open` lines
The walk-back heuristic lands on the first blank line above the error, but
then needs to advance past non-declaration preamble lines to reach an
actual target of `set_option ... in`. Previously the script would insert
before `variable`, producing invalid syntax; now it skips past such
statements.
* chore: round 21 (GammaSpecAdjunction, Gluing)
* Revert "fix: `add_set_option.py` skip `variable`/`include`/`omit`/`open` lines"
This reverts commit a3a71e3288d5a7899b501579a32531b7a207d08a.
* chore: round 22
* chore: round 23
* chore: script-fixed 36 more mathlib modules with useBackward
* fix: add useBackward to 3 decls in Representability.lean
* chore: remove unused simp arguments (326 across 123 files)
Added scripts/fix_unused_simp_args.py which parses the
\"This simp argument is unused\" warnings from a lake build log
and rewrites the corresponding simp call. For plain arguments it
drops them; for \`← X\` arguments it rewrites to \`- X\` (simp's own
hint notes the \`←\` form has side effects on the simp set even
when the rewrite itself is unused, so the \`-\` form preserves
that behavior while silencing the warning).
* chore: fix long lines, `show` -> `change`, drop unused `- X` simp args
* chore: one more long-line fix
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* chore: useBackward on 3 MathlibTest files for lake test
* Empty line
* Bump batteries
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* doc(scripts): document new helpers (fix_unused_simp_args.py, fix_long_lines.py, *_module_set_option.py, fix_nonlocal_set_option.py)
* chore: add `simpNF` nolints for 178 lemmas that simp can now prove
Under the stricter `@[defeq]` inference the set of theorems that `simp`
treats as reflexivity-lemmas shrank slightly, which means a number of
previously-accepted `@[simp]` lemmas can now be derived from other simp
lemmas and so fail the `simpNF` linter. Add them to `nolints.json`
rather than individually removing the `@[simp]` attribute, since the
ideal long-term fix (actually removing the attributes) is better done
in follow-up PRs with proper code-review of each individual lemma.
* chore: bump to nightly-2026-04-23
* cleanup
* revert an unnecessary change
* revert unnecessary changes
* add adaptation notes
* minor fixes, whitespace and PR links
* adaptation notes
* two improvements
* fix
* fix FilteredColimitCommutesFiniteLimit
* fix IsPrestack
* improvements
* improvements
* fix extra degeneracy
* small improvement in DerivedCategory/Ext
* slightly improve the proof in Limits/Shapes/Equalizers.lean
* removed adaptation note for DerivedCategory/Ext/Map
* More
* chore: bump to nightly-2026-04-24
* adapt to lean4#13363: canUnfoldAtMatcher allowlist changes
Adapt proofs to lean4#13363 which replaces the transparency bump from
`.reducible` to `.instances` in `whnfMatcher` with an explicit allowlist
in `canUnfoldAtMatcher`. Class projections like `CategoryStruct.comp`,
`CategoryStruct.id`, `Stream.next?`, `Min.min` etc. are no longer
auto-unfolded in match discriminants and need explicit unfolding in
proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* chore: remove unused helper lemmas from Ordinal/Notation adaptation
Remove `zero_zero_eq`, `one_one_eq`, `repr_zero'`, and `ofNat_unfold`
which were added during the lean4#13363 adaptation but are not used in
any proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13363
* more cleaningup
* adapt Limits/Shapes/ConcreteCategory to lean4#13363
Use `WalkingMulticospan.Hom.id_eq_id` and `Functor.map_id` to reduce
stuck matches on `𝟙` in WalkingMulticospan naturality proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* Bump batteries
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13363
* chore: bump to nightly-2026-04-25
* Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13528
* satisfy linter
* fixes
* archive and counterexamples
* fix: round 30 - Pi/Basic + TensorProduct/Pi after nightly merge
* chore: round 32 fixed by script
* chore: round 33 (5 of 6 fixed by script)
* fix: Biproducts isoCoproduct simp leaves isTrue goal needing subst
* chore: round 34 (3 of 5 by script)
* fix: round 34 SequentialProduct + StdSimplex
* chore: round 35
* chore: round 36
* chore: round 37
* chore: round 37 - remove unused simp args
* chore: avoid 'adaptation note' substring in adaptation note bodies
* chore: round 41 (2 of 3 fixed by script)
* chore: resolve merge conflict in Sheaf/Free.lean
Drop the leftover ιFree_mapFree_inv lemma from the adaption branch; the
upstream refactor (mapFreeIso) replaces it and provides a deprecated alias.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: nolint two simpNF auto-generated lemmas
These are @[simps]-style auto-generated lemmas whose LHS now simplifies via
new simp set behavior; nolint to keep adaption focused.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Remove my custom scripts used for managing lean4#13492 migration
* chore: bump to nightly-2026-04-27
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* chore: bump to nightly-2026-04-28
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* chore: drop stale `DeprecatedModule` import in `RingTheory/Regular/Depth`
The internal `Mathlib.Tactic.Linter.DeprecatedModule` module was removed on
master in 9037b087ee0; `deprecated_module` is now a built-in Lean command.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: extend `lean-pr-testing-13492` set_option pattern to remaining decls
Newly-added or master-merged declarations need the same
`set_option backward.defeqAttrib.useBackward true in` adaptation as the
rest of the lean4#13492 mathlib branch. One genuine proof-level breakage
remains in `AlternatingFaceMapComplex.ε.naturality` (line 233).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fix(AlgebraicTopology): repair `ε.naturality` under stricter defeq
Under lean4#13492, `simp [ChainComplex.toSingle₀Equiv]` no longer expands
the `(toSingle₀Equiv).symm.f 0` redex. Use the explicit projection lemma
`ChainComplex.toSingle₀Equiv_symm_apply_f_zero` instead. Includes
`#adaptation_note`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: extend `useBackward` set_option to two more pushout-product files
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: remove redundant `@[expose]` attributes flagged by lean4#13359
The new `warn.redundantExpose` linter from lean4#13359 reports that these
declarations would be exposed by default, so the explicit attribute is
redundant.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: add `@[expose] public section` to silence private-module warning
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `Pretriangulated.{id,comp}_hom₁/₂/₃`
Under lean4#13492's stricter defeq, `(f ≫ g).hom₃` already simplifies
via the `@[simps]`-generated `triangleCategory_comp` to the form these
manually-written simp lemmas were producing, so simpNF now reports them
as redundant. Lemmas remain available as named references (just not
`@[simp]`).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `coe_id`/`coe_comp` in `Order.Category`
Under lean4#13492's stricter defeq, the `ConcreteCategory` simp lemmas
already cover these — the file comment already noted they are duplicates
"kept for `dsimp`". Lemmas remain available as named references.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` flagged by simpNF in CategoryTheory + Topology
Under lean4#13492's stricter defeq, several auto-generated and
manually-written `@[simp]` lemmas in `CategoryTheory.{Comma/Over,Core,
Functor/KanExtension,Limits/Shapes/Pullback/Iso,ObjectProperty,Sites},
Topology.Category.TopCat.OpenNhds` are flagged as having LHSs that
simplify further. Drop the offending `@[simp]` (via `attribute [-simp]`
on `@[simps]`-generated lemmas, by trimming the `@[simps]` projection
list, or by removing `@[simp]` from manually-written ones).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop more `@[simp]` flagged by simpNF as 'LHS simplifies from'
Finishes Phase 1 of the lean4#13492 simpNF cleanup on `nightly-testing`:
the remaining `Left-hand side simplifies from` reports become non-simp
lemmas (or have the corresponding `@[simps]` projection's `@[simp]`
removed via `attribute [-simp]`). Lemmas remain available as named
references.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `coe_id`/`coe_comp` in `Algebra.Category`
Mirror of the `Order.Category` fixes — these `@[to_additive (attr := simp)]`
lemmas are explicitly documented as duplicates of the `ConcreteCategory`
simp lemmas kept "for `dsimp`". Under lean4#13492's stricter defeq, simp
can already prove them, so drop the simp attribute.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simps!]` on `WeierstrassCurve.{Affine,Jacobian,Projective}.{map,baseChange}`
These are `abbrev`s aliasing the underlying `WeierstrassCurve.{map,baseChange}`,
whose `@[simps]`-generated lemmas (`WeierstrassCurve.map_a₁`, etc.)
already cover what these abbreviations expose. Under lean4#13492's
stricter defeq the simpNF linter flags every `_a₁`...`_a₆` projection as
provable by simp.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simps!]`/`@[simp]` in CategoryTheory bicategory + monoidal
Continues the lean4#13492 simpNF cleanup:
- `Bicategory.Opposites.{op2,op2_unop,unop2,unop2_op}`: drop `@[simps!]`
- `Monoidal.Action.Basic.{actionLeft,actionRight}` (×2): drop `@[simps!]`
- `Bicategory.Functor.LocallyDiscrete.toOplaxFunctor{,'}`: trim
`@[simps!]` projection list to just `map` (the others are redundant)
- `Monoidal.Grp.{id,comp}_hom_hom`: drop `@[simp]`
- `Monoidal.Grp.mkIso`: keep `@[simps!]` (the auto-generated lemmas are
referenced by `@[deprecated] alias`) but `attribute [-simp]` on the
flagged projections.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simp]`/`@[simps]` flagged by simpNF
Continues the lean4#13492 cleanup, mostly trimming `@[simps]` projection
lists or dropping `@[simp]` attributes (`Bicategory.LocallyGroupoid`,
`Monoidal.Mon.mkIso`, `Comma.{toPUnitIdEquiv,toIdPUnitEquiv}`,
`Combinatorics.Graph.noEdge`, `RootSystem.Equiv.comp`,
`Group.Equiv.{monoid,addMonoid}HomCongr{Left,Right}Equiv`,
`Free{Magma,Semigroup}.{map_pure,pure_bind}`).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simps]`/`@[simp]` flagged by simpNF (batch 4)
- `NonUnitalAlgHom.{fst,snd,prod}`: `@[simps]` → `@[simps toFun]`
- `Unitization.{lift,starLift}`: drop `apply_apply` from `@[simps!]` list
- `Unitization.inrNonUnitalAlgHom`: `@[simps]` → `@[simps toFun]`
- `Cat.Hom.comp_obj`, `Cat.{whiskerLeft,whiskerRight}_app`: drop `@[simp]`
- `Graph.copy`: `@[simps]` → `@[simps -isSimp]` + add `[copy]` to
`simp_all` in `copy_eq` proof
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simps]`/`@[simp]` flagged by simpNF (batch 5, big)
Continues the lean4#13492 simpNF cleanup across the long-tail 2-error and
1-error files. Pattern is consistent: trim the `@[simps]` projection list
to drop the redundant projection, or drop `@[simp]` (or its
`(attr := simp)` to_additive directive) on a manually-written lemma. For
a few cases where the auto-generated lemma is referenced downstream, the
`@[simps!]` is kept and `attribute [-simp]` is used to drop only the
`@[simp]` status.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: bump to nightly-2026-04-29
* chore: fix namespace context in `attribute [-simp]` calls
Inside `namespace Foo`, `attribute [-simp] Foo.bar` is interpreted
relative to the current namespace and fails to resolve. Use `_root_.`
prefix on the fully-qualified name so the directive actually fires.
This fixes ~12 of the simpNF errors that the previous batches were
intended to address but where the directive was a no-op.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more simpNF-flagged simp lemmas (batch 6)
Reduces simpNF lint errors from 56 → 20. Patterns used:
- For `@[to_additive (attr := simp)]` cases where only the additive
version is flagged, switch to `@[to_additive] / attribute [simp] foo`
pattern, which puts simp only on the multiplicative version.
- For redundant `_symm_apply` lemmas auto-generated by `@[simps]` on
equivs, switch to `@[simps apply]` (omitting the redundant
`_symm_apply` projection).
- For deeper-recursion projections like `_val_inv_*` in `@[simps!]` on
Units-of-Units structures, drop `@[simps]` entirely or restrict the
projection list.
- Manually-written `@[simp]` lemmas redundant with other simp lemmas:
drop `@[simp]`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more simpNF-flagged simps via explicit projection lists
Reduces simpNF lint errors from 20 → 11. Pattern used: switch from
`@[simps!]` + `attribute [-simp] foo` (which doesn't actually remove
simp from `simps!`-generated lemmas in this lean version) to either:
- `@[simps! GOOD_PROJECTIONS]` listing only projections that should
remain simp lemmas, omitting the redundant deep-recursion ones; or
- `@[simps! TOP_PROJECTIONS]` plus a manually-written non-simp theorem
for the remaining declaration name (e.g. `noEdge_isLink`).
Files: Combinatorics/Graph/Basic, CategoryTheory/Comma/Over/Basic,
CategoryTheory/Core, Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from def equation lemmas
Removes `@[simp]` from `def addY`, `def piPremeasure`,
`def zeroDefaultSupp`, `def equivExterior` (in
WeierstrassCurve, MeasureTheory, Plausible, CliffordAlgebra).
The auto-generated `_eq_1` equation lemmas for these defs are
redundant given other simp lemmas, per simpNF.
Adjusts `Petersson.lean` to drop `-Matrix.SpecialLinearGroup.coe_matrix_coe`
from a simp arg list since that lemma is no longer simp.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* adaptation notes about nolint simpNF
* chore: nolint simpNF on auto-generated equation lemmas
The previous commit added `nolint simpNF` to the parent `def`s, but the
linter still complained about their auto-generated `.eq_1`/`.eq_2` equation
lemmas. Add explicit `attribute [nolint simpNF]` for each.
Also fix Contraction.lean: the `#adaptation_note` was placed between the
doc-comment and the `def`, which is a syntax error. Move it before the
doc-comment.
Linter is now clean.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: add adaptation_note to each `attribute [nolint simpNF]`
Followup to a3dbe9e910c: each bare `attribute [nolint simpNF]` for the
`.eq_1`/`.eq_2` lemmas now has its own `#adaptation_note` so it can be
grepped for and revisited.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* lake update batteries
* chore: fix mutual instance + filtered closure rfl failures
Two unrelated breakages exposed by the master merge:
* `Mathlib/SetTheory/Lists.lean`: the `mutual` block of three `instance`
declarations now triggers an "instance `..._mutual` target ... is not a
type class" error from the new mutual-instance handling. Switch the
mutual-block declarations to `def` and add a separate
`attribute [instance]` afterwards. The old workaround
`attribute [nolint nonClassInstance] Lists.Equiv.decidable._mutual`
is no longer needed.
* `Mathlib/CategoryTheory/Filtered/Small.lean`: two `rfl` calls in
`small_fullSubcategory_{filtered,cofiltered}Closure` started failing
under the new defeq regime. Wrap both theorems with
`set_option backward.defeqAttrib.useBackward true in`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: bump to nightly-2026-04-30
* chore: bump to nightly-2026-05-01
* chore: bump to nightly-2026-05-02
* fix
* adaptation note
* fix bad merge
* adaptation notes
* fix
* fixes
* attributes
* fixes
* fixes via attributes
* fixes
* linter
* nolint
* Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13613
* chore: bump to nightly-2026-05-03
* remove unneeded simp
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13613
* chore: bump to nightly-2026-05-04
* fixes
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* fixes from nightly-testing
* lake-manifest
* lake-manifest
* fix from nightly-testing
* fix test
* chore: bump to nightly-2026-05-05
* chore: restore @[to_additive (attr := simp)] symmetry
PR 215 rewrote a number of `@[to_additive (attr := simp)]` attributes to
`@[to_additive]`, sometimes followed by an asymmetric `attribute [simp]`
on only one side of the to_additive pair. Restore the original symmetric
form everywhere this pattern appears.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Revert "chore: restore @[to_additive (attr := simp)] symmetry"
This reverts commit d79879fec19f7f3ea2ab4f2f038661047c74e7c4.
* fix(to_additive): propagate @[defeq] symmetrically to additive translations
Under lean4#13492's stricter `@[defeq]` inference, `inferDefEqAttr` only tags a
theorem `@[defeq]` if its rfl proof passes `withReducibleAndInstances <| isDefEq
lhs rhs`. For `to_additive`-generated additive lemmas this check fails
systematically — even on cases like `AddMonoidHom.coe_id` whose proof is rfl
and whose multiplicative source `MonoidHom.coe_id` is `@[defeq]`. The result
was a divergence: `dsimp` reduced `(𝟙 X : X → X)` to `id` for `X : GrpCat`
but stopped at `⇑(AddMonoidHom.id X)` for `X : AddGrpCat`, which made simpNF
flag a host of additive `coe_id`/`coe_comp` lemmas as redundant simp lemmas
even though their multiplicative twins were fine.
Fix: in `to_additive`'s `defeqAttr` propagation, after calling `inferDefEqAttr`
on the target, promote it to `@[defeq]` whenever the source is `@[defeq]` and
the target is at least `@[backward_defeq]` (i.e. rfl-shaped). The translation
preserves rfl-ness, so a multiplicative `@[defeq]` source implies the additive
translation should also be `@[defeq]` for symmetric `dsimp` behaviour.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: restore @[to_additive (attr := simp)] symmetry
PR 215 rewrote a number of `@[to_additive (attr := simp)]` attributes to
`@[to_additive]`, sometimes followed by an asymmetric `attribute [simp]`
on only one side of the to_additive pair. Restore the original symmetric
form everywhere this pattern appears.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant @[simps!] on Mon.mkIso / AddMon.mkIso
`mkIso` is an abbrev for `mkIso'`, and `mkIso'` already has `@[simps]`. The
`simps!` projections of `mkIso` would just rederive what `simps` on `mkIso'`
already provides, and simpNF rightly flags the duplicates. Dropping the
`(attr := simps!)` here matches PR 215's original intent and leaves the
`@[to_additive (attr := simp)]` symmetry restoration in place for the rest.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* deprecation
* fix
* deprecation
* chore: restore lost content from #38972 merge in Cartesian/Mon.lean
The merge of master into nightly-testing dropped the `IsMonHom (toUnit M)`,
`IsMonHom η[M]`, `Mono η[M]` instances in the `SemiCartesianMonoidalCategory`
section, plus `IsMonHom.monoidHom` and the matching `yonedaMon.map`. Restore
upstream/master's version of the file and re-add scoped
`backward.defeqAttrib.useBackward true` on `Mon.uniqueHomToTrivial` and
`yonedaMonFullyFaithful` for compatibility with the nightly Lean toolchain.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* add missing imports (as public)
* chore: bump to nightly-2026-05-06
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13613
* chore: bump to nightly-2026-05-07
* fix
* remove `change` tactics flagged by unusedTactics linter
* fix
* fix
* fix
* fix
* fix
* fixes
* fixes
* fixes
* fixes
* adaptation note
* linting
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* chore: revert spurious blank-line additions
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: revert remaining spurious blank-line additions
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: undo over-eager blank-line reverts (restore lines from PR base)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* fix: restore mapFreeIso_hom lemma from #38341
Lost during the master-merge resolution in 7aa60c9cea7. The upstream
refactor in #38341 introduced this lemma; the merge dropped it because
the adaptation branch had reorganised the surrounding declarations.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fix: drop stale Reorder defs re-added during merge
`Reorder.permuteUniv` and `Reorder.isEmpty` (on the pre-#36604 shape of
`Reorder`) were deleted by #36604 when the structure was renamed to
`ArgReorder` and a new `Reorder` wrapper was introduced. They were
accidentally re-added during a merge resolution and reference a
`Reorder` type that is not yet in scope at that point.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore(RingTheory/Bialgebra/TensorProduct): enable `backward.defeqAttrib.useBackward` for `comm`
The `rw [comul a]` inside `comm` no longer matches after upstream changes to
defeq attribute handling. Locally re-enabling the backward behaviour with
`set_option backward.defeqAttrib.useBackward true` restores the previous
elaboration and lets the existing proof go through.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kim Morrison <kim.morrison@anu.edu.au>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* fixes
* fixes
* fix
* fix
* chore: bump to nightly-2026-05-11
* partial fixes
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13636
* fixes
* fix
* fix
* chore: remove orphan blank lines left by f46fb2595a2 strip
The strip commit f46fb2595a ("strip all `set_option
backward.defeqAttrib.useBackward true`") deleted only the set_option
line; for files where it had been inserted between two blank lines
(typically right after `@[expose] public section`), the deletion left
an extra blank line behind. That orphan blank then surfaces as PR-diff
noise on every nightly bump branch forked from those files.
Eighteen files still carry this orphan on nightly-testing; remove the
extra blank in each. No code change.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: adaptations for nightly-2026-05-10 (#219)
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13636
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13636
* refactor: use `simpa using!` for lean4 PR 13636 (reducible-close)
* chore: bump batteries pin to 5796d42 (simpa using! transformation)
* fix: convert 10 additional sites to `simpa using!` (post-Jack-wrapping master drift)
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13636
* fix: convert 11 more sites to `simpa using!` (second batch)
* fix: revert over-converted using! in non-simpa tactics (filter_upwards, convert, induction)
* fix: convert ~14 more sites to `simpa using!` (third batch + WittVector macro)
* fix: convert 4 more sites to `simpa using!` (fourth batch)
* fix: convert 4 more sites to `simpa using!` (fifth batch)
* fix: convert 7 more sites to `simpa using!` (sixth batch)
* fix: convert 9 more sites to `simpa using!` (seventh batch)
* chore: bump to nightly-2026-05-12
* fix: convert 2 more sites to `simpa using!` (eighth batch)
* fix: convert 9 more sites to `simpa using!` (ninth batch)
* fix: convert 1 more site to `simpa using!` (tenth batch)
* fix: convert 2 more sites to `simpa using!` (eleventh batch)
* fix: line 194 of ZMod (missed in previous batch)
* style: split long lines exceeding 100 chars after `using!` conversion
* fix: restructure Ramification.lean simpa to single-line (line-split broke parser in struct literal)
* fix: revert using! to using in FunctorExtension (test if Mathlib master simp lemmas resolve)
* fix: restore FunctorExtension and Filtration to pristine (using! conversion was incorrect)
* fix: restore FunctorExtension/Filtration with using! + disable longLine linter for affected decls
* Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13715
* fixes
* update simps config
* fix test
* update
* fix: add `simpaUsingBang` to flexible linter's allowed-finishers set
* fix: convert 9 Archive sites to `simpa using!`
* fix: convert 7 Counterexamples sites to `simpa using!`
* docstrings to appease linter
* style: split long line in DimensionPolynomial
* chore(nightly-testing): fix build after lean updates
Drop the no-longer-existing `Mathlib.Tactic.Linter.DeprecatedModule` import
from two deprecation stubs, and add `set_option backward.defeqAttrib.useBackward true in`
to the simps-generated natural transformation in `Nondegenerate.lean`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13651
* chore: fix `WhitespaceLinter` test
* chore: bump to nightly-2026-05-13
* chore: adaptations for nightly-2026-05-13
* chore: adaptations for nightly-2026-05-11 (#220)
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
* chore: adaptations for nightly-2026-05-12 (#221)
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* chore: adaptations for nightly-2026-05-13 (#222)
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* chore: adaptations for nightly-2026-05-13 (#223)
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* chore: bump to nightly-2026-05-14
* chore: adaptations for nightly-2026-05-14
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13651
* chore: adaptations for nightly-2026-05-14 (#224)
* chore: add useBackward to failing decls (round 13)
* chore: partial adds in round 14 (4 files still need manual fix)
* fix: scope useBackward at more decl sites (round 14 manual fixes)
* chore: useBackward on mapComp'_inv_naturality and pullHom_pullHom (doesn't fix IsPrestack yet)
* chore: partial attempts in IsPrestack (remains broken)
* chore: add useBackward to failing decls (round 15)
* fix: Stalk.lean needs useBackward on 4 decls
* chore: add useBackward to failing decls (round 16)
* fix: add useBackward to mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom and variants
* chore: round 17 partial (DescentData still broken)
* chore: partial useBackward on DescentData (still broken)
* chore: partial DescentData fixes (still has cascading issues)
* chore: file-level useBackward on DescentData, minor proof edits
* chore: OpenImmersion.lean useBackward
* chore: partial DescentData - line 352 still has metavar issue
* fix: DescentData + useBackward on mapComp'₀₂₃_hom
* chore: round 18 partial
* fix: Precoverage.lean file-level useBackward
* chore: round 20
* fix: `add_set_option.py` skip `variable`/`include`/`omit`/`open` lines
The walk-back heuristic lands on the first blank line above the error, but
then needs to advance past non-declaration preamble lines to reach an
actual target of `set_option ... in`. Previously the script would insert
before `variable`, producing invalid syntax; now it skips past such
statements.
* chore: round 21 (GammaSpecAdjunction, Gluing)
* Revert "fix: `add_set_option.py` skip `variable`/`include`/`omit`/`open` lines"
This reverts commit a3a71e3288d5a7899b501579a32531b7a207d08a.
* chore: round 22
* chore: round 23
* chore: script-fixed 36 more mathlib modules with useBackward
* fix: add useBackward to 3 decls in Representability.lean
* chore: remove unused simp arguments (326 across 123 files)
Added scripts/fix_unused_simp_args.py which parses the
\"This simp argument is unused\" warnings from a lake build log
and rewrites the corresponding simp call. For plain arguments it
drops them; for \`← X\` arguments it rewrites to \`- X\` (simp's own
hint notes the \`←\` form has side effects on the simp set even
when the rewrite itself is unused, so the \`-\` form preserves
that behavior while silencing the warning).
* chore: fix long lines, `show` -> `change`, drop unused `- X` simp args
* chore: one more long-line fix
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* chore: useBackward on 3 MathlibTest files for lake test
* Empty line
* Bump batteries
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13492
* doc(scripts): document new helpers (fix_unused_simp_args.py, fix_long_lines.py, *_module_set_option.py, fix_nonlocal_set_option.py)
* chore: add `simpNF` nolints for 178 lemmas that simp can now prove
Under the stricter `@[defeq]` inference the set of theorems that `simp`
treats as reflexivity-lemmas shrank slightly, which means a number of
previously-accepted `@[simp]` lemmas can now be derived from other simp
lemmas and so fail the `simpNF` linter. Add them to `nolints.json`
rather than individually removing the `@[simp]` attribute, since the
ideal long-term fix (actually removing the attributes) is better done
in follow-up PRs with proper code-review of each individual lemma.
* chore: bump to nightly-2026-04-23
* cleanup
* revert an unnecessary change
* revert unnecessary changes
* add adaptation notes
* minor fixes, whitespace and PR links
* adaptation notes
* two improvements
* fix
* fix FilteredColimitCommutesFiniteLimit
* fix IsPrestack
* improvements
* improvements
* fix extra degeneracy
* small improvement in DerivedCategory/Ext
* slightly improve the proof in Limits/Shapes/Equalizers.lean
* removed adaptation note for DerivedCategory/Ext/Map
* More
* chore: bump to nightly-2026-04-24
* adapt to lean4#13363: canUnfoldAtMatcher allowlist changes
Adapt proofs to lean4#13363 which replaces the transparency bump from
`.reducible` to `.instances` in `whnfMatcher` with an explicit allowlist
in `canUnfoldAtMatcher`. Class projections like `CategoryStruct.comp`,
`CategoryStruct.id`, `Stream.next?`, `Min.min` etc. are no longer
auto-unfolded in match discriminants and need explicit unfolding in
proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* chore: remove unused helper lemmas from Ordinal/Notation adaptation
Remove `zero_zero_eq`, `one_one_eq`, `repr_zero'`, and `ofNat_unfold`
which were added during the lean4#13363 adaptation but are not used in
any proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13363
* more cleaningup
* adapt Limits/Shapes/ConcreteCategory to lean4#13363
Use `WalkingMulticospan.Hom.id_eq_id` and `Functor.map_id` to reduce
stuck matches on `𝟙` in WalkingMulticospan naturality proofs.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* Bump batteries
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13363
* chore: bump to nightly-2026-04-25
* Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13528
* satisfy linter
* fixes
* archive and counterexamples
* fix: round 30 - Pi/Basic + TensorProduct/Pi after nightly merge
* chore: round 32 fixed by script
* chore: round 33 (5 of 6 fixed by script)
* fix: Biproducts isoCoproduct simp leaves isTrue goal needing subst
* chore: round 34 (3 of 5 by script)
* fix: round 34 SequentialProduct + StdSimplex
* chore: round 35
* chore: round 36
* chore: round 37
* chore: round 37 - remove unused simp args
* chore: avoid 'adaptation note' substring in adaptation note bodies
* chore: round 41 (2 of 3 fixed by script)
* chore: resolve merge conflict in Sheaf/Free.lean
Drop the leftover ιFree_mapFree_inv lemma from the adaption branch; the
upstream refactor (mapFreeIso) replaces it and provides a deprecated alias.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: nolint two simpNF auto-generated lemmas
These are @[simps]-style auto-generated lemmas whose LHS now simplifies via
new simp set behavior; nolint to keep adaption focused.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Remove my custom scripts used for managing lean4#13492 migration
* chore: bump to nightly-2026-04-27
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* chore: bump to nightly-2026-04-28
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* chore: drop stale `DeprecatedModule` import in `RingTheory/Regular/Depth`
The internal `Mathlib.Tactic.Linter.DeprecatedModule` module was removed on
master in 9037b087ee0; `deprecated_module` is now a built-in Lean command.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: extend `lean-pr-testing-13492` set_option pattern to remaining decls
Newly-added or master-merged declarations need the same
`set_option backward.defeqAttrib.useBackward true in` adaptation as the
rest of the lean4#13492 mathlib branch. One genuine proof-level breakage
remains in `AlternatingFaceMapComplex.ε.naturality` (line 233).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fix(AlgebraicTopology): repair `ε.naturality` under stricter defeq
Under lean4#13492, `simp [ChainComplex.toSingle₀Equiv]` no longer expands
the `(toSingle₀Equiv).symm.f 0` redex. Use the explicit projection lemma
`ChainComplex.toSingle₀Equiv_symm_apply_f_zero` instead. Includes
`#adaptation_note`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: extend `useBackward` set_option to two more pushout-product files
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: remove redundant `@[expose]` attributes flagged by lean4#13359
The new `warn.redundantExpose` linter from lean4#13359 reports that these
declarations would be exposed by default, so the explicit attribute is
redundant.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: add `@[expose] public section` to silence private-module warning
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `Pretriangulated.{id,comp}_hom₁/₂/₃`
Under lean4#13492's stricter defeq, `(f ≫ g).hom₃` already simplifies
via the `@[simps]`-generated `triangleCategory_comp` to the form these
manually-written simp lemmas were producing, so simpNF now reports them
as redundant. Lemmas remain available as named references (just not
`@[simp]`).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `coe_id`/`coe_comp` in `Order.Category`
Under lean4#13492's stricter defeq, the `ConcreteCategory` simp lemmas
already cover these — the file comment already noted they are duplicates
"kept for `dsimp`". Lemmas remain available as named references.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` flagged by simpNF in CategoryTheory + Topology
Under lean4#13492's stricter defeq, several auto-generated and
manually-written `@[simp]` lemmas in `CategoryTheory.{Comma/Over,Core,
Functor/KanExtension,Limits/Shapes/Pullback/Iso,ObjectProperty,Sites},
Topology.Category.TopCat.OpenNhds` are flagged as having LHSs that
simplify further. Drop the offending `@[simp]` (via `attribute [-simp]`
on `@[simps]`-generated lemmas, by trimming the `@[simps]` projection
list, or by removing `@[simp]` from manually-written ones).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop more `@[simp]` flagged by simpNF as 'LHS simplifies from'
Finishes Phase 1 of the lean4#13492 simpNF cleanup on `nightly-testing`:
the remaining `Left-hand side simplifies from` reports become non-simp
lemmas (or have the corresponding `@[simps]` projection's `@[simp]`
removed via `attribute [-simp]`). Lemmas remain available as named
references.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from `coe_id`/`coe_comp` in `Algebra.Category`
Mirror of the `Order.Category` fixes — these `@[to_additive (attr := simp)]`
lemmas are explicitly documented as duplicates of the `ConcreteCategory`
simp lemmas kept "for `dsimp`". Under lean4#13492's stricter defeq, simp
can already prove them, so drop the simp attribute.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simps!]` on `WeierstrassCurve.{Affine,Jacobian,Projective}.{map,baseChange}`
These are `abbrev`s aliasing the underlying `WeierstrassCurve.{map,baseChange}`,
whose `@[simps]`-generated lemmas (`WeierstrassCurve.map_a₁`, etc.)
already cover what these abbreviations expose. Under lean4#13492's
stricter defeq the simpNF linter flags every `_a₁`...`_a₆` projection as
provable by simp.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simps!]`/`@[simp]` in CategoryTheory bicategory + monoidal
Continues the lean4#13492 simpNF cleanup:
- `Bicategory.Opposites.{op2,op2_unop,unop2,unop2_op}`: drop `@[simps!]`
- `Monoidal.Action.Basic.{actionLeft,actionRight}` (×2): drop `@[simps!]`
- `Bicategory.Functor.LocallyDiscrete.toOplaxFunctor{,'}`: trim
`@[simps!]` projection list to just `map` (the others are redundant)
- `Monoidal.Grp.{id,comp}_hom_hom`: drop `@[simp]`
- `Monoidal.Grp.mkIso`: keep `@[simps!]` (the auto-generated lemmas are
referenced by `@[deprecated] alias`) but `attribute [-simp]` on the
flagged projections.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simp]`/`@[simps]` flagged by simpNF
Continues the lean4#13492 cleanup, mostly trimming `@[simps]` projection
lists or dropping `@[simp]` attributes (`Bicategory.LocallyGroupoid`,
`Monoidal.Mon.mkIso`, `Comma.{toPUnitIdEquiv,toIdPUnitEquiv}`,
`Combinatorics.Graph.noEdge`, `RootSystem.Equiv.comp`,
`Group.Equiv.{monoid,addMonoid}HomCongr{Left,Right}Equiv`,
`Free{Magma,Semigroup}.{map_pure,pure_bind}`).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simps]`/`@[simp]` flagged by simpNF (batch 4)
- `NonUnitalAlgHom.{fst,snd,prod}`: `@[simps]` → `@[simps toFun]`
- `Unitization.{lift,starLift}`: drop `apply_apply` from `@[simps!]` list
- `Unitization.inrNonUnitalAlgHom`: `@[simps]` → `@[simps toFun]`
- `Cat.Hom.comp_obj`, `Cat.{whiskerLeft,whiskerRight}_app`: drop `@[simp]`
- `Graph.copy`: `@[simps]` → `@[simps -isSimp]` + add `[copy]` to
`simp_all` in `copy_eq` proof
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more `@[simps]`/`@[simp]` flagged by simpNF (batch 5, big)
Continues the lean4#13492 simpNF cleanup across the long-tail 2-error and
1-error files. Pattern is consistent: trim the `@[simps]` projection list
to drop the redundant projection, or drop `@[simp]` (or its
`(attr := simp)` to_additive directive) on a manually-written lemma. For
a few cases where the auto-generated lemma is referenced downstream, the
`@[simps!]` is kept and `attribute [-simp]` is used to drop only the
`@[simp]` status.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: bump to nightly-2026-04-29
* chore: fix namespace context in `attribute [-simp]` calls
Inside `namespace Foo`, `attribute [-simp] Foo.bar` is interpreted
relative to the current namespace and fails to resolve. Use `_root_.`
prefix on the fully-qualified name so the directive actually fires.
This fixes ~12 of the simpNF errors that the previous batches were
intended to address but where the directive was a no-op.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more simpNF-flagged simp lemmas (batch 6)
Reduces simpNF lint errors from 56 → 20. Patterns used:
- For `@[to_additive (attr := simp)]` cases where only the additive
version is flagged, switch to `@[to_additive] / attribute [simp] foo`
pattern, which puts simp only on the multiplicative version.
- For redundant `_symm_apply` lemmas auto-generated by `@[simps]` on
equivs, switch to `@[simps apply]` (omitting the redundant
`_symm_apply` projection).
- For deeper-recursion projections like `_val_inv_*` in `@[simps!]` on
Units-of-Units structures, drop `@[simps]` entirely or restrict the
projection list.
- Manually-written `@[simp]` lemmas redundant with other simp lemmas:
drop `@[simp]`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: trim more simpNF-flagged simps via explicit projection lists
Reduces simpNF lint errors from 20 → 11. Pattern used: switch from
`@[simps!]` + `attribute [-simp] foo` (which doesn't actually remove
simp from `simps!`-generated lemmas in this lean version) to either:
- `@[simps! GOOD_PROJECTIONS]` listing only projections that should
remain simp lemmas, omitting the redundant deep-recursion ones; or
- `@[simps! TOP_PROJECTIONS]` plus a manually-written non-simp theorem
for the remaining declaration name (e.g. `noEdge_isLink`).
Files: Combinatorics/Graph/Basic, CategoryTheory/Comma/Over/Basic,
CategoryTheory/Core, Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant `@[simp]` from def equation lemmas
Removes `@[simp]` from `def addY`, `def piPremeasure`,
`def zeroDefaultSupp`, `def equivExterior` (in
WeierstrassCurve, MeasureTheory, Plausible, CliffordAlgebra).
The auto-generated `_eq_1` equation lemmas for these defs are
redundant given other simp lemmas, per simpNF.
Adjusts `Petersson.lean` to drop `-Matrix.SpecialLinearGroup.coe_matrix_coe`
from a simp arg list since that lemma is no longer simp.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13528
* adaptation notes about nolint simpNF
* chore: nolint simpNF on auto-generated equation lemmas
The previous commit added `nolint simpNF` to the parent `def`s, but the
linter still complained about their auto-generated `.eq_1`/`.eq_2` equation
lemmas. Add explicit `attribute [nolint simpNF]` for each.
Also fix Contraction.lean: the `#adaptation_note` was placed between the
doc-comment and the `def`, which is a syntax error. Move it before the
doc-comment.
Linter is now clean.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: add adaptation_note to each `attribute [nolint simpNF]`
Followup to a3dbe9e910c: each bare `attribute [nolint simpNF]` for the
`.eq_1`/`.eq_2` lemmas now has its own `#adaptation_note` so it can be
grepped for and revisited.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* lake update batteries
* chore: fix mutual instance + filtered closure rfl failures
Two unrelated breakages exposed by the master merge:
* `Mathlib/SetTheory/Lists.lean`: the `mutual` block of three `instance`
declarations now triggers an "instance `..._mutual` target ... is not a
type class" error from the new mutual-instance handling. Switch the
mutual-block declarations to `def` and add a separate
`attribute [instance]` afterwards. The old workaround
`attribute [nolint nonClassInstance] Lists.Equiv.decidable._mutual`
is no longer needed.
* `Mathlib/CategoryTheory/Filtered/Small.lean`: two `rfl` calls in
`small_fullSubcategory_{filtered,cofiltered}Closure` started failing
under the new defeq regime. Wrap both theorems with
`set_option backward.defeqAttrib.useBackward true in`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: bump to nightly-2026-04-30
* chore: bump to nightly-2026-05-01
* chore: bump to nightly-2026-05-02
* fix
* adaptation note
* fix bad merge
* adaptation notes
* fix
* fixes
* attributes
* fixes
* fixes via attributes
* fixes
* linter
* nolint
* Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13613
* chore: bump to nightly-2026-05-03
* remove unneeded simp
* Update lean-toolchain for https://github.com/leanprover/lean4/pull/13613
* chore: bump to nightly-2026-05-04
* fixes
* Apply suggestions from code review
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
* fixes from nightly-testing
* lake-manifest
* lake-manifest
* fix from nightly-testing
* fix test
* chore: bump to nightly-2026-05-05
* chore: restore @[to_additive (attr := simp)] symmetry
PR 215 rewrote a number of `@[to_additive (attr := simp)]` attributes to
`@[to_additive]`, sometimes followed by an asymmetric `attribute [simp]`
on only one side of the to_additive pair. Restore the original symmetric
form everywhere this pattern appears.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Revert "chore: restore @[to_additive (attr := simp)] symmetry"
This reverts commit d79879fec19f7f3ea2ab4f2f038661047c74e7c4.
* fix(to_additive): propagate @[defeq] symmetrically to additive translations
Under lean4#13492's stricter `@[defeq]` inference, `inferDefEqAttr` only tags a
theorem `@[defeq]` if its rfl proof passes `withReducibleAndInstances <| isDefEq
lhs rhs`. For `to_additive`-generated additive lemmas this check fails
systematically — even on cases like `AddMonoidHom.coe_id` whose proof is rfl
and whose multiplicative source `MonoidHom.coe_id` is `@[defeq]`. The result
was a divergence: `dsimp` reduced `(𝟙 X : X → X)` to `id` for `X : GrpCat`
but stopped at `⇑(AddMonoidHom.id X)` for `X : AddGrpCat`, which made simpNF
flag a host of additive `coe_id`/`coe_comp` lemmas as redundant simp lemmas
even though their multiplicative twins were fine.
Fix: in `to_additive`'s `defeqAttr` propagation, after calling `inferDefEqAttr`
on the target, promote it to `@[defeq]` whenever the source is `@[defeq]` and
the target is at least `@[backward_defeq]` (i.e. rfl-shaped). The translation
preserves rfl-ness, so a multiplicative `@[defeq]` source implies the additive
translation should also be `@[defeq]` for symmetric `dsimp` behaviour.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: restore @[to_additive (attr := simp)] symmetry
PR 215 rewrote a number of `@[to_additive (attr := simp)]` attributes to
`@[to_additive]`, sometimes followed by an asymmetric `attribute [simp]`
on only one side of the to_additive pair. Restore the original symmetric
form everywhere this pattern appears.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* chore: drop redundant @[simps!] on Mon.mkIso / AddMon.mkIso
`mkIso` is an abbrev for `mkIso'`, and `mkIso'` already has `@[simps]`. The
`simps!` projections of `mkIso` would just rederive what `simps` on `mkIso'`
already provides, and simpNF rightly flags the duplicates. Dropping the
`(attr := simps!)` here matches PR 215's original intent and leaves the
`@[to_additive (attr := simp)]` symmetry restoration in place for the rest.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* deprecation
* fix
* deprecation
* chore: restore lost content from #38972 merge in Cartesian/Mon.lean
The merge of master into nightly-testing dropped the `IsMonHom (toUnit M)`,
`IsMonHom η[M]`, `Mono η[M]` instances in the `SemiCartesianMonoidalCategory`
section, plus `IsMonHom.monoidHom` and the matching `yonedaMon.map`. Restore
upstream/master's version of the file and re-add scoped
`backward.defeqAttrib.useBackward true` on `Mon.uniqueHomToTrivial` and
`yonedaMonFullyFaithful` for compatibility with the nightly Lean toolchain.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* add missing imports (as…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
8 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.