Skip to content

[Merged by Bors] - chore(AlgebraicGeometry/Restrict): restore two lemmas that were deleted by toolchain bump#40189

Closed
justus-springer wants to merge 1 commit into
leanprover-community:masterfrom
justus-springer:justus/readd_missing_restrict_lemmas
Closed

[Merged by Bors] - chore(AlgebraicGeometry/Restrict): restore two lemmas that were deleted by toolchain bump#40189
justus-springer wants to merge 1 commit into
leanprover-community:masterfrom
justus-springer:justus/readd_missing_restrict_lemmas

Conversation

@justus-springer

@justus-springer justus-springer commented Jun 3, 2026

Copy link
Copy Markdown
Collaborator

These two lemmas were originally added in #39442. Then the toolchain bump #39980 mysteriously deleted them two days later without replacement.

Open in Gitpod

@github-actions

github-actions Bot commented Jun 3, 2026

Copy link
Copy Markdown

PR summary 5bc6d7d62b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ isoImage_ι_inv_morphismRestrict_homOfLE
+ morphismRestrict_homOfLE_isoImage_ι_hom

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 5bc6d7d62b
Reference commit 51d2df2eb0

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-algebraic-geometry Algebraic geometry label Jun 3, 2026
This was referenced Jun 3, 2026
Closed
Closed
@bryangingechen

bryangingechen commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Thanks!
bors r+

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 3, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@justus-springer
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
6fd9ef1 
…ed by toolchain bump (#40189)

These two lemmas were originally added in #39442. Then the toolchain bump #39980 mysteriously deleted them two days later without replacement.
@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

This PR was included in a batch that was canceled, it will be automatically retried

mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@justus-springer
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
630116a 
…ed by toolchain bump (#40189)

These two lemmas were originally added in #39442. Then the toolchain bump #39980 mysteriously deleted them two days later without replacement.
@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(AlgebraicGeometry/Restrict): restore two lemmas that were deleted by toolchain bump [Merged by Bors] - chore(AlgebraicGeometry/Restrict): restore two lemmas that were deleted by toolchain bump Jun 3, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 3, 2026
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@justus-springer @Bergschaf
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
01599e5 
…ed by toolchain bump (leanprover-community#40189)

These two lemmas were originally added in leanprover-community#39442. Then the toolchain bump leanprover-community#39980 mysteriously deleted them two days later without replacement.
@Garmelon Garmelon mentioned this pull request Jun 5, 2026
Closed
mathlib-bors Bot pushed a commit that referenced this pull request Jun 15, 2026
@Garmelon
chore(CI): fix merge conflict resolution for nightly-testing (#40257)
50b70b9 
Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see #40189 (see [#PR reviews > #39443 &#96;nonempty_preimage_iff&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
felixpernegger pushed a commit to felixpernegger/mathlib4 that referenced this pull request Jun 16, 2026
@Garmelon @felixpernegger
chore(CI): fix merge conflict resolution for nightly-testing (leanpro…
5dceab1 
…ver-community#40257)

Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
gasparattila pushed a commit to gasparattila/mathlib4 that referenced this pull request Jun 16, 2026
@Garmelon @gasparattila
chore(CI): fix merge conflict resolution for nightly-testing (leanpro…
c4a3033 
…ver-community#40257)

Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Jun 18, 2026
@Garmelon @xroblot
chore(CI): fix merge conflict resolution for nightly-testing (leanpro…
3a55039 
…ver-community#40257)

Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@justus-springer @ReemMelamed
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
4790bc7 
…ed by toolchain bump (leanprover-community#40189)

These two lemmas were originally added in leanprover-community#39442. Then the toolchain bump leanprover-community#39980 mysteriously deleted them two days later without replacement.
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@Garmelon @ReemMelamed
chore(CI): fix merge conflict resolution for nightly-testing (leanpro…
4ba2c37 
…ver-community#40257)

Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
bryangingechen pushed a commit to jcommelin/mathlib4 that referenced this pull request Jun 22, 2026
@Garmelon @bryangingechen
chore(CI): fix merge conflict resolution for nightly-testing (leanpro…
201a2b5 
…ver-community#40257)

Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened).

Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`.

Co-authored-by: Joscha <joscha@plugh.de>
mathlib-bors Bot pushed a commit that referenced this pull request Jul 10, 2026
@justus-springer
feat(AlgebraicGeometry/Birational): composition of rational maps (#39445
d45663d 
)

Define composition of partial and rational maps.

- [x] depends on: #39442
- [x] depends on: #39443
- [x] depends on: #39317
- [x] depends on: #40189
michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Jul 11, 2026
@justus-springer @michaellee94
feat(AlgebraicGeometry/Birational): composition of rational maps (lea…
7a70c89 
…nprover-community#39445)

Define composition of partial and rational maps.

- [x] depends on: leanprover-community#39442
- [x] depends on: leanprover-community#39443
- [x] depends on: leanprover-community#39317
- [x] depends on: leanprover-community#40189
mpacholski pushed a commit to mpacholski/mathlib4 that referenced this pull request Jul 16, 2026
@justus-springer @mpacholski
feat(AlgebraicGeometry/Birational): composition of rational maps (lea…
1d511b9 
…nprover-community#39445)

Define composition of partial and rational maps.

- [x] depends on: leanprover-community#39442
- [x] depends on: leanprover-community#39443
- [x] depends on: leanprover-community#39317
- [x] depends on: leanprover-community#40189
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@justus-springer @bryangingechen