Merge branch 'master' into spin_group

.docker/debian/lean/Dockerfile

@@ -26,7 +26,10 @@ RUN python3 -m pip install --user mathlibtools
 # now install `pyinstaller`, and run it on the installed copy of `leanproject`
 RUN python3 -m pip install --user pyinstaller
 WORKDIR /home/lean/.local/bin
-RUN pyinstaller --onefile --noconfirm leanproject
+# We need the `--hidden-import` flag here due to PyInstaller not knowing the dependencies
+# of PyNaCl (https://github.com/pyinstaller/pyinstaller/issues/3525), which is itself a transitive
+# dependency of mathlibtools via PyGithub.
+RUN pyinstaller --onefile --noconfirm --hidden-import _cffi_backend leanproject
 # this has created `/home/lean/.local/bin/dist/leanproject`,
 # which we'll now copy to a fresh container
 

.github/CODEOWNERS

@@ -0,0 +1,19 @@
+# By default, the mathlib maintainers own everything in the repo.
+# Later matches will take precedence over this match.
+
+# Disabled until we have better coverage by other patterns. Reenable in the future.
+# *        @leanprover-community/mathlib-maintainers
+
+src/category_theory/    @leanprover-community/mathlib-CT
+
+src/measure_theory/     @leanprover-community/mathlib-meas
+
+src/algebraic_topology/ @leanprover-community/mathlib-CT # for now the category theory team can take care of this
+
+src/algebraic_geometry/ @leanprover-community/mathlib-AG
+
+src/combinatorics/      @leanprover-community/mathlib-CO
+
+src/probability/        @leanprover-community/mathlib-PR
+
+src/tactic/             @leanprover-community/mathlib-meta

.github/workflows/bors.yml

@@ -81,8 +81,8 @@ jobs:
           set -o pipefail
           leanpkg configure
           echo "::set-output name=started::true"
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
+          lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          lean --json -T400000 --make src | python3 scripts/detect_errors.py
 
       - name: push release to azure
         if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
@@ -197,7 +197,7 @@ jobs:
       - name: tests
         run: |
           set -o pipefail
-          lean --json -T150000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
         if: ${{ ! 1 }}

.github/workflows/build.yml

@@ -89,8 +89,8 @@ jobs:
           set -o pipefail
           leanpkg configure
           echo "::set-output name=started::true"
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
+          lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          lean --json -T400000 --make src | python3 scripts/detect_errors.py
 
       - name: push release to azure
         if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
@@ -205,7 +205,7 @@ jobs:
       - name: tests
         run: |
           set -o pipefail
-          lean --json -T150000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
         if: ${{ ! 1 }}

.github/workflows/build.yml.in

@@ -67,8 +67,8 @@ jobs:
           set -o pipefail
           leanpkg configure
           echo "::set-output name=started::true"
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
+          lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          lean --json -T400000 --make src | python3 scripts/detect_errors.py
 
       - name: push release to azure
         if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
@@ -183,7 +183,7 @@ jobs:
       - name: tests
         run: |
           set -o pipefail
-          lean --json -T150000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
         if: ${{ ! IS_SELF_HOSTED }}

.github/workflows/build_fork.yml

@@ -87,8 +87,8 @@ jobs:
           set -o pipefail
           leanpkg configure
           echo "::set-output name=started::true"
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
-          lean --json -T150000 --make src | python3 scripts/detect_errors.py
+          lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          lean --json -T400000 --make src | python3 scripts/detect_errors.py
 
       - name: push release to azure
         if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
@@ -203,7 +203,7 @@ jobs:
       - name: tests
         run: |
           set -o pipefail
-          lean --json -T150000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
         if: ${{ ! 0 }}

.github/workflows/maintainer_merge_comment.yml

@@ -0,0 +1,42 @@
+name: Maintainer merge (comment)
+
+on:
+  issue_comment:
+    types: [created, edited]
+
+jobs:
+  ping_zulip:
+    name: Ping maintainers on Zulip
+    if: (github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\r\nmaintainer merge'))
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check whether user is part of mathlib-reviewers team
+        uses: TheModdingInquisition/[email protected]
+        with:
+          organization: 'leanprover-community'
+          team: 'mathlib-reviewers' # required. The team to check for
+          token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
+          comment: 'You seem to not be authorized' # optional. A comment to post if the user is not part of the team.
+                                                  # This feature is only applicable in an issue (or PR) context
+          exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
+
+      - name: Send message on Zulip
+        uses: zulip/github-actions-zulip/send-message@v1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: '[email protected]'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'mathlib reviewers'
+          type: 'stream'
+          topic: 'maintainer merge'
+          content: |
+            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.comment.user.login, github.event.issue.number) }}
+
+            > ${{ github.event.issue.title }}
+
+      - name: Add comment to PR
+        uses: GrantBirki/[email protected]
+        with:
+          issue-number: ${{ github.event.issue.number }}
+          body: |
+            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}.

.github/workflows/maintainer_merge_review.yml

@@ -0,0 +1,40 @@
+name: Maintainer merge (review)
+
+on:
+  pull_request_review:
+    types: [submitted, edited]
+
+jobs:
+  ping_zulip:
+    name: Ping maintainers on Zulip
+    if: (github.event.issue.pull_request != 'null') && (startsWith(github.event.review.body, 'maintainer merge') || contains(toJSON(github.event.review.body), '\r\nmaintainer merge'))
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check whether user is part of mathlib-reviewers team
+        uses: TheModdingInquisition/[email protected]
+        with:
+          organization: 'leanprover-community'
+          team: 'mathlib-reviewers' # required. The team to check for
+          token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
+          exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
+
+      - name: Send message on Zulip
+        uses: zulip/github-actions-zulip/send-message@v1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: '[email protected]'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'mathlib reviewers'
+          type: 'stream'
+          topic: 'maintainer merge'
+          content: |
+            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.review.user.login, github.event.pull_request.number) }}
+
+            > ${{ github.event.pull_request.title }}
+
+      - name: Add comment to PR
+        uses: GrantBirki/[email protected]
+        with:
+          issue-number: ${{ github.event.pull_request.number }}
+          body: |
+            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.review.user.login }}.

.github/workflows/maintainer_merge_review_comment.yml

@@ -0,0 +1,40 @@
+name: Maintainer merge (review comment)
+
+on:
+  pull_request_review_comment:
+    types: [created, edited]
+
+jobs:
+  ping_zulip:
+    name: Ping maintainers on Zulip
+    if: (github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\r\nmaintainer merge'))
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check whether user is part of mathlib-reviewers team
+        uses: TheModdingInquisition/[email protected]
+        with:
+          organization: 'leanprover-community'
+          team: 'mathlib-reviewers' # required. The team to check for
+          token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
+          exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
+
+      - name: Send message on Zulip
+        uses: zulip/github-actions-zulip/send-message@v1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: '[email protected]'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'mathlib reviewers'
+          type: 'stream'
+          topic: 'maintainer merge'
+          content: |
+            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.comment.user.login, github.event.pull_request.number) }}
+
+            > ${{ github.event.pull_request.title }}
+
+      - name: Add comment to PR
+        uses: GrantBirki/[email protected]
+        with:
+          issue-number: ${{ github.event.pull_request.number }}
+          body: |
+            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}.

.gitignore

@@ -9,3 +9,4 @@ all.lean
 *~
 .DS_Store
 *.lock
+port_status.yaml

archive/100-theorems-list/30_ballot_problem.lean

@@ -320,7 +320,7 @@ lemma first_vote_pos :
         (nonempty_image_iff.2 (counted_sequence_nonempty _ _))],
     { have : list.cons (-1) '' counted_sequence (p + 1) q ∩ {l : list ℤ | l.head = 1} = ∅,
       { ext,
-        simp only [mem_inter_eq, mem_image, mem_set_of_eq, mem_empty_eq, iff_false, not_and,
+        simp only [mem_inter_iff, mem_image, mem_set_of_eq, mem_empty_iff_false, iff_false, not_and,
           forall_exists_index, and_imp],
         rintro l _ rfl,
         norm_num },
@@ -392,7 +392,7 @@ begin
   rw [counted_succ_succ, union_inter_distrib_right,
     (_ : list.cons (-1) '' counted_sequence (p + 1) q ∩ {l | l.head = 1} = ∅), union_empty];
   { ext,
-    simp only [mem_inter_eq, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_eq,
+    simp only [mem_inter_iff, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_iff_false,
       iff_false, not_and, forall_exists_index, and_imp],
     rintro y hy rfl,
     norm_num }
@@ -410,7 +410,7 @@ begin
   have : (counted_sequence p (q + 1)).image (list.cons 1) ∩ stays_positive =
          (counted_sequence p (q + 1) ∩ stays_positive).image (list.cons 1),
   { ext t,
-    simp only [mem_inter_eq, mem_image],
+    simp only [mem_inter_iff, mem_image],
     split,
     { simp only [and_imp, exists_imp_distrib],
       rintro l hl rfl t,
@@ -433,7 +433,7 @@ begin
   rw [counted_succ_succ, union_inter_distrib_right,
     (_ : list.cons 1 '' counted_sequence p (q + 1) ∩ {l : list ℤ | l.head = 1}ᶜ = ∅), empty_union];
   { ext,
-    simp only [mem_inter_eq, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_eq,
+    simp only [mem_inter_iff, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_iff_false,
       iff_false, not_and, forall_exists_index, and_imp],
     rintro y hy rfl,
     norm_num }
@@ -451,7 +451,7 @@ begin
   have : (counted_sequence (p + 1) q).image (list.cons (-1)) ∩ stays_positive =
          ((counted_sequence (p + 1) q) ∩ stays_positive).image (list.cons (-1)),
   { ext t,
-    simp only [mem_inter_eq, mem_image],
+    simp only [mem_inter_iff, mem_image],
     split,
     { simp only [and_imp, exists_imp_distrib],
       rintro l hl rfl t,

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -115,16 +115,16 @@ begin
         rintros x ⟨rfl | _⟩ y ⟨rfl | _⟩ _,
         { apply (irrefl _ ‹j < j›).elim },
         { exfalso,
-          apply not_le_of_lt (trans ‹i < j› ‹j < y›) (le_max_of_mem ‹y ∈ t› ‹t.max = i›) },
+          apply not_le_of_lt (trans ‹i < j› ‹j < y›) (le_max_of_eq ‹y ∈ t› ‹t.max = i›) },
         { apply lt_of_le_of_lt _ ‹f i < f j› <|> apply lt_of_lt_of_le ‹f j < f i› _,
-          rcases lt_or_eq_of_le (le_max_of_mem ‹x ∈ t› ‹t.max = i›) with _ | rfl,
+          rcases lt_or_eq_of_le (le_max_of_eq ‹x ∈ t› ‹t.max = i›) with _ | rfl,
           { apply le_of_lt (ht₁.2.2 ‹x ∈ t› (mem_of_max ‹t.max = i›) ‹x < i›) },
           { refl } },
         { apply ht₁.2.2 ‹x ∈ t› ‹y ∈ t› ‹x < y› } },
       -- Finally show that this new subsequence is one longer than the old one.
       { rw [card_insert_of_not_mem, ht₂],
         intro _,
-        apply not_le_of_lt ‹i < j› (le_max_of_mem ‹j ∈ t› ‹t.max = i›) } } },
+        apply not_le_of_lt ‹i < j› (le_max_of_eq ‹j ∈ t› ‹t.max = i›) } } },
       -- Finished both goals!
   -- Now that we have uniqueness of each label, it remains to do some counting to finish off.
   -- Suppose all the labels are small.