chore: adaptations for nightly-2026-05-07 (#218)

* Update lean-toolchain for leanprover/lean4#13492

* Revert "chore: more proof-level `irreducible_def` patches" and predecessor

Revert 6c4ca63 and 265db6f. 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 leanprover/lean4#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 leanprover/lean4#13492

* chore: useBackward on 3 MathlibTest files for lake test

* Empty line

* Bump batteries

* Update lean-toolchain for leanprover/lean4#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 leanprover/lean4#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 leanprover/lean4#13363

* chore: bump to nightly-2026-04-25

* Update lean-toolchain for testing leanprover/lean4#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 leanprover/lean4#13528

* chore: bump to nightly-2026-04-28

* Update lean-toolchain for leanprover/lean4#13528

* chore: drop stale `DeprecatedModule` import in `RingTheory/Regular/Depth`

The internal `Mathlib.Tactic.Linter.DeprecatedModule` module was removed on
master in 9037b08; `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 leanprover/lean4#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 a3dbe9e: 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 leanprover/lean4#13613

* chore: bump to nightly-2026-05-03

* remove unneeded simp

* Update lean-toolchain for leanprover/lean4#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 d79879f.

* 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 leanprover-community#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 leanprover/lean4#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 leanprover-community#38341

Lost during the master-merge resolution in 7aa60c9. The upstream
refactor in leanprover-community#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-leanprover-community#36604 shape of
`Reorder`) were deleted by leanprover-community#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>

Author: 11 people

Cache/Requests.lean

@@ -94,7 +94,7 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
       let remoteUrl := parts[1]!.takeWhile (· != ' ') |>.copy -- Remove (fetch) or (push) suffix
 
       -- Check if this remote points to leanprover-community/mathlib4
-      let isMathlibRepo := remoteUrl.containsSubstr "leanprover-community/mathlib4"
+      let isMathlibRepo := remoteUrl.contains "leanprover-community/mathlib4"
 
       if isMathlibRepo then
         if remoteName == "origin" then

Mathlib/Algebra/Colimit/DirectLimit.lean

@@ -613,10 +613,10 @@ lemma map₀_algebraMap (i : ι) (r : R) :
 instance : Algebra R (DirectLimit G f) where
   algebraMap := map₀RingHom (f := f).comp (algebraMap R (∀ i, G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [smul_def, map₀_algebraMap i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_def (i : ι) (r : R) :
@@ -871,7 +871,6 @@ variable [Nonempty ι]
 
 variable (G f) in
 /-- The canonical map from a component to the direct limit. -/
-@[simps]
 def of (i) : G i →ₙₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.NonUnitalRing.of G f i)
@@ -886,7 +885,7 @@ variable (G f) in
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit.
 -/
-@[simps]
+@[simps toFun]
 def lift (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
     DirectLimit G f →ₙₐ[R] P where
   toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm

Mathlib/Algebra/Group/Defs.lean

@@ -15,6 +15,7 @@ public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.OfNat
 public import Mathlib.Data.Nat.Notation
 public import Mathlib.Tactic.Simps.Basic
+public import Mathlib.Tactic.AdaptationNote
 
 /-!
 # Typeclasses for (semi)groups and monoids

Mathlib/Algebra/Group/Nat/Even.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Even
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Data.Nat.Sqrt
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # `IsSquare` and `Even` for natural numbers

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -114,15 +114,17 @@ variable (C) in
 def quotientCompQhIso : HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q :=
   HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)
 
+#adaptation_note /-- Prior to nightly-2026-05-07, the LHS of these statements was guarded with
+`dsimp%`; it now reports `made no progress`, so we write the (already-reduced) form directly. -/
 @[reassoc (attr := simp)]
 lemma quotientCompQhIso_hom_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
+    Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
       (quotientCompQhIso C).hom.app K ≫ Q.map f :=
   (quotientCompQhIso C).hom.naturality f
 
 @[reassoc]
 lemma quotientCompQhIso_inv_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Q.map f ≫ (quotientCompQhIso C).inv.app L =
+    Q.map f ≫ (quotientCompQhIso C).inv.app L =
       (quotientCompQhIso C).inv.app K ≫ Qh.map ((HomotopyCategory.quotient _ _).map f) :=
   (quotientCompQhIso C).inv.naturality f
 

Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean

@@ -56,8 +56,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKInjective] [L.IsKInjective
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]; rfl
 
 end IsKInjective
 

Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean

@@ -57,8 +57,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKProjective] [L.IsKProjecti
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]; rfl
 
 end IsKProjective
 

Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean

@@ -222,7 +222,12 @@ lemma HomologicalComplex.homotopyEquivalences_extendMap_iff
     (e : ComplexShape.Embedding c c') [e.IsRelIff] :
     homotopyEquivalences C c' (extendMap f e) ↔
       homotopyEquivalences C c f := by
-  simp [← HomotopyCategory.inverseImage_quotient_isomorphisms,
+  #adaptation_note /-- Prior to nightly-2026-05-07, `dsimp%` was used directly inline as the last
+  argument to the original `simp`; it now reports `made no progress` so we apply
+  `NatIso.isIso_map_iff` via a `change` + `rw` after the rest of the simp set has done its work. -/
+  simp only [← HomotopyCategory.inverseImage_quotient_isomorphisms,
     MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff,
-    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C),
-    dsimp% NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C)]
+  change _ ↔ IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)
+  rw [NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+  rfl

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -548,8 +548,8 @@ lemma isStableUnderBaseChange (hP : RingHom.IsStableUnderBaseChange Q) :
   · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
       (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
     intro i
-    simp only [Scheme.Pullback.openCoverOfRight_f,
-      limit.lift_π, PullbackCone.mk_π_app, Category.comp_id]
+    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
+      Category.comp_id]
     apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance
   rw [iff_of_isAffine (P := P)] at H ⊢
   exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean

@@ -203,8 +203,8 @@ an affine open cover of `Proj ℬ` consisting of `D(f(s))` for `s ∈ A` positiv
 set_option backward.isDefEq.respectTransparency false in
 theorem map_comp : map (g.comp f) (irrelevant_le_map_comp hf hg) = map g hg ≫ map f hf := by
   refine (mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_
-  simp only [Scheme.AffineOpenCover.openCover_f,
-    mapAffineOpenCover_f, awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
+  simp only [Scheme.AffineOpenCover.openCover_f, mapAffineOpenCover_f,
+    awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
   simp [awayι_comp_map_assoc _ _ _ _ (map_mem f s.2.2), awayι_comp_map _ _ _ _ s.2.2]
 
 set_option backward.isDefEq.respectTransparency false in