chore: kill some erws#38415
Open
yuanyi-350 wants to merge 15 commits intoleanprover-community:masterfrom
Open
Conversation
PR summary 977f84bd6eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for Decrease in tech debt: (relative, absolute) = (13.00, 0.02)
Current commit 6e91aae471 This script lives in the
|
This was referenced Apr 23, 2026
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 23, 2026
- simplifies the proof passed to `Submodule.Quotient.equiv` in `tensorQuotientEquiv` to a single `simp [range_map_eq_span_tmul]` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 24, 2026
… an `erw` (#38418) - rewrites `withDensityᵥ_rnDeriv_eq` to replace `erw [VectorMeasure.sub_apply]` with a plain `rw` - adds `JordanDecomposition.toSignedMeasure` to the same rewrite chain so the proof closes without `erw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
This was referenced Apr 25, 2026
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
…rw (#38503) - rewrites `exists_upperSemicontinuous_le_lintegral_le` to replace `erw [ENNReal.biSup_add]` with a plain `rw` - uses `ENNReal.biSup_add'` so the rewrite closes without `erw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
](https://gitpod.io/from-referrer/){kind=link}
task_id: erw-elim-v3-0127 target_path: Mathlib/CategoryTheory/Localization/Construction.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0127
task_id: erw-elim-v3-0117 target_path: Mathlib/CategoryTheory/Limits/Shapes/Images.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0117
task_id: erw-elim-v3-0280 target_path: Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0280
task_id: erw-elim-v3-0202 target_path: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0202
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
- rewrites `BlockTriangular.det` to replace a `simp only` plus `erw` pair with a single `rw` - uses `Matrix.det_reindex_self he.symm` directly in the rewrite chain Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
- rewrites `lintegral_indicator_const_comp` to replace `erw [lintegral_comp ...]` with a plain `rw` - uses `lintegral_map` at the start of the rewrite chain before `lintegral_indicator_const` and `Measure.map_apply` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
This was referenced Apr 25, 2026
Closed
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
- shortens the `uniq` proof in `unitIso` to `simp [functor, inverse, fac]`, removing the `dsimp` plus `erw [fac]` sequence Extracted from #38415 [](https://gitpod.io/from-referrer/)
This was referenced Apr 25, 2026
Closed
Closed
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
…38521) - rewrites the sheafification whiskering lemmas with `simp only [sheafify, ...]`, removing the transparency workaround - rewrites `whiskerRight_toSheafify_sheafifyCompIso_hom` with `simp only [toSheafify, sheafify, ...]` instead of `erw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
- adds `← comp_evaluation G k` to the simplification step, so `limitObjIsoLimitCompEvaluation_hom_π_assoc` no longer needs `erw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
…38519) - rewrites the sliced `dite` goals with `simp only`, replacing both `erw` steps in `isLimit` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 25, 2026
- rewrites `Finset.sum_sigma` via `← Finset.univ_sigma_univ`, so the biproduct proof uses a plain `rw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 26, 2026
#38506) - rewrites the `TopCat.comp_app` step in `colimitPresheafObjIsoComponentwiseLimit` with `simp only [colimitCocone, colimit, ← TopCat.comp_app]` - folds `colimitCocone_ι_app_c`, `limitObjIsoLimitCompEvaluation_inv_π_app_assoc`, and `limMap_π_assoc` into a single `rw` chain in `colimitPresheafObjIsoComponentwiseLimit_inv_ι_app` Extracted from #38415 [](https://gitpod.io/from-referrer/)
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 26, 2026
- rewrites `kernelSubobject_arrow_comp_assoc` after inserting `← SimplicialObject.δ_def`, replacing the `erw` step Extracted from #38415 [](https://gitpod.io/from-referrer/)
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
2 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.
erw#38418erw#38417