[Merged by Bors] - chore: remove superfluous parentheses in calls to `ext` #5258

semorrison · 2023-06-19T11:22:14Z

depends on: [Merged by Bors] - chore: bump Std4 #5219

semorrison · 2023-06-19T15:02:22Z

This PR/issue depends on:

~~[Merged by Bors] - chore: bump Std4 #5219~~
By Dependent Issues (🤖). Happy coding!

Introduced while making it multiplicative in leanprover-community/mathlib#13359

…es` can't be used for global variables (#5207) ```lean variable (d : ℕ) example (h : d ≤ 0) : d = 0 := by interval_cases d rfl ``` This fails. This PR fixes this bug.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>

…t}): restore a more faithful mathported proof, using the "newer" `push_neg` (#5132) These are just three cases where a mathported proof had to be changed, due to unwanted behaviour with `push_neg/contradiction`. Since #5082 is supposed to fix some issues with these tactics, some of these workarounds can be removed. Note: this was not in any way systematic, I simply `grep`ped the line after a `contra`, then `grep`ped for a `not` and then selected 3 likely candidates. There are potentially more situations like these.

My current method for accessing the mathlib4 docs is: 1. google for "mathlib docs" 2. insert a "4" into the url The [mathlib3 readme](https://github.com/leanprover-community/mathlib/blob/893964fc28cefbcffc7cb784ed00a2895b4e65cf/README.md) has a prominent link to the mathlib3 docs. We should have something similar for mathlib4. Hopefully this will help google find the mathlib4 docs, too.

Adds tail recursive definition of maximal `k` such that `p^k | n` for `p, n : Nat` and `csimp` theorem relating it to `Nat.padicValNat`

…5208)

Co-authored-by: Moritz Firsching <firsching@google.com>

I forgot that we already had the fact that sheaves valued in an abelian category form an abelian category, so this PR removes some of the duplication. Note: The existing file that had this is in `Topology/Category/Sheaves`, and not in `CategoryTheory/Sites`. This should be moved at some point.

Add the instance ```lean instance instDecidableLE (α : Type u) (β : Type v) [LE α] [LE β] (x y : α × β) [Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] : Decidable (x ≤ y) ```

Some such lemmas are already labelled `@[simp]`, and this PR adds `@[simp]` to the remaining ones. It's useful for some automation I'm writing to have these all in `simp`. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

While experimenting with making `ext` more powerful a proof was failing here. Rather than fix it, it seemed easier to just remove it. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

@fpvandoorn

Heavily based on the code from the sphere eversion project. Co-authored-by: @fpvandoorn

sgouezel · 2023-06-20T11:22:00Z

bors r+
Thanks!

fpvandoorn · 2023-06-20T12:35:14Z

the git history got messed up

Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp> Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors · 2023-06-20T13:55:21Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp> Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Scott Morrison and others added 9 commits June 18, 2023 17:20

chore: bump Std4

59c86e0

bump again

a7482f1

fix

e818907

fixes

e3e4c44

fixes

19c8670

fix

b098b2e

cleanup syntax around ext

c84ebdb

cleanup syntax around ext

1f7b3f4

finished

2fa8acd

semorrison added awaiting-review The author would like community review of the PR awaiting-CI blocked-by-other-PR This PR depends on another PR which is still in the queue. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Jun 19, 2023

Parcly-Taxel and others added 16 commits June 20, 2023 06:50

feat: port Probability.Process.Adapted (#5205)

f196651

chore: fix a typo (#5202)

9c4235a

Introduced while making it multiplicative in leanprover-community/mathlib#13359

fix(Mathlib.Tactic.IntervalCases, test.interval_cases): `interval_cas…

5363012

…es` can't be used for global variables (#5207) ```lean variable (d : ℕ) example (h : d ≤ 0) : d = 0 := by interval_cases d rfl ``` This fails. This PR fixes this bug.

feat: port Data.DList from Lean core (#1498)

3aa6e2f

Co-authored-by: Komyyy <pol_tta@outlook.jp>

feat: port Control.Monad.Cont (#4981)

0bab8e5

feat: port Archive.Examples.PropEncodable (#5098)

33e416c

Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>

feat: add Nat.maxPowDiv (#5158)

562833e

Adds tail recursive definition of maximal `k` such that `p^k | n` for `p, n : Nat` and `csimp` theorem relating it to `Nat.padicValNat`

feat: port Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges (#…

3fb3cae

…5208)

feat: port Archive.Imo.Imo1962Q1 (#5210)

69a9d5e

feat: port Probability.Process.Stopping (#5213)

fd7198b

feat: port Archive.Imo.Imo2019Q1 (#5211)

0239099

feat: port NumberTheory.LegendreSymbol.Basic (#5197)

9c15670

Co-authored-by: Moritz Firsching <firsching@google.com>

chore: add Prod.instDecidableLE (#5083)

de27d50

Add the instance ```lean instance instDecidableLE (α : Type u) (β : Type v) [LE α] [LE β] (x y : α × β) [Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] : Decidable (x ≤ y) ```

semorrison and others added 10 commits June 20, 2023 06:50

chore: better error message for non-cached files (#5129)

22dcd4c

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

chore: cleanup CategoryTheory.Pi.Basic (#5180)

a132cce

While experimenting with making `ext` more powerful a proof was failing here. Rather than fix it, it seemed easier to just remove it. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

chore: add @[ext] lemmas for NatTrans synonyms (#5228)

fcf9056

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

chore: reviewing porting notes about rw/simp/simp_rw (#5244)

1bf5c8b

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

feat: port NumberTheory.KummerDedekind (#5249)

039debd

feat: port CategoryTheory.Monoidal.Internal.Types (#5253)

148ea08

chore: use in in set_option maxHeartbeats (#5261)

0487f83

feat: functions eventually constant along filters (#5248)

4bc657c

Heavily based on the code from the sphere eversion project. Co-authored-by: @fpvandoorn

fix

62ae132

semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 20, 2023

merge

35cec0f

semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 20, 2023

semorrison added 2 commits June 20, 2023 16:02

fix

3a94ef6

typo

3e546a1

github-actions bot removed the awaiting-CI label Jun 20, 2023

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jun 20, 2023

bors bot changed the title ~~chore: remove superfluous parentheses in calls to ext~~ [Merged by Bors] - chore: remove superfluous parentheses in calls to ext Jun 20, 2023

bors bot closed this Jun 20, 2023

bors bot deleted the ext_followup branch June 20, 2023 13:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: remove superfluous parentheses in calls to `ext` #5258

[Merged by Bors] - chore: remove superfluous parentheses in calls to `ext` #5258

semorrison commented Jun 19, 2023 •

edited by github-actions bot

semorrison commented Jun 19, 2023

sgouezel commented Jun 20, 2023

fpvandoorn commented Jun 20, 2023

bors bot commented Jun 20, 2023

[Merged by Bors] - chore: remove superfluous parentheses in calls to ext #5258

[Merged by Bors] - chore: remove superfluous parentheses in calls to ext #5258

Conversation

semorrison commented Jun 19, 2023 • edited by github-actions bot

semorrison commented Jun 19, 2023

sgouezel commented Jun 20, 2023

fpvandoorn commented Jun 20, 2023

bors bot commented Jun 20, 2023

[Merged by Bors] - chore: remove superfluous parentheses in calls to `ext` #5258

[Merged by Bors] - chore: remove superfluous parentheses in calls to `ext` #5258

semorrison commented Jun 19, 2023 •

edited by github-actions bot