Merge commit '65a1391a0106c9204fe45bc73a039f056558cb83'

* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
  feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
  feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
  feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
  move old README.md to OLD_README.md
  doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
  feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
  feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
  feat(probability/independence): Independence of singletons (leanprover-community#18506)
  feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
  feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
  chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
  feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
  feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
  feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
  feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
  feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
  feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
  feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
  ...

# Conflicts:
#	README.md

.devcontainer/README.md

@@ -0,0 +1,11 @@
+# Remote containers for VSCode
+
+Installing the `Remote - Containers` VSCode extension
+will allow you to open a project inside the `leanprovercommunity/mathlib` container
+(meaning you don't even need a local copy of lean installed).
+
+The file `/.devcontainer/devcontainer.json` sets this up:
+if you have the extension installed, you'll be prompted to ask if you'd like to run inside the
+container, no configuration necessary.
+
+See `/.docker/README.md` for a description of the `leanprovercommunity/mathlib` container.

.devcontainer/devcontainer.json

@@ -0,0 +1,21 @@
+{
+	"name": "mathlib",
+	// "image": "leanprovercommunity/mathlib", // it's faster to build the container than download it
+	"build": {
+		"dockerfile": "../.docker/debian/mathlib/Dockerfile",
+	},
+
+	// Set *default* container specific settings.json values on container create.
+	"settings": {
+		"terminal.integrated.shell.linux": "/bin/bash"
+	},
+
+	// Add the IDs of extensions you want installed when the container is created.
+	"extensions": ["jroesch.lean"],
+
+	// Use 'postCreateCommand' to run commands after the container is created.
+	// "postCreateCommand": "uname -a",
+
+	// Comment out connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root.
+	"remoteUser": "lean"
+}

.docker/README.md

@@ -0,0 +1,66 @@
+# Docker containers
+
+The `.docker` directory contains instructions for building Docker containers
+with Lean and mathlib.
+
+## Build
+
+You can build these containers using `scripts/docker_build.sh`.
+This will result in the creation of two containers:
+
+* `leanprovercommunity/lean` - contains elan, lean, and leanproject
+* `leanprovercommunity/mathlib` - additionally contains a copy of mathlib, with oleans
+
+In fact, for each container you'll get two different tags, `:debian` and `:latest`,
+which are just synonyms.
+(We used to have an `alpine` distribution, but it wasn't robust enough to warrant maintenance.)
+There is also a `leanprovercommunity/mathlib:gitpod` for use at
+[https://gitpod.io/](https://gitpod.io/).
+
+## Usage
+
+### gitpod.io
+
+There is a container based on `gitpod/workspace-base`
+enabling [https://gitpod.io/](https://gitpod.io/) to create in-browser VSCode sessions
+with elan/lean/leanproject/mathlib already set up.
+
+Either prepend `https://gitpod.io/#` to basically any URL at github, e.g.
+[https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker](https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker),
+or install a [gitpod browser extension](https://www.gitpod.io/docs/browser-extension/)
+which will add buttons directly on github.
+
+You can enable gitpod for repositories importing mathlib as a dependency simply by creating
+the file `/.gitpod.yml` containing:
+
+```yml
+image: leanprovercommunity/mathlib:gitpod
+
+vscode:
+  extensions:
+    - jroesch.lean
+
+tasks:
+  - command: . /home/gitpod/.profile && leanproject get-mathlib-cache
+```
+
+### Command line
+
+You can use these containers as virtual machines:
+
+```sh
+docker run -it leanprovercommunity/mathlib
+```
+
+### Docker registry
+
+These containers are deployed to the Docker registry, so anyone can just
+`docker run -it leanprovercommunity/mathlib` to get a local lean+mathlib environment.
+
+There is a local script in `scripts/docker_push.sh` for deployment, which requires
+logging in to the leanprovercommunity account at hub.docker.com
+(credentials available to maintainers).
+
+### Remote containers for VSCode
+
+See `/.devcontainer/README.md`.

.docker/debian/lean/Dockerfile

@@ -0,0 +1,59 @@
+# This is the Dockerfile for `leanprovercommunity/lean`.
+# It is based on the generic `debian` image, and installs `elan` and `leanproject`.
+# See also the image `leanprovercommunity/mathlib` which contains a copy of mathlib.
+
+# NOTE: to run this docker image on macos or windows,
+# you will need to increase the allowed memory (in the docker GUI) beyond 2GB
+
+# We start with a temporary `builder` container,
+# in which we install `python` and prepare a standalone version of `leanproject`.
+FROM debian as leanproject-builder
+
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git python3 python3-pip python3-venv zlib1g-dev -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+ENV PATH="/home/lean/.local/bin:$PATH"
+
+# install `leanproject` using `pip`
+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
+# 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
+
+# We now build the final container.
+FROM debian
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
+# install leanproject
+COPY --from=leanproject-builder /home/lean/.local/bin/dist/leanproject /home/lean/.local/bin/

.docker/debian/mathlib/Dockerfile

@@ -0,0 +1,11 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib`.
+# It is based on the `leanprovercommunity/lean` image,
+# and contains a cloned copy of the `mathlib` github repository,
+# along with precompiled oleans.
+
+FROM leanprovercommunity/lean:debian
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+# clone a copy of mathlib, and download precompiled oleans
+RUN leanproject get mathlib

.docker/gitpod/mathlib/Dockerfile

@@ -0,0 +1,30 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM gitpod/workspace-base
+
+USER root
+
+RUN apt-get update && apt-get install curl git python3 python3-pip python3-venv -y
+
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
+# install `leanproject` using `pip`
+# RUN python3 -m pip install --user mathlibtools
+RUN python3 -m pip install --user pipx && python3 -m pipx ensurepath && source ~/.profile && pipx install mathlibtools==1.1.1
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

.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/PULL_REQUEST_TEMPLATE.md

@@ -1,9 +1,23 @@
 
+
 ---
-<!--
-put comments you want to keep out of the PR commit here.
+<!-- The text above the `---` will become the commit message when your
+PR is merged. Please leave a blank newline before the `---`, otherwise
+GitHub will format the text above it as a title.
+
+To indicate co-authors, include lines at the bottom of the commit message 
+(that is, before the `---`) using the following format:
+
+Co-authored-by: Author Name <[email protected]>
+
+Any other comments you want to keep out of the PR commit should go
+below the `---`, and placed outside this HTML comment, or else they
+will be invisible to reviewers.
+
 If this PR depends on other PRs, please list them below this comment,
 using the following format:
 - [ ] depends on: #abc [optional extra text]
 - [ ] depends on: #xyz [optional extra text]
 -->
+
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

.github/workflows/add_label_from_comment.yml

@@ -1,12 +1,12 @@
-name: Add "ready-to-merge" label from comment
+name: Add "ready-to-merge" and "delegated" label from comment
 
 on:
   issue_comment:
     types: [created]
 
 jobs:
-  add_label:
-    name: Add label
+  add_ready_to_merge_label:
+    name: Add ready-to-merge label
     if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge'))
     runs-on: ubuntu-latest
     steps:
@@ -74,3 +74,70 @@ jobs:
           curl --request DELETE \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-author \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
+  add_delegated_label:
+    name: Add delegated label
+    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\r\nbors d'))
+    runs-on: ubuntu-latest
+    steps:
+      - uses: octokit/[email protected]
+        name: Get PR head
+        id: get_pr_head
+        with:
+          route: GET /repos/:repository/pulls/:pull_number
+          repository: ${{ github.repository }}
+          pull_number: ${{ github.event.issue.number }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_pr_head.outputs.data, since it is a string
+      - id: parse_pr_head
+        name: Parse PR head
+        uses: gr2m/[email protected]
+        with:
+          json: ${{ steps.get_pr_head.outputs.data }}
+          head_user: 'head.user.login'
+
+      # we skip the rest if this PR is from a fork,
+      # since the GITHUB_TOKEN doesn't have write perms
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        uses: octokit/[email protected]
+        name: Get comment author
+        id: get_user
+        with:
+          route: GET /repos/:repository/collaborators/:username/permission
+          repository: ${{ github.repository }}
+          username: ${{ github.event.comment.user.login }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_user.outputs.data, since it is a string
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        id: parse_user
+        name: Parse comment author permission
+        uses: gr2m/[email protected]
+        with:
+          json: ${{ steps.get_user.outputs.data }}
+          permission: 'permission'
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        uses: octokit/[email protected]
+        id: add_label
+        name: Add label
+        with:
+          route: POST /repos/:repository/issues/:issue_number/labels
+          repository: ${{ github.repository }}
+          issue_number: ${{ github.event.issue.number }}
+          labels: '["delegated"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        id: remove_labels
+        name: Remove "awaiting-review"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-review \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'