New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Port/Data.Finset.Pointwise #1911

Closed

arienmalec wants to merge 24 commits into master from port/Data.Finset.Pointwise

Collaborator

arienmalec commented Jan 28, 2023 •

edited by github-actions bot

Loading

port of data.finset.pointwise

depends on: [Merged by Bors] - fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn #1946

arienmalec added 4 commits

January 28, 2023 11:54


          feat: port Data.Finset.Pointwise

04be081


          Initial file copy from mathport

5d39dbc


          automated fixes

80aaa34

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean


          various simple fixes

b987920

arienmalec added help-wanted mathlib-port labels

arienmalec and others added 10 commits

January 28, 2023 14:49


          another to_additive fix

106b549


          to_additive fixes

bbf72fd


          to_additive and mono fixes

70b103f


          hasVsub -> hasVSub

cacf2d8


          bUnion -> bunion\_1

16ae2a7


          manually name to_additive

f793ed8


          to_additive fixes

5d75003


          Prod -> prod fixes

fb0d1c7


          coe -> CoeTC.coe

ff6bd55


          small fixes

d670b36

Collaborator

LukasMias commented Jan 30, 2023

Opened a Zulip thread on some of the to_additive failures in this file: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20for.20generated.20lemmas

LukasMias added 2 commits

January 30, 2023 12:49


          other small changes

e38b6db


          naming changes

LukasMias mentioned this pull request

[Merged by Bors] - fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn #1946

Closed

LukasMias added 2 commits

January 30, 2023 16:32


          First compiling version

94a3e90


          necessary fix to ListOfFn

9e9d644

semorrison added the blocked-by-other-PR label


          linter fixes

7bee269

bors bot pushed a commit that referenced this pull request


          fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn (#1946)

b109671

A misaligned `to_additive` causes some proofs to fail in #1911. No backport needed, the misalign happened due to a mathlib4 exclusive mistake as I understand.

semorrison removed the blocked-by-other-PR label

Contributor

semorrison commented Jan 30, 2023

This PR/issue depends on:

~~[Merged by Bors] - fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn #1946~~
By Dependent Issues (🤖). Happy coding!


          reordered arguments

4afe43d

Collaborator

LukasMias commented Jan 30, 2023

Finset.vsub apparently used to be a dangerous instance, due to the β in VSub α β being an outParam and hence producing subgoals of the form [Decidable ?α]. The usual tricks failed me, but switching around VSub α β and Decidable α works. Though this feels like something that could break things down the line & might need backporting? Some expert opinion would be appreciated, maybe there's a better fix, too.

arienmalec removed the help-wanted label

arienmalec added the awaiting-review label

jcommelin reviewed

View reviewed changes

Mathlib/Data/Finset/Pointwise.lean Outdated Show resolved Hide resolved

Mathlib/Data/Finset/Pointwise.lean Outdated

+              #align finset.image_add Finset.image_add
+              /-- The singleton operation as a `MulHom`. -/
+              @[to_additive "The singleton operation as an `add_hom`."]

Member

jcommelin Jan 31, 2023

Suggested change

      
            @[to_additive "The singleton operation as an `add_hom`."]
          
            @[to_additive "The singleton operation as an `AddHom`."]

Mathlib/Data/Finset/Pointwise.lean Outdated Show resolved Hide resolved

Mathlib/Data/Finset/Pointwise.lean Outdated

+              scoped[Pointwise] attribute [instance] Finset.nsmul Finset.npow Finset.zsmul Finset.zpow
+              /-- `Finset α` is a `Semigroup` under pointwise operations if `α` is. -/
+              @[to_additive "`Finset α` is an `add_semigroup` under pointwise operations if `α` is. "]

Member

jcommelin Jan 31, 2023

Suggested change

      
            @[to_additive "`Finset α` is an `add_semigroup` under pointwise operations if `α` is. "]
          
            @[to_additive "`Finset α` is an `AddSemigroup` under pointwise operations if `α` is. "]

Mathlib/Data/Finset/Pointwise.lean Outdated

+              #align finset.add_semigroup Finset.addSemigroup
+              /-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is. -/
+              @[to_additive "`Finset α` is an `add_comm_semigroup` under pointwise operations if `α` is. "]

Member

jcommelin Jan 31, 2023

Suggested change

      
            @[to_additive "`Finset α` is an `add_comm_semigroup` under pointwise operations if `α` is. "]
          
            @[to_additive "`Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. "]

Mathlib/Data/Finset/Pointwise.lean Outdated

+              variable [MulOneClass α]
+              /-- `Finset α` is a `MulOneClass` under pointwise operations if `α` is. -/
+              @[to_additive "`Finset α` is an `add_zero_class` under pointwise operations if `α` is."]

Member

jcommelin Jan 31, 2023

Suggested change

      
            @[to_additive "`Finset α` is an `add_zero_class` under pointwise operations if `α` is."]
          
            @[to_additive "`Finset α` is an `AddZeroClass` under pointwise operations if `α` is."]

Mathlib/Data/Finset/Pointwise.lean Outdated

Comment on lines 770 to 771

		/-- The singleton operation as a `monoid_hom`. -/
		@[to_additive "The singleton operation as an `add_monoid_hom`."]

Member

jcommelin Jan 31, 2023

Suggested change

      
            /-- The singleton operation as a `monoid_hom`. -/
          
            @[to_additive "The singleton operation as an `add_monoid_hom`."]
          
            /-- The singleton operation as a `MonoidHom`. -/
          
            @[to_additive "The singleton operation as an `AddMonoidHom`."]

Mathlib/Data/Finset/Pointwise.lean Outdated

Comment on lines 789 to 790

		/-- The coercion from `Finset` to `set` as a `monoid_hom`. -/
		@[to_additive "The coercion from `Finset` to `set` as an `add_monoid_hom`."]

Member

jcommelin Jan 31, 2023

Suggested change

      
            /-- The coercion from `Finset` to `set` as a `monoid_hom`. -/
          
            @[to_additive "The coercion from `Finset` to `set` as an `add_monoid_hom`."]
          
            /-- The coercion from `Finset` to `Set` as a `MonoidHom`. -/
          
            @[to_additive "The coercion from `Finset` to `Set` as an `AddMonoidHom`."]

Mathlib/Data/Finset/Pointwise.lean Outdated

Comment on lines 810 to 811

		/-- Lift a `monoid_hom` to `Finset` via `image`. -/
		@[to_additive "Lift an `add_monoid_hom` to `Finset` via `image`", simps]

Member

jcommelin Jan 31, 2023

Suggested change

      
            /-- Lift a `monoid_hom` to `Finset` via `image`. -/
          
            @[to_additive "Lift an `add_monoid_hom` to `Finset` via `image`", simps]
          
            /-- Lift a `MonoidHom` to `Finset` via `image`. -/
          
            @[to_additive "Lift an `AddMonoidHom` to `Finset` via `image`", simps]

Mathlib/Data/Finset/Pointwise.lean Outdated

+              #align finset.coe_pow Finset.coe_pow
+              /-- `Finset α` is a `Monoid` under pointwise operations if `α` is. -/
+              @[to_additive "`Finset α` is an `add_monoid` under pointwise operations if `α` is. "]

Member

jcommelin Jan 31, 2023

Suggested change

      
            @[to_additive "`Finset α` is an `add_monoid` under pointwise operations if `α` is. "]
          
            @[to_additive "`Finset α` is an `AddMonoid` under pointwise operations if `α` is. "]

jcommelin added awaiting-author and removed awaiting-review labels

Collaborator Author

arienmalec commented Jan 31, 2023

I'll just run fix-comments.sh here -- may have forgotten this step.


          auto: naming

41dc5f6

arienmalec added awaiting-review and removed awaiting-author labels

Member

jcommelin commented Jan 31, 2023

@arienmalec unfortunately fix-comments.py doesn't know how to fix the docstrings passed to to_additive. So please fix those manually.


          fix docu in to_additive

79c4cde

Collaborator Author

arienmalec commented Jan 31, 2023

@arienmalec unfortunately fix-comments.py doesn't know how to fix the docstrings passed to to_additive. So please fix those manually.

Ah, I see it now. Done.

Member

jcommelin commented Jan 31, 2023

Thanks 🎉

bors merge

github-actions bot added ready-to-merge and removed awaiting-review labels

bors bot pushed a commit that referenced this pull request


          feat: Port/Data.Finset.Pointwise (#1911)

344f657

port of data.finset.pointwise



Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>

bors bot commented Jan 31, 2023

Build failed:

Build

Member

jcommelin commented Feb 1, 2023

bors r+

bors bot pushed a commit that referenced this pull request


          feat: Port/Data.Finset.Pointwise (#1911)

54eb5bf

port of data.finset.pointwise



Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>

bors bot commented Feb 1, 2023

Build failed:

Build

jcommelin added 2 commits

February 1, 2023 10:13


          Merge branch 'master' into port/Data.Finset.Pointwise

64d83f1


          BigOperators exists

dfa8d8c

Member

jcommelin commented Feb 1, 2023

bors r+

bors bot pushed a commit that referenced this pull request


          feat: Port/Data.Finset.Pointwise (#1911)

e50f014

port of data.finset.pointwise



Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

bors bot commented Feb 1, 2023

Pull request successfully merged into master.

Build succeeded:

bors bot changed the title ~~feat: Port/Data.Finset.Pointwise~~ [Merged by Bors] - feat: Port/Data.Finset.Pointwise

bors bot closed this

bors bot deleted the port/Data.Finset.Pointwise branch

February 1, 2023 10:25

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment