[Merged by Bors] - feat: last adaptations for v4.31.0#229
Closed
kim-em wants to merge 18 commits into
Closed
Conversation
…sing` lean4#13636 made `simpa using h` close at reducible transparency. The simp trace here is identical to master (verified by tracing both): the term normalizes to `p ∣ Polynomial.map (↑f.toRingEquiv.symm) q` while the goal keeps `↑f.symm`. Master closed that `f.toRingEquiv.symm` vs `f.symm` gap at semireducible transparency; reducible cannot. Use `simpa using!` to restore semireducible closing, and keep `-RingEquiv.symm_mk` so the term stays `↑f.toRingEquiv.symm` rather than expanding to a structure literal (which even semireducible could not bridge — that was why plain `using!` failed earlier). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Another module duplicated by the May 28 master merge: master had reduced it to a `deprecated_module` shim re-exporting `ModularForms.LevelOne.DimensionFormula`, but the merge kept nightly-testing's old full module, causing duplicate declarations. Take master's shim, dropping the `Mathlib.Tactic.Linter.DeprecatedModule` import (removed on nightly-testing) to match the other shims. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…/Dominant` On the current Lean nightly `dsimp only [restrict_domain, restrict_hom]` reports "made no progress" (the `@[simps]`-generated equation lemmas no longer fire under `dsimp`'s reduced transparency), so the subsequent `rw [IsDominant.comp_iff]` / `rw [e₁, h, ← e₂]` could not find their patterns. Sidestep the dependent-type rewrite entirely: * `isDominant_restrict_hom`: close by `exact (inferInstance : IsDominant (X.homOfLE hU' ≫ f.hom))` — the goal is defeq to this (instance synthesis + `exact` still use semireducible), and the `IsDominant (f ≫ g)` instance fires from the two dominance facts. * `isDominant_hom_iff_of_equiv`: after rewriting both sides to the restricted form, close with `iff_of_eq (congrArg (IsDominant ·) h)` rather than rewriting under the dependent `IsDominant` type. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…trib.useBackward` Restore the original `dsimp only [restrict_domain, restrict_hom]` proofs (reverting the earlier rewrite in d79d34f) by wrapping the two lemmas in `set_option backward.defeqAttrib.useBackward true in`, which lets `dsimp` fire the `@[simps]` equation lemmas again on the current Lean nightly. Also update the expected output in `MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta` to the new diagnostic wording. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The `deprecated_module` / `#show_deprecated_modules` machinery is now provided by Lean core rather than the Mathlib linter, so the base module is `MathlibTest.Linter.DeprecatedModule.ImportBase` (not the old `MathlibTest.DeprecatedModule` / `…DeprecatedModuleNew`): * `ImportAsAll`/`ImportAsMeta`/`ImportAsPublic`/`Basic`: update the stale module names in imports and expected `#show_deprecated_modules` output. * `ImportAsPlain`: it still used the legacy "capture the import warning via a trailing `#guard_msgs`" idiom, which can't work now that core emits the warning at import time. Convert it to the `module --deprecated_module: ignore` + `#show_deprecated_modules` form used by its siblings. * Delete the orphaned `MathlibTest/DeprecatedModuleTest.lean` (removed on master; it imported the now-nonexistent `MathlibTest.DeprecatedModule`). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* `AlternatingFaceMapComplex`: `not_lt_zero'` deprecated, use `not_lt_zero`. * `Finsupp/Single`: `Finsupp.support_single_ne_zero` deprecated, use the unprimed `Finsupp.support_single`. * `Probability/Independence/Basic`: drop the `beta_reduce` step that no longer fires. * `MeasureSpace.eq_zero_of_isEmpty` and `VectorMeasure.eq_zero_of_isEmpty`: these are `@[nontriviality]` (a scoped simp set), so the new `warning.simp.varHead` lint about `μ` being a variable LHS is exactly the "acceptable for scoped simp lemmas" case — suppress per-declaration. * `Over.mapId` / `Under.mapId`: the outer `variable [P.IsStableUnderComposition]` is redundant with the per-decl `[P.IsMultiplicative]`, but is needed by the surrounding `Over.map` / `Under.map` declarations. Suppress the `linter.overlappingInstances` lint on the two `mapId` definitions. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replace two `grind` calls in `sum_neg_one_pow_finrank_eq_zero_of_exact` that no longer succeed on v4.31.0-rc1 with explicit rank-nullity / exactness proofs, recording the prior tactics in `#adaptation_note`s. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Author
|
bors p=100 |
Author
|
bors merge |
mathlib-bors Bot
pushed a commit
that referenced
this pull request
May 28, 2026
Sorry, automated processes fell apart at the last moment.
|
Canceled. Address comments or fix if necessary, and then someone with permission can run |
Author
|
bors merge |
mathlib-bors Bot
pushed a commit
that referenced
this pull request
May 28, 2026
Sorry, automated processes fell apart at the last moment.
|
Pull request successfully merged into bump/v4.31.0. Build succeeded:
|
mathlib-bors
Bot
changed the title
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
1 participant
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.
Sorry, automated processes fell apart at the last moment.