Skip to content

[Merged by Bors] - feat: insert and erase lemmas#3569

Closed
YaelDillies wants to merge 2 commits intomasterfrom
disjoint_erase_comm
Closed

[Merged by Bors] - feat: insert and erase lemmas#3569
YaelDillies wants to merge 2 commits intomasterfrom
disjoint_erase_comm

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Apr 21, 2023

@YaelDillies
feat: insert and erase lemmas
32ffca2 
* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
@YaelDillies YaelDillies added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Apr 21, 2023
@Vierkantor Vierkantor self-assigned this Apr 21, 2023
eric-wieser
eric-wieser approved these changes Apr 23, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I've checked the whole diff and it looks like you got everything. Some of the comments still refer to the mathlib3 names though.

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 23, 2023
@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 24, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Apr 24, 2023

bors merge

@Vierkantor, as this is only a forward-port I assume the assignment was "I plan to get back to this" not "please wait for me to review this and don't merge without me"

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 24, 2023
bors bot pushed a commit that referenced this pull request Apr 24, 2023
@YaelDillies
feat: insert and erase lemmas (#3569)
0437079 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Apr 24, 2023

You are absolutely right about assigned meaning "I will look at this when I have time", in fact I had selected the reply box and was writing bors r+ myself when your comment appears.

@bors
Copy link
Copy Markdown

bors bot commented Apr 24, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: insert and erase lemmas [Merged by Bors] - feat: insert and erase lemmas Apr 24, 2023
@bors bors bot closed this Apr 24, 2023
@bors bors bot deleted the disjoint_erase_comm branch April 24, 2023 11:34
kim-em pushed a commit that referenced this pull request May 10, 2023
@YaelDillies
feat: insert and erase lemmas (#3569)
fe76a1b 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
@YaelDillies @hrmacbeth
feat: insert and erase lemmas (#3569)
4cf99fa 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
@YaelDillies @hrmacbeth
feat: insert and erase lemmas (#3569)
fc7620f 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

@Vierkantor Vierkantor

Labels

mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @eric-wieser @Vierkantor