[Merged by Bors] - feat: port Algebra.Group.WithOne.Defs by kbuzzard · Pull Request #841 · leanprover-community/mathlib4

kbuzzard · 2022-12-03T18:34:26Z

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

kbuzzard · 2022-12-03T21:53:42Z

Things of note here:

Like WithBot, we add coe : α → WithOne α and tag it @[coe] for compatibility with Lean 4's coercion mechanism
Neither @[coe, to_additive] nor @[to_additive, coe] seems to tag the additivised definition with coe; same for @[norm_cast, to_additive] (which used to work in Lean 3). I've had to manually tag some to-additivised declarations as a consequence.
I had to comment out a CanLift instance, and also rewrite a proof, because there is still no lift tactic.
There are some shows which might not be needed; I asked at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/_proof_1/near/313734606 because I don't know how to test this.
WithZero.zero_mul with WithZero.mul_zero used to be tagged @[simp] but a linter told me that simp only [zero_mul] proves it, so I removed the tags. This makes sense: WithZero alpha is an instance of MulZeroClass. I'm slightly surprised that the linter in mathlib3 doesn't flag this.

kim-em · 2022-12-04T01:44:26Z

Mathlib/Algebra/Group/WithOne/Defs.lean

+-- example [Semigroup α] :
+--     @Monoid.toMulOneClass _ (@instMonoidWithOne α _) = @instMulOneClassWithOne α _ :=
+--   rfl
+


I'd have to make a corresponding PR to mathlib3 then, right? https://github.com/leanprover-community/mathlib/blob/c982179ec21091d3e102d8a5d9f5fe06c8fafb73/src/algebra/group/with_one/defs.lean#L127-L128

kim-em · 2022-12-04T01:45:54Z

If you can remember it, could you add a porting note to the proof you had to rewrite for lack of simp? It would be good, even if only as a test, to restore this when lift arrives, hopefully soon.

kim-em · 2022-12-04T01:46:12Z

bors d+

Please update the wiki page when you merge.

bors · 2022-12-04T01:46:13Z

✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Ruben-VandeVelde · 2022-12-04T12:55:33Z

Mathlib/Algebra/Group/WithOne/Defs.lean

+-- porting note: in Lean 4 this is a syntactic tautology
+-- @[to_additive]
+-- theorem some_eq_coe {a : α} : (some a : WithOne α) = ↑a :=
+--   rfl
+-- #align with_one.some_eq_coe WithOne.some_eq_coe


Suggested change

-- porting note: in Lean 4 this is a syntactic tautology

-- @[to_additive]

-- theorem some_eq_coe {a : α} : (some a : WithOne α) = ↑a :=

-- rfl

-- #align with_one.some_eq_coe WithOne.some_eq_coe

#noalign with_one.some_eq_coe

And with_zero.some_eq_coe too!

Mathlib/Algebra/Group/WithOne/Defs.lean

kbuzzard · 2022-12-04T23:59:44Z

OK I just realised that every @[to_additive] followed by an #align needs to have a second #align added for the additivised definition. I've just added these but don't want to hit merge until the branch compiles and unfortunately it's time for bed.

kbuzzard · 2022-12-05T00:12:52Z

Oh nice, it doesn't take hours to compile like mathlib3 :-)

kbuzzard · 2022-12-05T00:13:09Z

bors r+

kim-em · 2022-12-06T01:48:59Z

bors merge

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

bors · 2022-12-06T02:09:16Z

Build failed (retrying...):

Build

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

bors · 2022-12-06T02:38:55Z

Build failed (retrying...):

Build

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

bors · 2022-12-06T03:00:14Z

Build failed:

Build

…ra-group-with-one-defs

Mathlib/Algebra/Group/WithOne/Defs.lean

kim-em · 2022-12-06T03:44:03Z

bors merge

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>

bors · 2022-12-06T04:00:49Z

Pull request successfully merged into master.

Build succeeded:

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.divisibility.basic`: leanprover-community/mathlib4#833 * `algebra.group.with_one.defs`: leanprover-community/mathlib4#841 * `algebra.hom.commute`: leanprover-community/mathlib4#831 * `algebra.hom.group`: leanprover-community/mathlib4#659 * `algebra.hom.units`: leanprover-community/mathlib4#745 * `algebra.ring.basic`: leanprover-community/mathlib4#830 * `category_theory.natural_isomorphism`: leanprover-community/mathlib4#820 * `combinatorics.quiver.connected_component`: leanprover-community/mathlib4#836 * `combinatorics.quiver.subquiver`: leanprover-community/mathlib4#828 Co-authored-by: Johan Commelin <johan@commelin.net>

mathlib3 SHA: dad7ecf9a1feae63e6e49f07619b7087403fb8d4 Ports Algebra.Order.Monoid.WithZero.[Defs, Basic]. - [x] depends on #841 - [x] depends on leanprover-community/mathlib3#17820 I'm planning to wait until leanprover-community/mathlib3#17820 is approved before doing a final refactor to move lemmas where they're needed. Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>

feat: port Algebra.Group/WithOne.Defs

040367b

kbuzzard added the WIP Work in progress label Dec 3, 2022

kbuzzard added 2 commits December 3, 2022 21:04

finished

7d73ae0

tidying up

0e3a970

kbuzzard mentioned this pull request Dec 3, 2022

feat: port Algebra.Group.With_One #827

Closed

2 tasks

kbuzzard added 3 commits December 3, 2022 21:24

add file name to Mathlib.lean

4981718

adding more porting notes

50b5859

clarified porting notes

8ab0ca6

kbuzzard added awaiting-review mathlib-port This is a port of a theory file from mathlib. and removed WIP Work in progress labels Dec 3, 2022

kbuzzard changed the title ~~feat: port Algebra.Group/WithOne.Defs~~ feat: port Algebra.Group.WithOne.Defs Dec 3, 2022

kim-em reviewed Dec 4, 2022

View reviewed changes

github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Dec 4, 2022

Ruben-VandeVelde reviewed Dec 4, 2022

View reviewed changes

zeramorphic mentioned this pull request Dec 4, 2022

[Merged by Bors] - feat: port Algebra.Order.Monoid.WithZero #851

Closed

2 tasks

Ruben-VandeVelde mentioned this pull request Dec 4, 2022

feat: port algebra.order.monoid.with_zero.defs #852

Closed

1 task

final touches

882d521

github-actions bot mentioned this pull request Dec 5, 2022

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib3#17806

Closed

ChrisHughes24 added the ready-to-merge This PR has been sent to bors. label Dec 5, 2022

github-actions bot mentioned this pull request Dec 6, 2022

chore(*): add mathlib4 synchronization comments #1 alreadydone/mathlib#2

Open

bors bot pushed a commit that referenced this pull request Dec 6, 2022

feat: port Algebra.Group.WithOne.Defs (#841)

5d30318

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

bors bot pushed a commit that referenced this pull request Dec 6, 2022

feat: port Algebra.Group.WithOne.Defs (#841)

3abe590

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

bors bot pushed a commit that referenced this pull request Dec 6, 2022

feat: port Algebra.Group.WithOne.Defs (#841)

7aa1fc1

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

Merge remote-tracking branch 'origin/master' into kbuzzard-port-algeb…

67ee04d

…ra-group-with-one-defs

kim-em reviewed Dec 6, 2022

View reviewed changes

Mathlib/Algebra/Group/WithOne/Defs.lean Outdated Show resolved Hide resolved

kim-em and others added 2 commits December 6, 2022 14:21

Update Mathlib/Algebra/Group/WithOne/Defs.lean

88560a4

fix

f2cb7df

bors bot pushed a commit that referenced this pull request Dec 6, 2022

feat: port Algebra.Group.WithOne.Defs (#841)

8a3baed

mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>

bors bot changed the title ~~feat: port Algebra.Group.WithOne.Defs~~ [Merged by Bors] - feat: port Algebra.Group.WithOne.Defs Dec 6, 2022

bors bot closed this Dec 6, 2022

bors bot deleted the kbuzzard-port-algebra-group-with-one-defs branch December 6, 2022 04:00

Conversation

kbuzzard commented Dec 3, 2022

Uh oh!

kbuzzard commented Dec 3, 2022

Uh oh!

kim-em Dec 4, 2022

Choose a reason for hiding this comment

Uh oh!

kbuzzard Dec 4, 2022

Choose a reason for hiding this comment

Uh oh!

kim-em commented Dec 4, 2022

Uh oh!

kim-em commented Dec 4, 2022

Uh oh!

bors bot commented Dec 4, 2022

Uh oh!

Ruben-VandeVelde Dec 4, 2022

Choose a reason for hiding this comment

Uh oh!

kbuzzard Dec 4, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kbuzzard commented Dec 4, 2022

Uh oh!

kbuzzard commented Dec 5, 2022

Uh oh!

kbuzzard commented Dec 5, 2022

Uh oh!

kim-em commented Dec 6, 2022

Uh oh!

bors bot commented Dec 6, 2022

Uh oh!

bors bot commented Dec 6, 2022

Uh oh!

bors bot commented Dec 6, 2022

Uh oh!

Uh oh!

kim-em commented Dec 6, 2022

Uh oh!

bors bot commented Dec 6, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants