perf: ensure linearity in Parsec.many*Core

Inlined the orElse combinator into Parsec.many*Core in order to ensure
linearity on the accumulator.

.github/workflows/ci.yml

@@ -62,7 +62,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": false,
                 "quick": false,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -76,7 +76,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": true,
                 "quick": true,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -98,7 +98,8 @@ jobs:
                 // exclude seriously slow tests
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
               },
-              {
+              // TODO: suddenly started failing in CI
+              /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
                 "quick": false,
@@ -106,7 +107,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
                 // exclude seriously slow/problematic tests (laketests crash)
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },
+              },*/
               {
                 "name": "macOS",
                 "os": "macos-latest",
@@ -140,8 +141,7 @@ jobs:
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
-                // also, the liasolver test hits “too many exported symbols”
-                "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
+                "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
                 "binary-check": "ldd"
@@ -154,7 +154,7 @@ jobs:
                 "quick": false,
                 "cross": true,
                 "cross_target": "aarch64-unknown-linux-gnu",
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
               },
@@ -252,7 +252,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
+        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -383,8 +383,14 @@ jobs:
           cd build/stage1
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
-          ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: build/stage1/test-results.xml
+        # prefix `if` above with `always` so it's run even if tests failed
+        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
@@ -446,9 +452,10 @@ jobs:
     name: Build matrix complete
     runs-on: ubuntu-latest
     needs: build
-    if: ${{ always() }}
+    # mark as merely cancelled not failed if builds are cancelled
+    if: ${{ !cancelled() }}
     steps:
-    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
+    - if: contains(needs.*.result, 'failure')
       uses: actions/github-script@v7
       with:
         script: |

.github/workflows/nix-ci.yml

@@ -77,7 +77,13 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build $NIX_BUILD_ARGS .#test -o push-test
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: push-test/test-results.xml
+        if: always()
+        continue-on-error: true
       - name: Build manual
         run: |
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc

.github/workflows/pr-release.yml

@@ -126,21 +126,19 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-
-            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
-            fi
-
             STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
             if [[ -n "$STD_REMOTE_TAGS" ]]; then
               echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
+
+              if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
+                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."    
+              else
+                echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+                MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
+              fi
             else
               echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
@@ -151,7 +149,8 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`."
+            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")"
+            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then

CODEOWNERS

@@ -13,6 +13,7 @@
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @semorrison
 /src/Lean/Elab/Tactic/ @semorrison
+/src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
 /src/Lean/PrettyPrinter/ @Kha

RELEASES.md

@@ -11,17 +11,26 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
-* New command `derive_functinal_induction`:
+* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
+
+  In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
+
+* Lean now generates an error if the type of a theorem is **not** a proposition.
+
+* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
+
+* Funcitonal induction principles.
+
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
+
+  For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
     | n+1, 0 => ackermann n 1
     | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  derive_functional_induction ackermann
   ```
   we get
   ```
@@ -31,6 +40,78 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
+* The termination checker now recognizes more recursion patterns without an
+  explicit `termination_by`. In particular the idiom of counting up to an upper
+  bound, as in
+  ```
+  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
+    if _ : i < arr.size then
+      Array.sum arr (i+1) (acc + arr[i])
+    else
+      acc
+  ```
+  is recognized without having to say `termination_by arr.size - i`.
+
+* Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
+  rather than `{a := x, b := y, c := z}`.
+  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
+
+* Now structure instances pretty print with parent structures' fields inlined.
+  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
+  Setting option `pp.structureInstances.flatten` to false turns this off.
+
+* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
+  to enable pretty printing function applications using generalized field notation (defaults to true).
+  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
+
+* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
+  When `pp.mvars` is false, metavariables pretty print as `?_`,
+  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798).
+
+* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
+  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
+  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
+  rather than `Nat.zero` and `Nat.succ n`.
+  Added option `tactic.customEliminators` to control whether to use custom eliminators.
+  [#3629](https://github.com/leanprover/lean4/pull/3629) and
+  [#3655](https://github.com/leanprover/lean4/pull/3655).
+
+Breaking changes:
+
+* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
+```
+def fact : Nat → Nat
+  | 0 => 1
+  | n+1 => (n+1) * fact n
+
+theorem ex : fact 0 = 1 := by unfold fact; decide
+
+#check fact.eq_1
+-- fact.eq_1 : fact 0 = 1
+
+#check fact.eq_2
+-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
+
+#check fact.def
+/-
+fact.def :
+  ∀ (x : Nat),
+    fact x =
+      match x with
+      | 0 => 1
+      | Nat.succ n => (n + 1) * fact n
+-/
+```
+
+* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
+
 v4.7.0
 ---------
 

default.nix

@@ -1,9 +0,0 @@
-# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
-{ nix = (import ./shell.nix {}).nix; } //
-(import (
-  fetchTarball {
-    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
-    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
-) {
-  src =  ./.;
-}).defaultNix

doc/dev/ffi.md

@@ -111,6 +111,15 @@ if (lean_io_result_is_ok(res)) {
 lean_io_mark_end_initialization();
 ```
 
+In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
+```c
+void lean_initialize_thread();
+```
+and should be finalized in order to free all thread-local resources by calling
+```c
+void lean_finalize_thread();
+```
+
 ## `@[extern]` in the Interpreter
 
 The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.

doc/flake.nix

@@ -27,7 +27,7 @@
         src = inputs.mdBook;
         cargoDeps = drv.cargoDeps.overrideAttrs (_: {
           inherit src;
-          outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
+          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
         });
         doCheck = false;
       });

doc/make/index.md

@@ -12,7 +12,7 @@ Platform-Specific Setup
 - [Windows (msys2)](msys2.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
-- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
+- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
 
 Generic Build Instructions
 --------------------------

flake.lock

@@ -1,12 +1,31 @@
 {
   "nodes": {
-    "flake-utils": {
+    "flake-compat": {
+      "flake": false,
       "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "lastModified": 1673956053,
+        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -18,11 +37,11 @@
     "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1676498134,
-        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
+        "lastModified": 1709737301,
+        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
         "owner": "leanprover",
         "repo": "lean4-mode",
-        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
+        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
         "type": "github"
       },
       "original": {
@@ -31,34 +50,35 @@
         "type": "github"
       }
     },
-    "lowdown-src": {
+    "libgit2": {
       "flake": false,
       "locked": {
-        "lastModified": 1633514407,
-        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "lastModified": 1697646580,
+        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
+        "owner": "libgit2",
+        "repo": "libgit2",
+        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
         "type": "github"
       },
       "original": {
-        "owner": "kristapsdz",
-        "repo": "lowdown",
+        "owner": "libgit2",
+        "repo": "libgit2",
         "type": "github"
       }
     },
     "nix": {
       "inputs": {
-        "lowdown-src": "lowdown-src",
+        "flake-compat": "flake-compat",
+        "libgit2": "libgit2",
         "nixpkgs": "nixpkgs",
         "nixpkgs-regression": "nixpkgs-regression"
       },
       "locked": {
-        "lastModified": 1657097207,
-        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "lastModified": 1711102798,
+        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
         "owner": "NixOS",
         "repo": "nix",
-        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "rev": "a22328066416650471c3545b0b138669ea212ab4",
         "type": "github"
       },
       "original": {
@@ -69,16 +89,33 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1653988320,
-        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
+        "lastModified": 1709083642,
+        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixos-22.05-small",
+        "ref": "release-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -101,11 +138,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
@@ -120,7 +157,23 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
       }
     }
   },

flake.nix

@@ -2,6 +2,9 @@
   description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  # old nixpkgs used for portable release with older glibc (2.27)
+  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
+  inputs.nixpkgs-old.flake = false;
   inputs.flake-utils.url = "github:numtide/flake-utils";
   inputs.nix.url = "github:NixOS/nix";
   inputs.lean4-mode = {
@@ -17,14 +20,41 @@
   #  inputs.lean4-mode.follows = "lean4-mode";
   #};
 
-  outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = import nixpkgs {
         inherit system;
         # for `vscode-with-extensions`
         config.allowUnfree = true;
       };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old = import nixpkgs-old { inherit system; };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
+
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
+
+      devShellWithDist = pkgsDist: pkgs.mkShell.override {
+	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+	} ({
+	  buildInputs = with pkgs; [
+	    cmake gmp ccache
+	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+	    # TODO: only add when proven to not affect the flakification
+	    #pkgs.python3
+	  ];
+	  # https://github.com/NixOS/nixpkgs/issues/60919
+	  hardeningDisable = [ "all" ];
+	  # more convenient `ctest` output
+	  CTEST_OUTPUT_ON_FAILURE = 1;
+	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+	  GMP = pkgsDist.gmp.override { withStatic = true; };
+	  GLIBC = pkgsDist.glibc;
+	  GLIBC_DEV = pkgsDist.glibc.dev;
+	  GCC_LIB = pkgsDist.gcc.cc.lib;
+	  ZLIB = pkgsDist.zlib;
+	  GDB = pkgsDist.gdb;
+	});
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
@@ -49,7 +79,10 @@
       };
       defaultPackage = lean-packages.lean-all;
 
-      inherit (lean-packages) devShell;
+      # The default development shell for working on lean itself
+      devShells.default = devShellWithDist pkgs;
+      devShells.oldGlibc = devShellWithDist pkgsDist-old;
+      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
 
       checks.lean = lean-packages.test;
     }) // rec {

nix/bootstrap.nix

@@ -65,7 +65,7 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.so $out/lib/lean
+      mv lib/lean/*.{so,dylib} $out/lib/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -170,10 +170,11 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
-          touch $out
+          mkdir $out
+          mv test-results.xml $out
         '';
       };
       update-stage0 =

nix/buildLeanPackage.nix

@@ -176,7 +176,7 @@ with builtins; let
       # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
       ln -s ${drv.c}/${drv.cPath} src.c
       # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
     '';
   };
   mkMod = mod: deps:

shell.nix

@@ -1,27 +0,0 @@
-let
-  flake = (import ./default.nix);
-  flakePkgs = flake.packages.${builtins.currentSystem};
-in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
-# use `shell` as default
-(attribs: attribs.shell // attribs) rec {
-  shell = pkgs.mkShell.override {
-    stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
-  } (rec {
-    buildInputs = with pkgs; [
-      cmake gmp ccache
-      flakePkgs.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-    ];
-    # https://github.com/NixOS/nixpkgs/issues/60919
-    hardeningDisable = [ "all" ];
-    # more convenient `ctest` output
-    CTEST_OUTPUT_ON_FAILURE = 1;
-  } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-    GMP = pkgsDist.gmp.override { withStatic = true; };
-    GLIBC = pkgsDist.glibc;
-    GLIBC_DEV = pkgsDist.glibc.dev;
-    GCC_LIB = pkgsDist.gcc.cc.lib;
-    ZLIB = pkgsDist.zlib;
-    GDB = pkgsDist.gdb;
-  });
-  nix = flake.devShell.${builtins.currentSystem};
-}

src/CMakeLists.txt

@@ -503,13 +503,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 # set up libInit_shared only on Windows; see also stdlib.make.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
   set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()

src/Init.lean

@@ -33,3 +33,4 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
+import Init.MacroTrace

src/Init/ByCases.lean

@@ -21,9 +21,9 @@ macro_rules
 
 /-! ## if-then-else -/
 
-@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
+@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
+@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
 
 theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
 

src/Init/Control/ExceptCps.lean

@@ -18,6 +18,7 @@ namespace ExceptCpsT
 def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
   x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
 
+set_option linter.unusedVariables false in  -- `s` unused
 @[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error

src/Init/Conv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.Meta
+import Init.Tactics
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -156,7 +156,6 @@ match [a, b] with
 simplifies to `a`. -/
 syntax (name := simpMatch) "simp_match" : conv
 
-
 /-- Executes the given tactic block without converting `conv` goal into a regular goal. -/
 syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
 
@@ -202,7 +201,7 @@ macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
   with inaccessible names to the given names.
 * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
-macro (name := case) tk:"case " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case) tk:"case " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case%$tk $args|* =>%$arr conv' => ($s); all_goals rfl)
 
 /--
@@ -211,7 +210,7 @@ has been solved after applying `tac`, nor admits the goal if `tac` failed.
 Recall that `case` closes the goal using `sorry` when `tac` fails, and
 the tactic execution is not interrupted.
 -/
-macro (name := case') tk:"case' " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case') tk:"case' " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case'%$tk $args|* =>%$arr conv' => $s)
 
 /--

src/Init/Core.lean

@@ -19,7 +19,7 @@ which applies to all applications of the function).
 -/
 @[simp] def inline {α : Sort u} (a : α) : α := a
 
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -165,6 +165,7 @@ whose first component is `a : α` and whose second component is `b : β a`
 It is sometimes known as the dependent sum type, since it is the type level version
 of an indexed summation.
 -/
+@[pp_using_anonymous_constructor]
 structure Sigma {α : Type u} (β : α → Type v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
   (This will usually require a type ascription to determine `β`
@@ -190,6 +191,7 @@ which can cause problems for universe level unification,
 because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
 `PSigma` is usually only used in automation that constructs pairs of arbitrary types.
 -/
+@[pp_using_anonymous_constructor]
 structure PSigma {α : Sort u} (β : α → Sort v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
   (This will usually require a type ascription to determine `β`
@@ -737,13 +739,16 @@ theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a ==
 section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
-theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
+/-- Non-dependent recursor for `HEq` -/
+noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
   h.rec m
 
-theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
+/-- `HEq.ndrec` variant -/
+noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
   h.rec m
 
-theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
+/-- `HEq.ndrec` variant -/
+noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
 
 theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
@@ -1591,7 +1596,7 @@ protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
 The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
 then they have equal equivalence classes.
 -/
-def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
+theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
   Quot.sound
 
 /--

src/Init/Data/AC.lean

@@ -106,7 +106,7 @@ def norm [info : ContextInformation α] (ctx : α) (e : Expr) : List Nat :=
   let xs := if info.isComm ctx then sort xs else xs
   if info.isIdem ctx then mergeIdem xs else xs
 
-theorem List.two_step_induction
+noncomputable def List.two_step_induction
   {motive : List Nat → Sort u}
   (l : List Nat)
   (empty : motive [])

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.Fin.Basic
 import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
-import Init.Util
+import Init.GetElem
 universe u v w
 
 namespace Array
@@ -59,6 +59,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
@@ -456,24 +458,12 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec loop (i : Nat) (j : Nat) (inv : i + j = as.size) : Option Nat :=
-    if hlt : j < as.size then
-      match i, inv with
-      | 0, inv => by
-        apply False.elim
-        rw [Nat.zero_add] at inv
-        rw [inv] at hlt
-        exact absurd hlt (Nat.lt_irrefl _)
-      | i+1, inv =>
-        if p as[j] then
-          some j
-        else
-          have : i + (j+1) = as.size := by
-            rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-          loop i (j+1) this
-    else
-      none
-  loop as.size 0 rfl
+  let rec loop (j : Nat) :=
+    if h : j < as.size then
+      if p as[j] then some j else loop (j + 1)
+    else none
+    termination_by as.size - j
+  loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 a.findIdx? fun a => a == v
@@ -727,33 +717,36 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     termination_by as.size - i
   go 0 #[]
 
-def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
-  if h : i < a.size then
-    let idx  : Fin a.size := ⟨i, h⟩;
-    let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    let a' := a.swap idx idx1
-    eraseIdxAux (i+1) a'
+/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  if h : i.val + 1 < a.size then
+    let a' := a.swap ⟨i.val + 1, h⟩ i
+    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+    have : a'.size - i' < a.size - i := by
+      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
+    a'.feraseIdx i'
   else
     a.pop
-termination_by a.size - i
+termination_by a.size - i.val
 
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  eraseIdxAux (i.val + 1) a
+theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+  induction a, i using Array.feraseIdx.induct with
+  | @case1 a i h a' _ _ ih =>
+    unfold feraseIdx
+    simp [h, a', ih]
+  | case2 a i h =>
+    unfold feraseIdx
+    simp [h]
 
+/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
 def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if i < a.size then eraseIdxAux (i+1) a else a
-
-def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size) : { r : Array α // r.size = a.size - 1 } :=
-  if h : i < r.size then
-    let idx  : Fin r.size := ⟨i, h⟩;
-    let idx1 : Fin r.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
-  else
-    ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
-termination_by r.size - i
-
-def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
-  eraseIdxSzAux a (i.val + 1) a rfl
+  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
@@ -809,7 +802,7 @@ where
     rfl
 
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
-    cases i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, go]
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
 
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/Array/Subarray.lean

@@ -32,6 +32,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
+
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Basic.lean

@@ -73,6 +73,9 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
+@[deprecated isLt]
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
+
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
@@ -615,4 +618,14 @@ section normalization_eqs
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
 
+/-- Converts a list of `Bool`s to a big-endian `BitVec`. -/
+def ofBoolListBE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => cons b (ofBoolListBE bs)
+
+/-- Converts a list of `Bool`s to a little-endian `BitVec`. -/
+def ofBoolListLE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => concat (ofBoolListLE bs) b
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -29,8 +29,6 @@ theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
 @[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
-theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
-
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
 
 @[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
@@ -43,12 +41,36 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
   have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
   omega
 
+@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb x i = false := by
+  rw [getMsb]
+  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
+  omega
+
 theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
+theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
+  rw [getMsb]
+
+theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
+  rw [getMsb]
+  by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
+    simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
+  · congr
+    omega
+  all_goals
+    apply getLsb_ge
+    omega
+
 -- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsg_eq`.
 @[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
@@ -72,7 +94,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
   else
     have w_pos := Nat.pos_of_ne_zero w_zero
     have r : i ≤ w - 1 := by
-      simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
+      simp [Nat.le_sub_iff_add_le w_pos]
       exact i_lt
     have q_lt : w - 1 - i < w := by
       simp only [Nat.sub_sub]
@@ -98,6 +120,8 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
+@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -292,6 +316,19 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
 
+@[simp] theorem getMsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsb (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsb x (i - (m - n))) := by
+  simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
+  by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
+    by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
+  all_goals
+    simp only [h₁, h₂, h₃, h₄]
+    simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
+      Bool.false_and, Bool.and_self] <;>
+    (try apply getLsb_ge) <;>
+    (try apply (getLsb_ge _ _ _).symm) <;>
+    omega
+
 @[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
   simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@@ -458,12 +495,12 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   | y+1 =>
     rw [Nat.succ_eq_add_one] at h
     rw [← h]
-    rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
+    rw [Nat.testBit_two_pow_sub_succ (isLt _)]
     · cases w : decide (i < v)
       · simp at w
         simp [w]
         rw [Nat.testBit_lt_two_pow]
-        calc BitVec.toNat x < 2 ^ v := toNat_lt _
+        calc BitVec.toNat x < 2 ^ v := isLt _
           _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
       · simp
 
@@ -482,6 +519,24 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp [h]
   omega
 
+/-! ### cast -/
+
+@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
 /-! ### shiftLeft -/
 
 @[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@@ -520,7 +575,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
   · simp
     rw [Nat.mod_eq_of_lt]
     rw [Nat.shiftLeft_eq, Nat.pow_add]
-    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
+    exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
   · omega
 
 @[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
@@ -531,6 +586,11 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     <;> simp_all
     <;> (rw [getLsb_ge]; omega)
 
+@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
+  have : n ≤ i + n := by omega
+  simp_all [shiftLeftZeroExtend_eq]
+
 @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
@@ -555,11 +615,18 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
     getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
-  simp [append_def]
+  simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
+@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
+    getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
+  simp [append_def]
+  by_cases h : n ≤ i
+  · simp [h]
+  · simp [h]
+
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
@@ -588,6 +655,31 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
   simp [cons]
 
+@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
+  ext i
+  simp only [getLsb_not, getLsb_append, cond_eq_if]
+  split
+  · simp_all
+  · simp_all; omega
+
+@[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -632,6 +724,13 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
+@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
+  rw [← BitVec.msb, msb_cons]
+
+@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
+  simp [cons, cond_eq_if]
+  omega
+
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
   apply eq_of_getLsb_eq
@@ -652,6 +751,21 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
     · simp_all
     · omega
 
+@[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
+  simp [cons]
+
+@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
 /-! ### concat -/
 
 @[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -827,7 +941,7 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
-/- ! ### intMax -/
+/-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
 def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
@@ -841,4 +955,20 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
     omega
   simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
 
+/-! ### ofBoolList -/
+
+@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
+
+@[simp] theorem getLsb_ofBoolListBE :
+    (ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getLsb_eq_getMsb]
+
+@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
+
+@[simp] theorem getMsb_ofBoolListLE :
+    (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getMsb_eq_getLsb]
+
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -195,18 +199,6 @@ instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 /-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 0).toUInt64 <<< 0x38 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
   (bs.get! 6).toUInt64 <<< 0x30 |||
@@ -216,3 +208,15 @@ def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   (bs.get! 2).toUInt64 <<< 0x10 |||
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

src/Init/Data/Channel.lean

@@ -41,7 +41,7 @@ Sends a message on an `Channel`.
 
 This function does not block.
 -/
-def Channel.send (v : α) (ch : Channel α) : BaseIO Unit :=
+def Channel.send (ch : Channel α) (v : α) : BaseIO Unit :=
   ch.atomically do
     let st ← get
     if st.closed then return

src/Init/Data/Fin/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise.Basic
-import Init.Coe
 
 open Nat
 
@@ -170,9 +168,3 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
 end Fin
-
-instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem xs i h := getElem xs i.1 h
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Data/FloatArray/Basic.lean

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
+
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/Int.lean

@@ -11,3 +11,4 @@ import Init.Data.Int.DivModLemmas
 import Init.Data.Int.Gcd
 import Init.Data.Int.Lemmas
 import Init.Data.Int.Order
+import Init.Data.Int.Pow

src/Init/Data/Int/DivMod.lean

@@ -160,6 +160,12 @@ instance : Mod Int where
 
 @[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
+theorem ofNat_div (m n : Nat) : ↑(m / n) = div ↑m ↑n := rfl
+
+theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
+  | 0, _ => by simp [fdiv]
+  | succ _, _ => rfl
+
 /-!
 # `bmod` ("balanced" mod)
 

src/Init/Data/Int/Gcd.lean

@@ -6,7 +6,12 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Data.Nat.Gcd
+import Init.Data.Nat.Lcm
+import Init.Data.Int.DivModLemmas
 
+/-!
+Definition and lemmas for gcd and lcm over Int
+-/
 namespace Int
 
 /-! ## gcd -/
@@ -14,4 +19,37 @@ namespace Int
 /-- Computes the greatest common divisor of two integers, as a `Nat`. -/
 def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs
 
+theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a := by
+  have := Nat.gcd_dvd_left a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b := by
+  have := Nat.gcd_dvd_right a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]
+@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]
+
+@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]
+@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]
+
+/-! ## lcm -/
+
+/-- Computes the least common multiple of two integers, as a `Nat`. -/
+def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  simp only [lcm]
+  apply Nat.lcm_ne_zero <;> simpa
+
+theorem dvd_lcm_left {a b : Int} : a ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))
+
+theorem dvd_lcm_right {a b : Int} : b ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))
+
+@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _
+
 end Int

src/Init/Data/Int/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Conv
-import Init.PropLemmas
+import Init.NotationExtra
 
 namespace Int
 
@@ -153,7 +153,7 @@ theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat
 theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
   cases n.lt_or_ge k with
   | inl h' =>
-    simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
+    simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
     conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
     apply subNatNat_add_add
   | inr h' => simp [subNatNat_of_le h',
@@ -169,12 +169,11 @@ theorem subNatNat_add_negSucc (m n k : Nat) :
     rw [subNatNat_sub h', Nat.add_comm]
   | inl h' =>
     have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
-    have h₃ : m ≤ n + k := le_of_succ_le_succ h₂
     rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
-    simp [Nat.add_comm]
-    rw [← add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃,
-      Nat.pred_succ]
-    rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
+    simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]
+    rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
+      ← Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
+      Nat.add_comm]
 
 protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
   | (m:Nat), (n:Nat), c => aux1 ..
@@ -188,15 +187,15 @@ protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
   | (m:Nat), -[n+1], -[k+1] => by
     rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
   | -[m+1], -[n+1], -[k+1] => by
-    simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
+    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 where
   aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
     | (k:Nat) => by simp [Nat.add_assoc]
     | -[k+1]  => by simp [subNatNat_add]
   aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
-    simp [add_succ]
+    simp
     rw [Int.add_comm, subNatNat_add_negSucc]
-    simp [add_succ, succ_add, Nat.add_comm]
+    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 
 protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
   rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -391,7 +390,7 @@ theorem ofNat_mul_subNatNat (m n k : Nat) :
     | inl h =>
       have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
       simp [subNatNat_of_lt h, subNatNat_of_lt h']
-      rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
+      rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
         ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
     | inr h =>
       have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
@@ -406,7 +405,7 @@ theorem negSucc_mul_subNatNat (m n k : Nat) :
   | inl h =>
     have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
     rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
-    simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
+    simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
   | inr h => cases Nat.lt_or_ge k n with
     | inl h' =>
       have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
@@ -422,12 +421,12 @@ protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
     simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
   | (m:Nat), -[n+1],  (k:Nat) => by
     simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
-  | (m:Nat), -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+  | (m:Nat), -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
   | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
   | -[m+1],  (n:Nat), -[k+1]  => by
     simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
   | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
-  | -[m+1],  -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
 
 protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
   simp [Int.mul_comm, Int.mul_add]
@@ -499,33 +498,6 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
 theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
   Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
 
-/-! # pow -/
-
-protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
-
-protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
-protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
-  rw [Int.mul_comm, Int.pow_succ]
-
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
-  | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
-
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
-  | 0,      h =>
-    have : i = 0 := eq_zero_of_le_zero h
-    this.symm ▸ Nat.le_refl _
-  | succ j, h =>
-    match le_or_eq_of_le_succ h with
-    | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
-      Nat.mul_one (n^i) ▸ this
-    | Or.inr h =>
-      h.symm ▸ Nat.le_refl _
-
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
-
 /-! NatCast lemmas -/
 
 /-!
@@ -545,10 +517,4 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 @[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
   simp
 
-theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
-  match n with
-  | 0 => rfl
-  | n + 1 =>
-    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
-
 end Int

src/Init/Data/Int/Order.lean

@@ -498,3 +498,525 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN
 @[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
   | 0 => rfl
   | _+1 => rfl
+
+/-! ### toNat' -/
+
+theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
+  | (m : Nat), n => by simp [toNat', Int.ofNat_inj]
+  | -[m+1], n => by constructor <;> nofun
+
+/-! ## Order properties of the integers -/
+
+protected theorem lt_of_not_ge {a b : Int} : ¬a ≤ b → b < a := Int.not_le.mp
+protected theorem not_le_of_gt {a b : Int} : b < a → ¬a ≤ b := Int.not_le.mpr
+
+protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
+
+@[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False := by
+  simp only [Int.not_lt, iff_false]; constructor
+
+theorem eq_negSucc_of_lt_zero : ∀ {a : Int}, a < 0 → ∃ n : Nat, a = -[n+1]
+  | ofNat _, h => absurd h (Int.not_lt.2 (ofNat_zero_le _))
+  | -[n+1],  _ => ⟨n, rfl⟩
+
+protected theorem lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c := by
+  have : -a + (a + b) < -a + (a + c) := Int.add_lt_add_left h _
+  simp [Int.neg_add_cancel_left] at this
+  assumption
+
+protected theorem lt_of_add_lt_add_right {a b c : Int} (h : a + b < c + b) : a < c :=
+  Int.lt_of_add_lt_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]
+
+protected theorem add_lt_add_iff_left (a : Int) : a + b < a + c ↔ b < c :=
+  ⟨Int.lt_of_add_lt_add_left, (Int.add_lt_add_left · _)⟩
+
+protected theorem add_lt_add_iff_right (c : Int) : a + c < b + c ↔ a < b :=
+  ⟨Int.lt_of_add_lt_add_right, (Int.add_lt_add_right · _)⟩
+
+protected theorem add_lt_add {a b c d : Int} (h₁ : a < b) (h₂ : c < d) : a + c < b + d :=
+  Int.lt_trans (Int.add_lt_add_right h₁ c) (Int.add_lt_add_left h₂ b)
+
+protected theorem add_lt_add_of_le_of_lt {a b c d : Int} (h₁ : a ≤ b) (h₂ : c < d) :
+    a + c < b + d :=
+  Int.lt_of_le_of_lt (Int.add_le_add_right h₁ c) (Int.add_lt_add_left h₂ b)
+
+protected theorem add_lt_add_of_lt_of_le {a b c d : Int} (h₁ : a < b) (h₂ : c ≤ d) :
+    a + c < b + d :=
+  Int.lt_of_lt_of_le (Int.add_lt_add_right h₁ c) (Int.add_le_add_left h₂ b)
+
+protected theorem lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b := by
+  have : a + 0 < a + b := Int.add_lt_add_left h a
+  rwa [Int.add_zero] at this
+
+protected theorem lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a := by
+  have : 0 + a < b + a := Int.add_lt_add_right h a
+  rwa [Int.zero_add] at this
+
+protected theorem add_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
+  Int.zero_add 0 ▸ Int.add_le_add ha hb
+
+protected theorem add_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add ha hb
+
+protected theorem add_pos_of_pos_of_nonneg {a b : Int} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_lt_of_le ha hb
+
+protected theorem add_pos_of_nonneg_of_pos {a b : Int} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_le_of_lt ha hb
+
+protected theorem add_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
+  Int.zero_add 0 ▸ Int.add_le_add ha hb
+
+protected theorem add_neg {a b : Int} (ha : a < 0) (hb : b < 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add ha hb
+
+protected theorem add_neg_of_neg_of_nonpos {a b : Int} (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_lt_of_le ha hb
+
+protected theorem add_neg_of_nonpos_of_neg {a b : Int} (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_le_of_lt ha hb
+
+protected theorem lt_add_of_le_of_pos {a b c : Int} (hbc : b ≤ c) (ha : 0 < a) : b < c + a :=
+  Int.add_zero b ▸ Int.add_lt_add_of_le_of_lt hbc ha
+
+theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
+
+theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
+
+@[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
+  lt_add_one_iff.2 (ofNat_zero_le _)
+
+theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
+  Int.le_of_lt (Int.lt_add_one_iff.2 h)
+
+protected theorem nonneg_of_neg_nonpos {a : Int} (h : -a ≤ 0) : 0 ≤ a :=
+  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
+
+protected theorem nonpos_of_neg_nonneg {a : Int} (h : 0 ≤ -a) : a ≤ 0 :=
+  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
+
+protected theorem lt_of_neg_lt_neg {a b : Int} (h : -b < -a) : a < b :=
+  Int.neg_neg a ▸ Int.neg_neg b ▸ Int.neg_lt_neg h
+
+protected theorem pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a :=
+  Int.lt_of_neg_lt_neg <| by rwa [Int.neg_zero]
+
+protected theorem neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0 :=
+  have : -0 < -a := by rwa [Int.neg_zero]
+  Int.lt_of_neg_lt_neg this
+
+protected theorem le_neg_of_le_neg {a b : Int} (h : a ≤ -b) : b ≤ -a := by
+  have h := Int.neg_le_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem neg_le_of_neg_le {a b : Int} (h : -a ≤ b) : -b ≤ a := by
+  have h := Int.neg_le_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem lt_neg_of_lt_neg {a b : Int} (h : a < -b) : b < -a := by
+  have h := Int.neg_lt_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem neg_lt_of_neg_lt {a b : Int} (h : -a < b) : -b < a := by
+  have h := Int.neg_lt_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem sub_nonpos_of_le {a b : Int} (h : a ≤ b) : a - b ≤ 0 := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem le_of_sub_nonpos {a b : Int} (h : a - b ≤ 0) : a ≤ b := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem sub_neg_of_lt {a b : Int} (h : a < b) : a - b < 0 := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem lt_of_sub_neg {a b : Int} (h : a - b < 0) : a < b := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem add_le_of_le_neg_add {a b c : Int} (h : b ≤ -a + c) : a + b ≤ c := by
+  have h := Int.add_le_add_left h a
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem le_neg_add_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ -a + c := by
+  have h := Int.add_le_add_left h (-a)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem add_le_of_le_sub_left {a b c : Int} (h : b ≤ c - a) : a + b ≤ c := by
+  have h := Int.add_le_add_left h a
+  rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
+
+protected theorem le_sub_left_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ c - a := by
+  have h := Int.add_le_add_right h (-a)
+  rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
+
+protected theorem add_le_of_le_sub_right {a b c : Int} (h : a ≤ c - b) : a + b ≤ c := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem le_sub_right_of_add_le {a b c : Int} (h : a + b ≤ c) : a ≤ c - b := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem le_add_of_neg_add_le {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c := by
+  have h := Int.add_le_add_left h b
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem neg_add_le_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c := by
+  have h := Int.add_le_add_left h (-b)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem le_add_of_sub_left_le {a b c : Int} (h : a - b ≤ c) : a ≤ b + c := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel, Int.add_comm] at h
+
+protected theorem le_add_of_sub_right_le {a b c : Int} (h : a - c ≤ b) : a ≤ b + c := by
+  have h := Int.add_le_add_right h c
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem sub_right_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - c ≤ b := by
+  have h := Int.add_le_add_right h (-c)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem le_add_of_neg_add_le_left {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c := by
+  rw [Int.add_comm] at h
+  exact Int.le_add_of_sub_left_le h
+
+protected theorem neg_add_le_left_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c := by
+  rw [Int.add_comm]
+  exact Int.sub_left_le_of_le_add h
+
+protected theorem le_add_of_neg_add_le_right {a b c : Int} (h : -c + a ≤ b) : a ≤ b + c := by
+  rw [Int.add_comm] at h
+  exact Int.le_add_of_sub_right_le h
+
+protected theorem neg_add_le_right_of_le_add {a b c : Int} (h : a ≤ b + c) : -c + a ≤ b := by
+  rw [Int.add_comm] at h
+  exact Int.neg_add_le_left_of_le_add h
+
+protected theorem le_add_of_neg_le_sub_left {a b c : Int} (h : -a ≤ b - c) : c ≤ a + b :=
+  Int.le_add_of_neg_add_le_left (Int.add_le_of_le_sub_right h)
+
+protected theorem neg_le_sub_left_of_le_add {a b c : Int} (h : c ≤ a + b) : -a ≤ b - c := by
+  have h := Int.le_neg_add_of_add_le (Int.sub_left_le_of_le_add h)
+  rwa [Int.add_comm] at h
+
+protected theorem le_add_of_neg_le_sub_right {a b c : Int} (h : -b ≤ a - c) : c ≤ a + b :=
+  Int.le_add_of_sub_right_le (Int.add_le_of_le_sub_left h)
+
+protected theorem neg_le_sub_right_of_le_add {a b c : Int} (h : c ≤ a + b) : -b ≤ a - c :=
+  Int.le_sub_left_of_add_le (Int.sub_right_le_of_le_add h)
+
+protected theorem sub_le_of_sub_le {a b c : Int} (h : a - b ≤ c) : a - c ≤ b :=
+  Int.sub_left_le_of_le_add (Int.le_add_of_sub_right_le h)
+
+protected theorem sub_le_sub_left {a b : Int} (h : a ≤ b) (c : Int) : c - b ≤ c - a :=
+  Int.add_le_add_left (Int.neg_le_neg h) c
+
+protected theorem sub_le_sub_right {a b : Int} (h : a ≤ b) (c : Int) : a - c ≤ b - c :=
+  Int.add_le_add_right h (-c)
+
+protected theorem sub_le_sub {a b c d : Int} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
+  Int.add_le_add hab (Int.neg_le_neg hcd)
+
+protected theorem add_lt_of_lt_neg_add {a b c : Int} (h : b < -a + c) : a + b < c := by
+  have h := Int.add_lt_add_left h a
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem lt_neg_add_of_add_lt {a b c : Int} (h : a + b < c) : b < -a + c := by
+  have h := Int.add_lt_add_left h (-a)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem add_lt_of_lt_sub_left {a b c : Int} (h : b < c - a) : a + b < c := by
+  have h := Int.add_lt_add_left h a
+  rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
+
+protected theorem lt_sub_left_of_add_lt {a b c : Int} (h : a + b < c) : b < c - a := by
+  have h := Int.add_lt_add_right h (-a)
+  rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
+
+protected theorem add_lt_of_lt_sub_right {a b c : Int} (h : a < c - b) : a + b < c := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c - b := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c := by
+  have h := Int.add_lt_add_left h b
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem neg_add_lt_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
+  have h := Int.add_lt_add_left h (-b)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem lt_add_of_sub_left_lt {a b c : Int} (h : a - b < c) : a < b + c := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel, Int.add_comm] at h
+
+protected theorem sub_left_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - b < c := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_sub_right_lt {a b c : Int} (h : a - c < b) : a < b + c := by
+  have h := Int.add_lt_add_right h c
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem sub_right_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - c < b := by
+  have h := Int.add_lt_add_right h (-c)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_neg_add_lt_left {a b c : Int} (h : -b + a < c) : a < b + c := by
+  rw [Int.add_comm] at h
+  exact Int.lt_add_of_sub_left_lt h
+
+protected theorem neg_add_lt_left_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
+  rw [Int.add_comm]
+  exact Int.sub_left_lt_of_lt_add h
+
+protected theorem lt_add_of_neg_add_lt_right {a b c : Int} (h : -c + a < b) : a < b + c := by
+  rw [Int.add_comm] at h
+  exact Int.lt_add_of_sub_right_lt h
+
+protected theorem neg_add_lt_right_of_lt_add {a b c : Int} (h : a < b + c) : -c + a < b := by
+  rw [Int.add_comm] at h
+  exact Int.neg_add_lt_left_of_lt_add h
+
+protected theorem lt_add_of_neg_lt_sub_left {a b c : Int} (h : -a < b - c) : c < a + b :=
+  Int.lt_add_of_neg_add_lt_left (Int.add_lt_of_lt_sub_right h)
+
+protected theorem neg_lt_sub_left_of_lt_add {a b c : Int} (h : c < a + b) : -a < b - c := by
+  have h := Int.lt_neg_add_of_add_lt (Int.sub_left_lt_of_lt_add h)
+  rwa [Int.add_comm] at h
+
+protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c < a + b :=
+  Int.lt_add_of_sub_right_lt (Int.add_lt_of_lt_sub_left h)
+
+protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
+  Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
+
+protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
+  Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
+
+protected theorem sub_lt_sub_left {a b : Int} (h : a < b) (c : Int) : c - b < c - a :=
+  Int.add_lt_add_left (Int.neg_lt_neg h) c
+
+protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b - c :=
+  Int.add_lt_add_right h (-c)
+
+protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
+  Int.add_lt_add hab (Int.neg_lt_neg hcd)
+
+protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
+  (hab : a ≤ b) (hcd : c < d) : a - d < b - c :=
+  Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)
+
+protected theorem sub_lt_sub_of_lt_of_le {a b c d : Int}
+  (hab : a < b) (hcd : c ≤ d) : a - d < b - c :=
+  Int.add_lt_add_of_lt_of_le hab (Int.neg_le_neg hcd)
+
+protected theorem add_le_add_three {a b c d e f : Int}
+    (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f :=
+  Int.add_le_add (Int.add_le_add h₁ h₂) h₃
+
+theorem exists_eq_neg_ofNat {a : Int} (H : a ≤ 0) : ∃ n : Nat, a = -(n : Int) :=
+  let ⟨n, h⟩ := eq_ofNat_of_zero_le (Int.neg_nonneg_of_nonpos H)
+  ⟨n, Int.eq_neg_of_eq_neg h.symm⟩
+
+theorem lt_of_add_one_le {a b : Int} (H : a + 1 ≤ b) : a < b := H
+
+theorem lt_add_one_of_le {a b : Int} (H : a ≤ b) : a < b + 1 := Int.add_le_add_right H 1
+
+theorem le_of_lt_add_one {a b : Int} (H : a < b + 1) : a ≤ b := Int.le_of_add_le_add_right H
+
+theorem sub_one_lt_of_le {a b : Int} (H : a ≤ b) : a - 1 < b :=
+  Int.sub_right_lt_of_lt_add <| lt_add_one_of_le H
+
+theorem le_of_sub_one_lt {a b : Int} (H : a - 1 < b) : a ≤ b :=
+  le_of_lt_add_one <| Int.lt_add_of_sub_right_lt H
+
+theorem le_sub_one_of_lt {a b : Int} (H : a < b) : a ≤ b - 1 := Int.le_sub_right_of_add_le H
+
+theorem lt_of_le_sub_one {a b : Int} (H : a ≤ b - 1) : a < b := Int.add_le_of_le_sub_right H
+
+/- ### Order properties and multiplication -/
+
+protected theorem mul_lt_mul {a b c d : Int}
+    (h₁ : a < c) (h₂ : b ≤ d) (h₃ : 0 < b) (h₄ : 0 ≤ c) : a * b < c * d :=
+  Int.lt_of_lt_of_le (Int.mul_lt_mul_of_pos_right h₁ h₃) (Int.mul_le_mul_of_nonneg_left h₂ h₄)
+
+protected theorem mul_lt_mul' {a b c d : Int}
+    (h₁ : a ≤ c) (h₂ : b < d) (h₃ : 0 ≤ b) (h₄ : 0 < c) : a * b < c * d :=
+  Int.lt_of_le_of_lt (Int.mul_le_mul_of_nonneg_right h₁ h₃) (Int.mul_lt_mul_of_pos_left h₂ h₄)
+
+protected theorem mul_neg_of_pos_of_neg {a b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0 := by
+  have h : a * b < a * 0 := Int.mul_lt_mul_of_pos_left hb ha
+  rwa [Int.mul_zero] at h
+
+protected theorem mul_neg_of_neg_of_pos {a b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0 := by
+  have h : a * b < 0 * b := Int.mul_lt_mul_of_pos_right ha hb
+  rwa [Int.zero_mul] at h
+
+protected theorem mul_nonneg_of_nonpos_of_nonpos {a b : Int}
+  (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b := by
+  have : 0 * b ≤ a * b := Int.mul_le_mul_of_nonpos_right ha hb
+  rwa [Int.zero_mul] at this
+
+protected theorem mul_lt_mul_of_neg_left {a b c : Int} (h : b < a) (hc : c < 0) : c * a < c * b :=
+  have : -c > 0 := Int.neg_pos_of_neg hc
+  have : -c * b < -c * a := Int.mul_lt_mul_of_pos_left h this
+  have : -(c * b) < -(c * a) := by
+    rwa [← Int.neg_mul_eq_neg_mul, ← Int.neg_mul_eq_neg_mul] at this
+  Int.lt_of_neg_lt_neg this
+
+protected theorem mul_lt_mul_of_neg_right {a b c : Int} (h : b < a) (hc : c < 0) : a * c < b * c :=
+  have : -c > 0 := Int.neg_pos_of_neg hc
+  have : b * -c < a * -c := Int.mul_lt_mul_of_pos_right h this
+  have : -(b * c) < -(a * c) := by
+    rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this
+  Int.lt_of_neg_lt_neg this
+
+protected theorem mul_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b := by
+  have : 0 * b < a * b := Int.mul_lt_mul_of_neg_right ha hb
+  rwa [Int.zero_mul] at this
+
+protected theorem mul_self_le_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b :=
+  Int.mul_le_mul h2 h2 h1 (Int.le_trans h1 h2)
+
+protected theorem mul_self_lt_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
+  Int.mul_lt_mul' (Int.le_of_lt h2) h2 h1 (Int.lt_of_le_of_lt h1 h2)
+
+/- ## sign -/
+
+@[simp] theorem sign_zero : sign 0 = 0 := rfl
+@[simp] theorem sign_one : sign 1 = 1 := rfl
+theorem sign_neg_one : sign (-1) = -1 := rfl
+
+@[simp] theorem sign_of_add_one (x : Nat) : Int.sign (x + 1) = 1 := rfl
+@[simp] theorem sign_negSucc (x : Nat) : Int.sign (Int.negSucc x) = -1 := rfl
+
+theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
+  match z with | 0 | succ _ | -[_+1] => rfl
+
+theorem natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1 := by
+  rw [Int.natAbs_sign, if_neg hz]
+
+theorem sign_ofNat_of_nonzero {n : Nat} (hn : n ≠ 0) : Int.sign n = 1 :=
+  match n, Nat.exists_eq_succ_of_ne_zero hn with
+  | _, ⟨n, rfl⟩ => Int.sign_of_add_one n
+
+@[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
+  match z with | 0 | succ _ | -[_+1] => rfl
+
+theorem sign_mul_natAbs : ∀ a : Int, sign a * natAbs a = a
+  | 0      => rfl
+  | succ _ => Int.one_mul _
+  | -[_+1] => (Int.neg_eq_neg_one_mul _).symm
+
+@[simp] theorem sign_mul : ∀ a b, sign (a * b) = sign a * sign b
+  | a, 0 | 0, b => by simp [Int.mul_zero, Int.zero_mul]
+  | succ _, succ _ | succ _, -[_+1] | -[_+1], succ _ | -[_+1], -[_+1] => rfl
+
+theorem sign_eq_one_of_pos {a : Int} (h : 0 < a) : sign a = 1 :=
+  match a, eq_succ_of_zero_lt h with
+  | _, ⟨_, rfl⟩ => rfl
+
+theorem sign_eq_neg_one_of_neg {a : Int} (h : a < 0) : sign a = -1 :=
+  match a, eq_negSucc_of_lt_zero h with
+  | _, ⟨_, rfl⟩ => rfl
+
+theorem eq_zero_of_sign_eq_zero : ∀ {a : Int}, sign a = 0 → a = 0
+  | 0, _ => rfl
+
+theorem pos_of_sign_eq_one : ∀ {a : Int}, sign a = 1 → 0 < a
+  | (_ + 1 : Nat), _ => ofNat_lt.2 (Nat.succ_pos _)
+
+theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
+  | (_ + 1 : Nat), h => nomatch h
+  | 0, h => nomatch h
+  | -[_+1], _ => negSucc_lt_zero _
+
+theorem sign_eq_one_iff_pos (a : Int) : sign a = 1 ↔ 0 < a :=
+  ⟨pos_of_sign_eq_one, sign_eq_one_of_pos⟩
+
+theorem sign_eq_neg_one_iff_neg (a : Int) : sign a = -1 ↔ a < 0 :=
+  ⟨neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg⟩
+
+@[simp] theorem sign_eq_zero_iff_zero (a : Int) : sign a = 0 ↔ a = 0 :=
+  ⟨eq_zero_of_sign_eq_zero, fun h => by rw [h, sign_zero]⟩
+
+@[simp] theorem sign_sign : sign (sign x) = sign x := by
+  match x with
+  | 0 => rfl
+  | .ofNat (_ + 1) => rfl
+  | .negSucc _ => rfl
+
+@[simp] theorem sign_nonneg : 0 ≤ sign x ↔ 0 ≤ x := by
+  match x with
+  | 0 => rfl
+  | .ofNat (_ + 1) =>
+    simp (config := { decide := true }) only [sign, true_iff]
+    exact Int.le_add_one (ofNat_nonneg _)
+  | .negSucc _ => simp (config := { decide := true }) [sign]
+
+theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
+  | succ _ => Int.mul_one _
+  | 0 => Int.mul_zero _
+  | -[_+1] => Int.mul_neg_one _
+
+/- ## natAbs -/
+
+theorem natAbs_ne_zero {a : Int} : a.natAbs ≠ 0 ↔ a ≠ 0 := not_congr Int.natAbs_eq_zero
+
+theorem natAbs_mul_self : ∀ {a : Int}, ↑(natAbs a * natAbs a) = a * a
+  | ofNat _ => rfl
+  | -[_+1]  => rfl
+
+theorem eq_nat_or_neg (a : Int) : ∃ n : Nat, a = n ∨ a = -↑n := ⟨_, natAbs_eq a⟩
+
+theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat}
+    (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs]
+
+@[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by
+  rw [← Int.ofNat_mul, natAbs_mul_self]
+
+theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = n ∨ a = -↑n := by
+  rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_ofNat]
+
+theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by
+  suffices ∀ a b : Nat, natAbs (subNatNat a b.succ) ≤ (a + b).succ by
+    match a, b with
+    | (a:Nat), (b:Nat) => rw [ofNat_add_ofNat, natAbs_ofNat]; apply Nat.le_refl
+    | (a:Nat), -[b+1]  => rw [natAbs_ofNat, natAbs_negSucc]; apply this
+    | -[a+1],  (b:Nat) =>
+      rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]; apply this
+    | -[a+1],  -[b+1]  => rw [natAbs_negSucc, succ_add]; apply Nat.le_refl
+  refine fun a b => subNatNat_elim a b.succ
+    (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
+    (fun i n (e : (n + i).succ = _) => ?_) rfl
+  · intro i n h
+    subst h
+    rw [Nat.add_comm _ i, Nat.add_assoc]
+    exact Nat.le_add_right i (b.succ + b).succ
+  · apply succ_le_succ
+    rw [← succ.inj e, ← Nat.add_assoc, Nat.add_comm]
+    apply Nat.le_add_right
+
+theorem natAbs_sub_le (a b : Int) : natAbs (a - b) ≤ natAbs a + natAbs b := by
+  rw [← Int.natAbs_neg b]; apply natAbs_add_le
+
+theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1 := by simp only [negSucc_eq, Int.neg_add]; rfl
+
+theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
+    (w₁ : 0 ≤ a) (w₂ : a < b) : a.natAbs < b.natAbs :=
+  match a, b, eq_ofNat_of_zero_le w₁, eq_ofNat_of_zero_le (Int.le_trans w₁ (Int.le_of_lt w₂)) with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_lt.1 w₂
+
+theorem eq_natAbs_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0 := by
+  rw [natAbs_eq_iff, Int.mul_eq_zero, ← Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
+
+end Int

src/Init/Data/Int/Pow.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Lemmas
+
+namespace Int
+
+/-! # pow -/
+
+protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
+
+protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
+protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
+  rw [Int.mul_comm, Int.pow_succ]
+
+theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
+  | 0      => Nat.le_refl _
+  | i + 1 => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
+
+theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
+  | 0,      h =>
+    have : i = 0 := Nat.eq_zero_of_le_zero h
+    this.symm ▸ Nat.le_refl _
+  | j + 1, h =>
+    match Nat.le_or_eq_of_le_succ h with
+    | Or.inl h => show n^i ≤ n^j * n from
+      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
+      Nat.mul_one (n^i) ▸ this
+    | Or.inr h =>
+      h.symm ▸ Nat.le_refl _
+
+theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
+  pow_le_pow_of_le_right h (Nat.zero_le _)
+
+theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
+  match n with
+  | 0 => rfl
+  | n + 1 =>
+    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
+
+end Int

src/Init/Data/List.lean

@@ -8,3 +8,4 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
+import Init.Data.List.Impl

src/Init/Data/List/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
@@ -54,15 +55,6 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
-instance : GetElem (List α) Nat α fun as i => i < as.length where
-  getElem as i h := as.get ⟨i, h⟩
-
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
-  rfl
-
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
-  rfl
-
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]
@@ -458,7 +450,7 @@ contains the longest initial segment for which `p` returns true
 and the second part is everything else.
 
 * `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
-* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
+* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
 -/
 @[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
   loop as []
@@ -520,11 +512,6 @@ def drop : Nat → List α → List α
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
-  match as, i with
-  | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
-
 /--
 `O(min n |xs|)`. Returns the first `n` elements of `xs`, or the whole list if `n` is too large.
 * `take 0 [a, b, c, d, e] = []`

src/Init/Data/List/Impl.lean

@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Lemmas
+
+/-!
+## Tail recursive implementations for `List` definitions.
+
+Many of the proofs require theorems about `Array`,
+so these are in a separate file to minimize imports.
+-/
+
+namespace List
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where
+  /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
+  unless `n ≥ l.length` in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::xs, 0, acc => acc.toListAppend (a::xs)
+  | x::xs, n+1, acc => go xs n (acc.push x)
+
+@[csimp] theorem set_eq_setTR : @set = @setTR := by
+  funext α l n a; simp [setTR]
+  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
+    setTR.go l a xs n acc = acc.data ++ xs.set n a
+  | [], _ => fun h => by simp [setTR.go, set, h]
+  | x::xs, 0 => by simp [setTR.go, set]
+  | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
+  exact (go #[] _ _ rfl).symm
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where
+  /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Array α → List α
+  | [], _ => l
+  | x::xs, acc => bif x == a then acc.toListAppend xs else go xs (acc.push x)
+
+@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
+  funext α _ l a; simp [eraseTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc h
+  | nil => simp [List.erase, eraseTR.go, h]
+  | cons x xs IH =>
+    simp [List.erase, eraseTR.go]
+    cases x == a <;> simp
+    · rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `eraseIdx`. -/
+@[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where
+  /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::as, 0, acc => acc.toListAppend as
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
+  funext α l n; simp [eraseIdxTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc h
+  | nil => simp [eraseIdx, eraseIdxTR.go, h]
+  | cons x xs IH =>
+    match n with
+    | 0 => simp [eraseIdx, eraseIdxTR.go]
+    | n+1 =>
+      simp [eraseIdx, eraseIdxTR.go]
+      rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `bind`. -/
+@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | x::xs, acc => go xs (acc ++ f x)
+
+@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+  funext α β as f
+  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
+    | [], acc => by simp [bindTR.go, bind]
+    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  exact (go as #[]).symm
+
+/-- Tail recursive version of `join`. -/
+@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
+
+@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
+  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+
+/-- Tail recursive version of `filterMap`. -/
+@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
+  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | a::as, acc => match f a with
+    | none => go as acc
+    | some b => go as (acc.push b)
+
+@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
+  funext α β f l
+  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
+    | [], acc => by simp [filterMapTR.go, filterMap]
+    | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
+  exact (go l #[]).symm
+
+/-- Tail recursive version of `replace`. -/
+@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
+  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
+  unless `b` is not found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+
+@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
+  funext α _ l b c; simp [replaceTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [replace, replaceTR.go]
+  | cons x xs IH =>
+    simp [replace, replaceTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `take`. -/
+@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
+  unless `n ≥ xs.length` in which case it returns `l`. -/
+  @[specialize] go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::_, 0, acc => acc.toList
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext α n l; simp [takeTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc
+  | nil => cases n <;> simp [take, takeTR.go]
+  | cons x xs IH =>
+    cases n with simp [take, takeTR.go]
+    | succ n => intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `takeWhile`. -/
+@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
+  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
+  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
+
+@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
+  funext α p l; simp [takeWhileTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [takeWhile, takeWhileTR.go]
+  | cons x xs IH =>
+    simp [takeWhile, takeWhileTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `foldr`. -/
+@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
+
+@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
+
+/-- Tail recursive version of `zipWith`. -/
+@[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where
+  /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/
+  go : List α → List β → Array γ → List γ
+  | a::as, b::bs, acc => go as bs (acc.push (f a b))
+  | _, _, acc => acc.toList
+
+@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
+  funext α β γ f as bs
+  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
+    | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
+    | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
+  exact (go as bs #[]).symm
+
+/-- Tail recursive version of `unzip`. -/
+def unzipTR (l : List (α × β)) : List α × List β :=
+  l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
+
+@[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
+  funext α β l; simp [unzipTR]; induction l <;> simp [*]
+
+/-- Tail recursive version of `enumFrom`. -/
+def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
+  let arr := l.toArray
+  (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
+
+@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
+  funext α n l; simp [enumFromTR, -Array.size_toArray]
+  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
+      simp [enumFrom, f]
+  rw [Array.foldr_eq_foldr_data]
+  simp [go]
+
+theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
+  | 0 => rfl
+  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
+    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
+
+/-- Tail recursive version of `dropLast`. -/
+@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
+
+@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
+  funext α l; simp [dropLastTR]
+
+/-- Tail recursive version of `intersperse`. -/
+def intersperseTR (sep : α) : List α → List α
+  | [] => []
+  | [x] => [x]
+  | x::y::xs => x :: sep :: y :: xs.foldr (fun a r => sep :: a :: r) []
+
+@[csimp] theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR := by
+  funext α sep l; simp [intersperseTR]
+  match l with
+  | [] | [_] => rfl
+  | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
+
+/-- Tail recursive version of `intercalate`. -/
+def intercalateTR (sep : List α) : List (List α) → List α
+  | [] => []
+  | [x] => x
+  | x::xs => go sep.toArray x xs #[]
+where
+  /-- Auxiliary for `intercalateTR`:
+  `intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)` -/
+  go (sep : Array α) : List α → List (List α) → Array α → List α
+  | x, [], acc => acc.toListAppend x
+  | x, y::xs, acc => go sep y xs (acc ++ x ++ sep)
+
+@[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by
+  funext α sep l; simp [intercalate, intercalateTR]
+  match l with
+  | [] => rfl
+  | [_] => simp
+  | x::y::xs =>
+    let rec go {acc x} : ∀ xs,
+      intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
+    | [] => by simp [intercalateTR.go]
+    | _::_ => by simp [intercalateTR.go, go]
+    simp [intersperse, go]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -266,6 +266,12 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
+@[simp] theorem getD_nil : getD [] n d = d := rfl
+
+@[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
+
+@[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -705,3 +711,5 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
   | _ :: l, i + 1, j + 1 => by
     have g : i ≠ j := h ∘ congrArg (· + 1)
     simp [get_set_ne l g]
+
+end List

src/Init/Data/Nat.lean

@@ -17,3 +17,5 @@ import Init.Data.Nat.Linear
 import Init.Data.Nat.SOM
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
+import Init.Data.Nat.Lcm
+import Init.Data.Nat.Compare

src/Init/Data/Nat/Basic.lean

@@ -10,6 +10,29 @@ universe u
 
 namespace Nat
 
+/-- Compiled version of `Nat.rec` so that we can define `Nat.recAux` to be defeq to `Nat.rec`.
+This is working around the fact that the compiler does not currently support recursors. -/
+private def recCompiled {motive : Nat → Sort u} (zero : motive zero) (succ : (n : Nat) → motive n → motive (Nat.succ n)) : (t : Nat) → motive t
+  | .zero => zero
+  | .succ n => succ n (recCompiled zero succ n)
+
+@[csimp]
+private theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled :=
+  funext fun _ => funext fun _ => funext fun succ => funext fun t =>
+    Nat.recOn t rfl (fun n ih => congrArg (succ n) ih)
+
+/-- Recursor identical to `Nat.rec` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`.
+Used as the default `Nat` eliminator by the `induction` tactic. -/
+@[elab_as_elim, induction_eliminator]
+protected abbrev recAux {motive : Nat → Sort u} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) : motive t :=
+  Nat.rec zero succ t
+
+/-- Recursor identical to `Nat.casesOn` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`.
+Used as the default `Nat` eliminator by the `cases` tactic. -/
+@[elab_as_elim, cases_eliminator]
+protected abbrev casesAuxOn {motive : Nat → Sort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : motive t :=
+  Nat.casesOn t zero succ
+
 /--
 `Nat.fold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
 * `Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2`
@@ -125,9 +148,12 @@ theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
 theorem add_one (n : Nat) : n + 1 = succ n :=
   rfl
 
-theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
+@[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
   rfl
 
+@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
+@[simp] theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := nofun
+
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
   | n, 0   => Eq.symm (Nat.zero_add n)
   | n, m+1 => by
@@ -209,6 +235,9 @@ protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
 protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
   rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
 
+protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
+protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
+
 /-! # Inequalities -/
 
 attribute [simp] Nat.le_refl
@@ -257,7 +286,7 @@ theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
 theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
   induction c with
   | zero => simp
-  | succ c ih => simp [Nat.add_succ, Nat.sub_succ, ih]
+  | succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
 
 protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
   Nat.le_trans
@@ -606,8 +635,6 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 @[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 :=
   fun h => Nat.noConfusion h
 
-theorem add_one_ne_zero (n) : n + 1 ≠ 0 := succ_ne_zero _
-
 /-! # mul + order -/
 
 theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
@@ -716,6 +743,11 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
 theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n
   | _+1, _ => rfl
 
+theorem sub_one_add_one_eq_of_pos : ∀ {n}, 0 < n → (n - 1) + 1 = n
+  | _+1, _ => rfl
+
+@[simp] theorem pred_eq_sub_one : pred n = n - 1 := rfl
+
 /-! # sub theorems -/
 
 theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
@@ -738,7 +770,7 @@ theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i := by
   | zero => contradiction
   | succ a ih =>
     match Nat.eq_or_lt_of_le h with
-    | Or.inl h => injection h with h; subst h; rw [←Nat.add_one, Nat.add_sub_self_left]; decide
+    | Or.inl h => injection h with h; subst h; rw [Nat.add_sub_self_left]; decide
     | Or.inr h =>
       have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
       exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
@@ -752,7 +784,7 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
 
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
-  | 0, succ b, _ => by simp
+  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true]
   | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
   | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
 
@@ -770,7 +802,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
 protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
   induction k with
   | zero => simp
-  | succ k ih => simp [add_succ, add_succ, succ_sub_succ, ih]
+  | succ k ih => simp [← Nat.add_assoc, ih]
 
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
@@ -883,7 +915,7 @@ protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m :=
 protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
   induction k with
   | zero => simp
-  | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
+  | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.add_succ, Nat.sub_succ, ih]
 
 protected theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n :=
   match m, le.dest h with

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -63,7 +63,7 @@ theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
-  | k + 1 => by simp [add_succ, shiftRight_add, shiftRight_succ]
+  | k + 1 => by simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]
 
 theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Joe Hendrix
 
 prelude
 import Init.Data.Bool
+import Init.Data.Int.Pow
 import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.TacticsExtra

src/Init/Data/Nat/Compare.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+prelude
+import Init.Classical
+import Init.Data.Ord
+
+/-! # Basic lemmas about comparing natural numbers
+
+This file introduce some basic lemmas about compare as applied to natural
+numbers.
+-/
+namespace Nat
+
+theorem compare_def_lt (a b : Nat) :
+    compare a b = if a < b then .lt else if b < a then .gt else .eq := by
+  simp only [compare, compareOfLessAndEq]
+  split
+  · rfl
+  · next h =>
+    match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with
+    | .inl h => simp [h, Nat.ne_of_gt h]
+    | .inr rfl => simp
+
+theorem compare_def_le (a b : Nat) :
+    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
+  rw [compare_def_lt]
+  split
+  · next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]
+  · next hge =>
+    split
+    · next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]
+    · next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]
+
+protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
+  simp only [compare_def_le]; (repeat' split) <;> try rfl
+  next h1 h2 => cases h1 (Nat.le_of_not_le h2)
+
+protected theorem compare_eq_eq {a b : Nat} : compare a b = .eq ↔ a = b := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
+  next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)
+
+protected theorem compare_eq_lt {a b : Nat} : compare a b = .lt ↔ a < b := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [*]
+
+protected theorem compare_eq_gt {a b : Nat} : compare a b = .gt ↔ b < a := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
+
+protected theorem compare_ne_gt {a b : Nat} : compare a b ≠ .gt ↔ a ≤ b := by
+  rw [compare_def_le]; (repeat' split) <;> simp [*]
+
+protected theorem compare_ne_lt {a b : Nat} : compare a b ≠ .lt ↔ b ≤ a := by
+  rw [compare_def_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+
+end Nat

src/Init/Data/Nat/Div.lean

@@ -10,6 +10,13 @@ import Init.Data.Nat.Basic
 
 namespace Nat
 
+/--
+Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
+there is some `c` such that `b = a * c`.
+-/
+instance : Dvd Nat where
+  dvd a b := Exists (fun c => b = a * c)
+
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
   fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
 
@@ -28,7 +35,7 @@ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 e
   rw [Nat.div]
   rfl
 
-theorem div.inductionOn.{u}
+def div.inductionOn.{u}
       {motive : Nat → Nat → Sort u}
       (x y : Nat)
       (ind  : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
@@ -95,7 +102,7 @@ protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]
 
-theorem mod.inductionOn.{u}
+def mod.inductionOn.{u}
       {motive : Nat → Nat → Sort u}
       (x y  : Nat)
       (ind  : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
@@ -198,11 +205,11 @@ theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
   induction y, k using mod.inductionOn generalizing x with
     (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
   | base y k h =>
-    simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
-    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
+    simp only [add_one, succ_mul, false_iff, Nat.not_le]
+    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
     exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
   | ind y k h IH =>
-    rw [← add_one, Nat.add_le_add_iff_right, IH k0, succ_mul,
+    rw [Nat.add_le_add_iff_right, IH k0, succ_mul,
         ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]
 
 protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) := by
@@ -286,7 +293,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
         rw [mul_succ] at h₁
         exact h₁
       rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
-      simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
+      simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
 
 theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
@@ -327,4 +334,50 @@ theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
   intro h₁
   apply Nat.not_le_of_gt h₀ h₁.right
 
+protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
+  let t := add_mul_div_right 0 m H
+  rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
+
+protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by
+  rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
+
+protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
+  | 0, _ => by simp [Nat.div_zero, n.zero_le]
+  | succ k, h => by
+    suffices succ k * (m / succ k) ≤ succ k * n from
+      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
+    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
+    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
+    have h3 : m ≤ succ k * n := h
+    rw [← h2] at h3
+    exact Nat.le_trans h1 h3
+
+@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
+  induction n <;> simp_all [mul_succ]
+
+@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
+  rw [Nat.mul_comm, mul_div_right _ H]
+
+protected theorem div_self (H : 0 < n) : n / n = 1 := by
+  let t := add_div_right 0 H
+  rwa [Nat.zero_add, Nat.zero_div] at t
+
+protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
+by rw [H2, Nat.mul_div_cancel _ H1]
+
+protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
+by rw [H2, Nat.mul_div_cancel_left _ H1]
+
+protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
+    m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
+
+protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
+    n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
+
+theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
+  match n, Nat.eq_zero_or_pos n with
+  | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
+  | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
+
+
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -5,17 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
-import Init.TacticsExtra
+import Init.Meta
 
 namespace Nat
 
-/--
-Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
-there is some `c` such that `b = a * c`.
--/
-instance : Dvd Nat where
-  dvd a b := Exists (fun c => b = a * c)
-
 protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
 
 protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
@@ -104,4 +97,36 @@ protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   subst h
   rw [Nat.mul_assoc, add_mul_mod_self_left]
 
+protected theorem dvd_of_mul_dvd_mul_left
+    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n := by
+  let ⟨l, H⟩ := H
+  rw [Nat.mul_assoc] at H
+  exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩
+
+protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
+  rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
+
+theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
+  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+
+protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
+  | ⟨e, he⟩, ⟨f, hf⟩ =>
+    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩
+
+protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
+  Nat.mul_dvd_mul (Nat.dvd_refl a) h
+
+protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
+  Nat.mul_dvd_mul h (Nat.dvd_refl c)
+
+@[simp] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
+  ⟨eq_one_of_dvd_one, fun h => h.symm ▸ Nat.dvd_refl _⟩
+
+protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by
+  match Nat.eq_zero_or_pos k with
+  | .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
+  | .inr hpos =>
+    have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
+    rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
+
 end Nat

src/Init/Data/Nat/Gcd.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Dvd
+import Init.NotationExtra
+import Init.RCases
 
 namespace Nat
 
@@ -14,8 +16,8 @@ def gcd (m n : @& Nat) : Nat :=
     n
   else
     gcd (n % m) m
-termination_by m
-decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
+  termination_by m
+  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
 @[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
   rfl
@@ -69,4 +71,166 @@ theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
   | H0 n => rw [gcd_zero_left]; exact kn
   | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
 
+theorem dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
+  ⟨fun h => let ⟨h₁, h₂⟩ := gcd_dvd m n; ⟨Nat.dvd_trans h h₁, Nat.dvd_trans h h₂⟩,
+   fun ⟨h₁, h₂⟩ => dvd_gcd h₁ h₂⟩
+
+theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
+  Nat.dvd_antisymm
+    (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
+    (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
+
+theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
+  ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
+   fun h => h ▸ gcd_dvd_right m n⟩
+
+theorem gcd_eq_right_iff_dvd : m ∣ n ↔ gcd n m = m := by
+  rw [gcd_comm]; exact gcd_eq_left_iff_dvd
+
+theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
+  Nat.dvd_antisymm
+    (dvd_gcd
+      (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
+      (dvd_gcd (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
+        (gcd_dvd_right (gcd m n) k)))
+    (dvd_gcd
+      (dvd_gcd (gcd_dvd_left m (gcd n k))
+        (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
+      (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
+
+@[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
+
+theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by
+  induction n, k using gcd.induction with
+  | H0 k => simp
+  | H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH
+
+theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n := by
+  rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]
+
+theorem gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < gcd m n :=
+  pos_of_dvd_of_pos (gcd_dvd_left m n) mpos
+
+theorem gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < gcd m n :=
+  pos_of_dvd_of_pos (gcd_dvd_right m n) npos
+
+theorem div_gcd_pos_of_pos_left (b : Nat) (h : 0 < a) : 0 < a / a.gcd b :=
+  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_left _ h)
+
+theorem div_gcd_pos_of_pos_right (a : Nat) (h : 0 < b) : 0 < b / a.gcd b :=
+  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_right _ h)
+
+theorem eq_zero_of_gcd_eq_zero_left {m n : Nat} (H : gcd m n = 0) : m = 0 :=
+  match eq_zero_or_pos m with
+  | .inl H0 => H0
+  | .inr H1 => absurd (Eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1))
+
+theorem eq_zero_of_gcd_eq_zero_right {m n : Nat} (H : gcd m n = 0) : n = 0 := by
+  rw [gcd_comm] at H
+  exact eq_zero_of_gcd_eq_zero_left H
+
+theorem gcd_ne_zero_left : m ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_left
+
+theorem gcd_ne_zero_right : n ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_right
+
+theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
+    gcd (m / k) (n / k) = gcd m n / k :=
+  match eq_zero_or_pos k with
+  | .inl H0 => by simp [H0]
+  | .inr H3 => by
+    apply Nat.eq_of_mul_eq_mul_right H3
+    rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
+        Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]
+
+theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : gcd m n ∣ gcd k n :=
+  dvd_gcd (Nat.dvd_trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)
+
+theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : gcd n m ∣ gcd n k :=
+  dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)
+
+theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
+  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
+
+theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
+  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
+
+theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n ∣ gcd m (k * n) :=
+  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
+
+theorem gcd_dvd_gcd_mul_right_right (m n k : Nat) : gcd m n ∣ gcd m (n * k) :=
+  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_right _ _)
+
+theorem gcd_eq_left {m n : Nat} (H : m ∣ n) : gcd m n = m :=
+  Nat.dvd_antisymm (gcd_dvd_left _ _) (dvd_gcd (Nat.dvd_refl _) H)
+
+theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n := by
+  rw [gcd_comm, gcd_eq_left H]
+
+@[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
+  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))
+
+@[simp] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
+  rw [gcd_comm, gcd_mul_left_left]
+
+@[simp] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
+  rw [Nat.mul_comm, gcd_mul_left_left]
+
+@[simp] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
+  rw [gcd_comm, gcd_mul_right_left]
+
+@[simp] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
+  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) (Nat.dvd_refl _))
+
+@[simp] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
+  rw [gcd_comm n m, gcd_gcd_self_right_left]
+
+@[simp] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
+  rw [gcd_comm, gcd_gcd_self_right_right]
+
+@[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
+  rw [gcd_comm m n, gcd_gcd_self_left_right]
+
+theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
+  simp [gcd_rec m (n + k * m), gcd_rec m n]
+
+theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
+  ⟨fun h => ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩,
+   fun h => by simp [h]⟩
+
+/-- Characterization of the value of `Nat.gcd`. -/
+theorem gcd_eq_iff (a b : Nat) :
+    gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g) := by
+  constructor
+  · rintro rfl
+    exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _, fun _ => Nat.dvd_gcd⟩
+  · rintro ⟨ha, hb, hc⟩
+    apply Nat.dvd_antisymm
+    · apply hc
+      · exact gcd_dvd_left a b
+      · exact gcd_dvd_right a b
+    · exact Nat.dvd_gcd ha hb
+
+/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
+def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
+    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
+  if h0 : gcd k m = 0 then
+    ⟨⟨⟨0, eq_zero_of_gcd_eq_zero_right h0 ▸ Nat.dvd_refl 0⟩,
+      ⟨n, Nat.dvd_refl n⟩⟩,
+      eq_zero_of_gcd_eq_zero_left h0 ▸ (Nat.zero_mul n).symm⟩
+  else by
+    have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
+    refine ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, ?_⟩⟩, hd.symm⟩
+    apply Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_ne_zero h0)
+    rw [hd, ← gcd_mul_right]
+    exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) H
+
+theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
+  let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
+    prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)
+  rw [h]
+  have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..
+  exact Nat.mul_dvd_mul
+    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
+    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
+
 end Nat

src/Init/Data/Nat/Lcm.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Data.Nat.Gcd
+import Init.Data.Nat.Lemmas
+
+namespace Nat
+
+/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
+def lcm (m n : Nat) : Nat := m * n / gcd m n
+
+theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
+  rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
+
+@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
+
+@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm]
+
+@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
+
+@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
+
+@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
+  match eq_zero_or_pos m with
+  | .inl h => rw [h, lcm_zero_left]
+  | .inr h => simp [lcm, Nat.mul_div_cancel _ h]
+
+theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
+  ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
+
+theorem dvd_lcm_right (m n : Nat) : n ∣ lcm m n := lcm_comm n m ▸ dvd_lcm_left n m
+
+theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
+  rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
+
+theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := by
+  match eq_zero_or_pos k with
+  | .inl h => rw [h]; exact Nat.dvd_zero _
+  | .inr kpos =>
+    apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
+    rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
+    exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
+
+theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
+Nat.dvd_antisymm
+  (lcm_dvd
+    (lcm_dvd (dvd_lcm_left m (lcm n k))
+      (Nat.dvd_trans (dvd_lcm_left n k) (dvd_lcm_right m (lcm n k))))
+    (Nat.dvd_trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
+  (lcm_dvd
+    (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
+    (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
+      (dvd_lcm_right (lcm m n) k)))
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  intro h
+  have h1 := gcd_mul_lcm m n
+  rw [h, Nat.mul_zero] at h1
+  match mul_eq_zero.1 h1.symm with
+  | .inl hm1 => exact hm hm1
+  | .inr hn1 => exact hn hn1
+
+end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Dvd
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
+import Init.Omega
 
 /-! # Basic lemmas about natural numbers
 
@@ -19,7 +19,6 @@ and later these lemmas should be organised into other files more systematically.
 -/
 
 namespace Nat
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -335,6 +334,32 @@ protected theorem sub_max_sub_right : ∀ (a b c : Nat), max (a - c) (b - c) = m
   | _, _, 0 => rfl
   | _, _, _+1 => Eq.trans (Nat.pred_max_pred ..) <| congrArg _ (Nat.sub_max_sub_right ..)
 
+protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
+  omega
+
+protected theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c := by
+  omega
+
+protected theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c := by
+  induction a generalizing b with
+  | zero => simp
+  | succ i ind =>
+    cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_max_add_right, ind]
+
+protected theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c := by
+  induction a generalizing b with
+  | zero => simp
+  | succ i ind =>
+    cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_min_add_right, ind]
+
+protected theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_max_mul_right ..
+
+protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_min_mul_right ..
+
 -- protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
 --   induction b, c using Nat.recDiagAux with
 --   | zero_left => rw [Nat.sub_zero, Nat.zero_max]; exact Nat.min_eq_right (Nat.sub_le ..)
@@ -383,10 +408,6 @@ protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
 protected theorem mul_mul_mul_comm (a b c d : Nat) : (a * b) * (c * d) = (a * c) * (b * d) := by
   rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_left_comm b]
 
-protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
-
-protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
-
 theorem mul_eq_zero : ∀ {m n}, n * m = 0 ↔ n = 0 ∨ m = 0
   | 0, _ => ⟨fun _ => .inr rfl, fun _ => rfl⟩
   | _, 0 => ⟨fun _ => .inl rfl, fun _ => Nat.zero_mul ..⟩
@@ -484,51 +505,6 @@ protected theorem pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a := by
 
 /-! ### div/mod -/
 
-protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
-  | 0, _ => by simp [Nat.div_zero, n.zero_le]
-  | succ k, h => by
-    suffices succ k * (m / succ k) ≤ succ k * n from
-      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
-    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
-    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
-    have h3 : m ≤ succ k * n := h
-    rw [← h2] at h3
-    exact Nat.le_trans h1 h3
-
-@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
-  induction n <;> simp_all [mul_succ]
-
-@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
-  rw [Nat.mul_comm, mul_div_right _ H]
-
-protected theorem div_self (H : 0 < n) : n / n = 1 := by
-  let t := add_div_right 0 H
-  rwa [Nat.zero_add, Nat.zero_div] at t
-
-protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
-  let t := add_mul_div_right 0 m H
-  rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
-
-protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m :=
-by rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
-
-protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
-by rw [H2, Nat.mul_div_cancel _ H1]
-
-protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
-by rw [H2, Nat.mul_div_cancel_left _ H1]
-
-protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
-    m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
-
-protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
-    n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
-
-theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
-  match n, Nat.eq_zero_or_pos n with
-  | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
-  | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
-
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
   match n % 2, @Nat.mod_lt n 2 (by decide) with
   | 0, _ => .inl rfl
@@ -719,37 +695,17 @@ theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
 
 /-! ### dvd -/
 
-theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
-  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
+    a = b * c := by
+  rw [← H2, Nat.mul_div_cancel' H1]
 
-protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
-  | ⟨e, he⟩, ⟨f, hf⟩ =>
-    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩
+protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = b * c :=
+  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
 
-protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
-  Nat.mul_dvd_mul (Nat.dvd_refl a) h
-
-protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
-  Nat.mul_dvd_mul h (Nat.dvd_refl c)
-
-@[simp] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
-  ⟨eq_one_of_dvd_one, fun h => h.symm ▸ Nat.dvd_refl _⟩
-
-protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by
-  match Nat.eq_zero_or_pos k with
-  | .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
-  | .inr hpos =>
-    have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
-    rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
-
-protected theorem dvd_of_mul_dvd_mul_left
-    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n := by
-  let ⟨l, H⟩ := H
-  rw [Nat.mul_assoc] at H
-  exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩
-
-protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
-  rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
+protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = c * b := by
+  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
 
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
@@ -773,18 +729,6 @@ theorem pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) : x ^ k ∣ x ^ l ↔
 theorem pow_dvd_pow_iff_le_right' {b k l : Nat} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l :=
   pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl)
 
-protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
-    a = b * c := by
-  rw [← H2, Nat.mul_div_cancel' H1]
-
-protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = b * c :=
-  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
-
-protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = c * b := by
-  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
-
 protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a ^ n := by
   cases Nat.exists_eq_add_of_le h
   case intro k p =>
@@ -836,7 +780,7 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
 
 theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
   | 0 => rfl
-  | k + 1 => by simp [add_succ, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
+  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
 
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with

src/Init/Data/Option/Basic.lean

@@ -37,6 +37,13 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none,   _ => none
   | some a, b => b a
 
+/-- Runs `f` on `o`'s value, if any, and returns its result, or else returns `none`.  -/
+@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
+  if let some a := o then
+    return (← f a)
+  else
+    return none
+
 @[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
   if let some a := o then
     return some (← f a)

src/Init/Data/Ord.lean

@@ -6,6 +6,7 @@ Authors: Dany Fabian, Sebastian Ullrich
 
 prelude
 import Init.Data.String
+import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
@@ -87,11 +88,24 @@ def isGE : Ordering → Bool
 
 end Ordering
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x = y` corresponds to `Ordering.eq`.
+-/
 @[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x == y` corresponds to `Ordering.eq`.
+-/
+@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
+  if x < y then .lt
+  else if x == y then .eq
+  else .gt
+
 /--
 Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
 first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
@@ -105,6 +119,7 @@ class Ord (α : Type u) where
 
 export Ord (compare)
 
+set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compare `x` and `y` by comparing `f x` and `f y`.
 -/
@@ -147,6 +162,13 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
+instance [Ord α] : Ord (Option α) where
+  compare
+  | none,   none   => .eq
+  | none,   some _ => .lt
+  | some _, none   => .gt
+  | some x, some y => compare x y
+
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
@@ -194,7 +216,7 @@ protected def opposite (ord : Ord α) : Ord α where
 /--
 `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
 -/
-protected def on (ord : Ord β) (f : α → β) : Ord α where
+protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -210,4 +232,13 @@ returns 'equal', by `ord₂`.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
+/--
+Creates an order which compares elements of an `Array` in lexicographic order.
+-/
+protected def arrayOrd [a : Ord α] : Ord (Array α) where
+  compare x y :=
+    let _ : LT α := a.toLT
+    let _ : BEq α := a.toBEq
+    compareOfLessAndBEq x.toList y.toList
+
 end Ord

src/Init/Data/Random.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.System.IO
-import Init.Data.Int
 universe u
 
 /-!

src/Init/Data/String/Extra.lean

@@ -62,4 +62,40 @@ namespace Iterator
 
 end Iterator
 
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 end String

src/Init/Ext.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
+import Init.Data.ToString.Macro
 import Init.TacticsExtra
 import Init.RCases
 

src/Init/GetElem.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Util
+
+@[never_extract]
+private def outOfBounds [Inhabited α] : α :=
+  panic! "index out of bounds"
+
+/--
+The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of return
+value `elem` and side conditions `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`.
+
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
+
+The proof side-condition `valid xs i` is automatically dispatched by the
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
+-/
+class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+              (valid : outParam (coll → idx → Prop)) where
+  /--
+  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
+  are proof side conditions to the application, they will be automatically
+  inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent, but here are some
+  important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
+    `default : α` if the index is not valid.
+  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
+    is not valid.
+  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
+    index is valid.
+  -/
+  getElem (xs : coll) (i : idx) (h : valid xs i) : elem
+
+  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
+
+@[inherit_doc getElem]
+syntax:max term noWs "[" withoutPosition(term) "]" : term
+macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
+
+@[inherit_doc getElem]
+syntax term noWs "[" withoutPosition(term) "]'" term:max : term
+macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
+
+/--
+The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
+returns `none` if `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+
+/--
+The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
+panics `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
+
+class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+
+  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+
+export LawfulGetElem (getElem?_def getElem!_def)
+
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
+  rw [getElem?_def]
+  exact dif_pos h
+
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
+  rw [getElem?_def]
+  exact dif_neg h
+
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
+    c[i]! = c[i]'h := by
+  simp only [getElem!_def, getElem?_def, h]
+
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
+  simp only [getElem!_def, getElem?_def, h]
+
+namespace Fin
+
+instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
+  getElem xs i h := getElem xs i.1 h
+  getElem? xs i := getElem? xs i.val
+  getElem! xs i := getElem! xs i.val
+
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
+
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+    a[i] = a[i.1] := rfl
+
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
+
+@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
+
+end Fin
+
+namespace List
+
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
+@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+  rfl
+
+@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+  rfl
+
+theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+  match as, i with
+  | _::_, 0   => rfl
+  | _::_, i+1 => get_drop_eq_drop _ i _
+
+end List
+
+namespace Array
+
+instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
+end Array
+
+namespace Lean.Syntax
+
+instance : GetElem Syntax Nat Syntax fun _ _ => True where
+  getElem stx i _ := stx.getArg i
+
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
+end Lean.Syntax

src/Init/MacroTrace.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Extra notation that depends on Init/Meta
+-/
+
+prelude
+import Init.Data.ToString.Macro
+import Init.Meta
+
+namespace Lean
+
+macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
+  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+
+end Lean

src/Init/Meta.lean

@@ -9,7 +9,6 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
-import Init.Data.String.Extra
 
 namespace Lean
 
@@ -105,43 +104,6 @@ def idBeginEscape := '«'
 def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
-
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 namespace Name
 
 def getRoot : Name → Name
@@ -947,6 +909,11 @@ def _root_.Substring.toName (s : Substring) : Name :=
       else
         Name.mkStr n comp
 
+/--
+Converts a `String` to a hierarchical `Name` after splitting it at the dots.
+
+`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
+-/
 def _root_.String.toName (s : String) : Name :=
   s.toSubstring.toName
 
@@ -1227,14 +1194,6 @@ instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
 
 end Lean.Syntax
 
-set_option linter.unusedVariables.funArgs false in
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the given tactic.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
-
 /-! # Helper functions for manipulating interpolated strings -/
 
 namespace Lean.Syntax

src/Init/NotationExtra.lean

@@ -6,13 +6,12 @@ Authors: Leonardo de Moura
 Extra notation that depends on Init/Meta
 -/
 prelude
-import Init.Meta
+import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
-import Init.Data.ToString
-namespace Lean
+import Init.Conv
+import Init.Meta
 
-macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
-  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+namespace Lean
 
 -- Auxiliary parsers and functions for declaring notation with binders
 
@@ -123,7 +122,7 @@ calc abc
   _ = xyz := pwxyz
 ```
 
-`calc` has term mode and tactic mode variants. This is the term mode variant.
+`calc` works as a term, as a tactic or as a `conv` tactic.
 
 See [Theorem Proving in Lean 4][tpil4] for more information.
 
@@ -131,45 +130,13 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 -/
 syntax (name := calc) "calc" calcSteps : term
 
-/-- Step-wise reasoning over transitive relations.
-```
-calc
-  a = b := pab
-  b = c := pbc
-  ...
-  y = z := pyz
-```
-proves `a = z` from the given step-wise proofs. `=` can be replaced with any
-relation implementing the typeclass `Trans`. Instead of repeating the right-
-hand sides, subsequent left-hand sides can be replaced with `_`.
-```
-calc
-  a = b := pab
-  _ = c := pbc
-  ...
-  _ = z := pyz
-```
-It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
-<proof>`. This is useful for aligning relation symbols:
-```
-calc abc
-  _ = bce := pabce
-  _ = cef := pbcef
-  ...
-  _ = xyz := pwxyz
-```
-
-`calc` has term mode and tactic mode variants. This is the tactic mode variant,
-which supports an additional feature: it works even if the goal is `a = z'`
-for some other `z'`; in this case it will not close the goal but will instead
-leave a subgoal proving `z = z'`.
-
-See [Theorem Proving in Lean 4][tpil4] for more information.
-
-[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
--/
+@[inherit_doc «calc»]
 syntax (name := calcTactic) "calc" calcSteps : tactic
 
+@[inherit_doc «calc»]
+macro tk:"calc" steps:calcSteps : conv =>
+  `(conv| tactic => calc%$tk $steps)
+
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
 
@@ -255,35 +222,35 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
   | _ => throw ()
 
 @[app_unexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"]
+  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++  a.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"]
+  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString ++ "." ++ a8.getString)]
   | _  => throw ()
 
 @[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

src/Init/Omega/Int.lean

@@ -6,7 +6,6 @@ Authors: Scott Morrison
 prelude
 import Init.Data.Int.DivMod
 import Init.Data.Int.Order
-import Init.Data.Nat.Basic
 
 /-!
 # Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.
@@ -51,6 +50,9 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
   simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
+theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
+  Int.ofNat_zero_le _
+
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
@@ -135,11 +137,13 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

src/Init/Omega/IntList.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 prelude
 import Init.Data.List.Lemmas
 import Init.Data.Int.DivModLemmas
-import Init.Data.Int.Gcd
+import Init.Data.Nat.Gcd
 
 namespace Lean.Omega
 

src/Init/Omega/LinearCombo.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.Omega.Coeffs
+import Init.Data.ToString.Macro
 
 /-!
 # Linear combinations

src/Init/Prelude.lean

@@ -488,6 +488,7 @@ attribute [unbox] Prod
 Similar to `Prod`, but `α` and `β` can be propositions.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
+@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α
@@ -509,6 +510,7 @@ structure MProd (α β : Type u) where
 constructed and destructed like a pair: if `ha : a` and `hb : b` then
 `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
 -/
+@[pp_using_anonymous_constructor]
 structure And (a b : Prop) : Prop where
   /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
   intro ::
@@ -575,6 +577,7 @@ a pair-like type, so if you have `x : α` and `h : p x` then
 `⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
 you can also make it explicit using `s.1` or `s.val`.
 -/
+@[pp_using_anonymous_constructor]
 structure Subtype {α : Sort u} (p : α → Prop) where
   /-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
   type. You can also write this as `s.1`, or simply as `s` when the type is
@@ -1194,7 +1197,12 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a / b` computes the result of dividing `a` by `b`.
   The meaning of this notation is type-dependent.
   * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
-  * For `Nat` and `Int`, `a / b` rounds toward 0.
+  * For `Nat`, `a / b` rounds downwards.
+  * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
+    It is implemented as `Int.ediv`, the unique function satisfiying
+    `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
+    Other rounding conventions are available using the functions
+    `Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
   * For `Float`, `a / 0` follows the IEEE 754 semantics for division,
     usually resulting in `inf` or `nan`. -/
   hDiv : α → β → γ
@@ -1206,7 +1214,8 @@ This enables the notation `a % b : γ` where `a : α`, `b : β`.
 class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`.
   The meaning of this notation is type-dependent.
-  * For `Nat` and `Int`, `a % 0` is defined to be `a`. -/
+  * For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
+    and `a % 0` is defined to be `a`. -/
   hMod : α → β → γ
 
 /--
@@ -1485,6 +1494,7 @@ instance [ShiftRight α] : HShiftRight α α α where
   hShiftRight a b := ShiftRight.shiftRight a b
 
 open HAdd (hAdd)
+open HSub (hSub)
 open HMul (hMul)
 open HPow (hPow)
 open HAppend (hAppend)
@@ -1808,6 +1818,7 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
 `Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
 It is the "canonical type with `n` elements".
 -/
+@[pp_using_anonymous_constructor]
 structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
   written as `i.1` or just `i` when the target type is known. -/
@@ -2035,7 +2046,7 @@ instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
 /--
-The size of type `UInt16`, that is, `2^System.Platform.numBits`, which may
+The size of type `USize`, that is, `2^System.Platform.numBits`, which may
 be either `2^32` or `2^64` depending on the platform's architecture.
 
 Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
@@ -2053,7 +2064,7 @@ instance : OfNat (Fin (n+1)) i where
   ofNat := Fin.ofNat i
 ```
 -/
-abbrev USize.size : Nat := Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)
+abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
 
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
@@ -2532,43 +2543,6 @@ def panic {α : Type u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
-/--
-The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
-When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
-of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
-`dom` is whatever proof side conditions are required to make this applicable.
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
-
-The proof side-condition `dom xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
--/
-class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
-  /--
-  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
-  If there are proof side conditions to the application, they will be automatically
-  inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent,
-  but here are some important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
-    does array indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
-    with proof side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
-  * `arr[i]!`: panics if the side goal is false
-  * `arr[i]?`: returns `none` if the side goal is false
-  * `arr[i]'h`: uses `h` to prove the side goal
-  -/
-  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
-
-export GetElem (getElem)
-
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
@@ -2626,9 +2600,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
-instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
-
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.
@@ -2744,7 +2715,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
@@ -3481,20 +3452,31 @@ instance : Hashable String where
 namespace Lean
 
 /--
-Hierarchical names. We use hierarchical names to name declarations and
-for creating unique identifiers for free variables and metavariables.
+Hierarchical names consist of a sequence of components, each of
+which is either a string or numeric, that are written separated by dots (`.`).
 
-You can create hierarchical names using the following quotation notation.
+Hierarchical names are used to name declarations and for creating
+unique identifiers for free variables and metavariables.
+
+You can create hierarchical names using a backtick:
 ```
 `Lean.Meta.whnf
 ```
-It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`
-You can use double quotes to request Lean to statically check whether the name
+It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.
+
+You can use double backticks to request Lean to statically check whether the name
 corresponds to a Lean declaration in scope.
 ```
 ``Lean.Meta.whnf
 ```
 If the name is not in scope, Lean will report an error.
+
+There are two ways to convert a `String` to a `Name`:
+
+ 1. `Name.mkSimple` creates a name with a single string component.
+
+ 2. `String.toName` first splits the string into its dot-separated
+    components, and then creates a hierarchical name.
 -/
 inductive Name where
   /-- The "anonymous" name. -/
@@ -3545,7 +3527,9 @@ abbrev mkNum (p : Name) (v : Nat) : Name :=
   Name.num p v
 
 /--
-Short for `.str .anonymous s`.
+Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.
+
+This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
 -/
 abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
@@ -3883,9 +3867,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
   | Syntax.node _ _ args => args.getD i Syntax.missing
   | _                    => Syntax.missing
 
-instance : GetElem Syntax Nat Syntax fun _ _ => True where
-  getElem stx i _ := stx.getArg i
-
 /-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`. -/
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with
@@ -4580,6 +4561,12 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
 Resolves the given name to an overload list of global definitions.
 The `List String` in each alternative is the deduced list of projections
 (which are ambiguous with name components).
+
+Remark: it will not trigger actions associated with reserved names. Recall that Lean
+has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
+containing stating that `foo` is equal to its definition. The action associated with `foo.def`
+automatically proves the theorem. At the macro level, the name is resolved, but the action is not
+executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n

src/Init/PropLemmas.lean

@@ -21,7 +21,10 @@ set_option linter.missingDocs true -- keep it documented
   | rfl, rfl, _ => rfl
 
 @[simp] theorem eq_true_eq_id : Eq True = id := by
-  funext _; simp only [true_iff, id.def, eq_iff_iff]
+  funext _; simp only [true_iff, id_def, eq_iff_iff]
+
+theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
+  cases propext (iff_of_true hp hq); rfl
 
 /-! ## not -/
 

src/Init/RCases.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro, Jacob von Raumer
 -/
 prelude
 import Init.Tactics
-import Init.NotationExtra
+import Init.Meta
+
 
 /-!
 # Recursive cases (`rcases`) tactic and related tactics
@@ -127,7 +128,7 @@ the input expression). An `rcases` pattern has the following grammar:
   and so on.
 * A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
   while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
+* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
   or a nested disjunction like `a ∨ b ∨ c`.
 
 A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,

src/Init/Simproc.lean

@@ -11,22 +11,23 @@ namespace Lean.Parser
 A user-defined simplification procedure used by the `simp` tactic, and its variants.
 Here is an example.
 ```lean
-simproc reduce_add (_ + _) := fun e => do
-  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
-  let some n ← getNatValue? (e.getArg! 4) | return none
-  let some m ← getNatValue? (e.getArg! 5) | return none
-  return some (.done { expr := mkNatLit (n+m) })
+theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]
+
+open Lean Meta Simp
+simproc ↓ shortCircuitAnd (And _ _) := fun e => do
+  let_expr And p q := e | return .continue
+  let r ← simp p
+  let_expr False := r.expr | return .continue
+  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
+  return .done { expr := r.expr, proof? := some proof }
 ```
-The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The `simp` tactic invokes `shortCircuitAnd` whenever it finds a term of the form `And _ _`.
 The simplification procedures are stored in an (imperfect) discrimination tree.
 The procedure should **not** assume the term `e` perfectly matches the given pattern.
 The body of a simplification procedure must have type `Simproc`, which is an alias for
-`Expr → SimpM (Option Step)`.
+`Expr → SimpM Step`
 You can instruct the simplifier to apply the procedure before its sub-expressions
-have been simplified by using the modifier `↓` before the procedure name. Example.
-```lean
-simproc ↓ reduce_add (_ + _) := fun e => ...
-```
+have been simplified by using the modifier `↓` before the procedure name.
 Simplification procedures can be also scoped or local.
 -/
 syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command

src/Init/System/FilePath.lean

@@ -73,7 +73,21 @@ private def posOfLastSep (p : FilePath) : Option String.Pos :=
   p.toString.revFind pathSeparators.contains
 
 def parent (p : FilePath) : Option FilePath :=
-  FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  if p.isAbsolute then
+    let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
+    if p.toString.length == lengthOfRootDirectory then
+      -- `p` is a root directory
+      none
+    else if posOfLastSep p == String.Pos.mk (lengthOfRootDirectory - 1) then
+      -- `p` is a direct child of the root
+      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
+    else
+      -- `p` is an absolute path with at least two subdirectories
+      extractParentPath
+  else
+    -- `p` is a relative path
+    extractParentPath
 
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with

src/Init/Tactics.lean

@@ -224,7 +224,7 @@ the first matching constructor, or else fails.
 syntax (name := constructor) "constructor" : tactic
 
 /--
-Applies the second constructor when
+Applies the first constructor when
 the goal is an inductive type with exactly two constructors, or fails otherwise.
 ```
 example : True ∨ False := by
@@ -354,6 +354,9 @@ macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
     with_annotate_state $tk skip
     all_goals $y:tactic)
 
+/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
+syntax (name := fail) "fail" (ppSpace str)? : tactic
+
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations. -/
 syntax (name := eqRefl) "eq_refl" : tactic
 
@@ -365,10 +368,23 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| eq_refl)
+macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+-/
+syntax (name := applyRfl) "apply_rfl" : tactic
+
+macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
+
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -899,9 +915,6 @@ example : ∀ x : Nat, x = x := by unhygienic
 -/
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
-/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail" (ppSpace str)? : tactic
-
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
 and if the file is re-elaborated and the input matches, the tactic is not re-run and
@@ -1310,6 +1323,22 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
+/--
+Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
+-/
+syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
+
+/--
+`rw?` tries to find a lemma which can rewrite the goal.
+
+`rw?` should not be left in proofs; it is a search tool, like `apply?`.
+
+Suggestions are printed as `rw [h]` or `rw [← h]`.
+
+You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
+-/
+syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic
+
 /--
 `show_term tac` runs `tac`, then prints the generated term in the form
 "exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
@@ -1493,16 +1522,16 @@ macro "get_elem_tactic" : tactic =>
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )
 
-@[inherit_doc getElem]
-syntax:max term noWs "[" withoutPosition(term) "]" : term
-macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
-
-@[inherit_doc getElem]
-syntax term noWs "[" withoutPosition(term) "]'" term:max : term
-macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
 /--
 Searches environment for definitions or theorems that can be substituted in
 for `exact?% to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
+
+set_option linter.unusedVariables.funArgs false in
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

src/Init/Util.lean

@@ -73,19 +73,6 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
-@[never_extract]
-private def outOfBounds [Inhabited α] : α :=
-  panic! "index out of bounds"
-
-@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
-  if h : _ then getElem xs i h else outOfBounds
-
-@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
-  if h : _ then some (getElem xs i h) else none
-
-macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
-macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
-
 /--
   Marks given value and its object graph closure as multi-threaded if currently
   marked single-threaded. This will make reference counter updates atomic and

src/Init/WF.lean

@@ -45,7 +45,7 @@ def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) :
 section
 variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
 
-theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
+noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
   induction (apply hwf a) with
   | intro x₁ _ ih => exact h x₁ ih
 
@@ -166,13 +166,13 @@ def lt_wfRel : WellFoundedRelation Nat where
       | Or.inl e => subst e; assumption
       | Or.inr e => exact Acc.inv ih e
 
-protected theorem strongInductionOn
+protected noncomputable def strongInductionOn
     {motive : Nat → Sort u}
     (n : Nat)
     (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
   Nat.lt_wfRel.wf.fix ind n
 
-protected theorem caseStrongInductionOn
+protected noncomputable def caseStrongInductionOn
     {motive : Nat → Sort u}
     (a : Nat)
     (zero : motive 0)

src/Lean.lean

@@ -24,6 +24,7 @@ import Lean.Eval
 import Lean.Structure
 import Lean.PrettyPrinter
 import Lean.CoreM
+import Lean.ReservedNameAction
 import Lean.InternalExceptionId
 import Lean.Server
 import Lean.ScopedEnvExtension

src/Lean/AuxRecursor.lean

@@ -34,7 +34,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   || declName == ``Eq.ndrec
   || declName == ``Eq.ndrecOn
 
-def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
+def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
   | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -147,7 +147,7 @@ def callLeanRefcountFn (builder : LLVM.Builder llvmctx)
     (delta : Option (LLVM.Value llvmctx) := Option.none) : M llvmctx Unit := do
   let fnName :=  s!"lean_{kind}{if checkRef? then "" else "_ref"}{if delta.isNone then "" else "_n"}"
   let retty ← LLVM.voidType llvmctx
-  let argtys := if delta.isNone then #[← LLVM.voidPtrType llvmctx] else #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys ← if delta.isNone then pure #[← LLVM.voidPtrType llvmctx] else pure #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   match delta with
@@ -663,7 +663,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
     (name : String := "") : M llvmctx (LLVM.Value llvmctx) :=
   match getExternEntryFor extData `c with
   | some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
-  | some (ExternEntry.inline "llvm" _pat) => throw "Unimplemented codegen of inline LLVM"
+  | some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
   | some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
   | some (ExternEntry.foreign _ extFn)  => emitSimpleExternalCall builder extFn ps ys retty name
   | _ => throw s!"Failed to emit extern application '{f}'."

src/Lean/Compiler/ImplementedByAttr.lean

@@ -17,7 +17,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
   getParam := fun declName stx => do
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
-    let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
+    let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
     let fnDecl ← getConstInfo fnName
     unless decl.levelParams.length == fnDecl.levelParams.length do
       throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"

src/Lean/Compiler/InitAttr.lean

@@ -44,7 +44,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
-        let initFnName ← Elab.resolveGlobalConstNoOverloadWithInfo initFnName
+        let initFnName ← Elab.realizeGlobalConstNoOverloadWithInfo initFnName
         let initDecl ← getConstInfo initFnName
         match getIOTypeArg initDecl.type with
         | none => throwError "initialization function '{initFnName}' must have type of the form `IO <type>`"

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -346,7 +346,7 @@ We call this whenever we enter a new local function. It clears both the
 current join point and the list of candidates since we can't lift join
 points outside of functions as explained in `mergeJpContextIfNecessary`.
 -/
-def withNewFunScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
+def withNewFunScope (x : ExtendM α): ExtendM α := do
   withReader (fun ctx => { ctx with currentJp? := none, candidates := {} }) do
     withNewScope do
       x
@@ -412,7 +412,7 @@ where
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)
     | .fun decl k =>
-      let decl ← withNewFunScope decl do
+      let decl ← withNewFunScope do
         decl.updateValue (← go decl.value)
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -88,7 +88,7 @@ occurring in `decl`.
 -/
 def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
   let nameNew ← mkAuxDeclName
-  let inlineAttr? := if (← read).inheritInlineAttrs then (← read).mainDecl.inlineAttr? else none
+  let inlineAttr? ← if (← read).inheritInlineAttrs then pure (← read).mainDecl.inlineAttr? else pure none
   let auxDecl ← go nameNew (← read).mainDecl.safe inlineAttr? |>.run' {}
   let us := auxDecl.levelParams.map mkLevelParam
   let auxDeclName ← match (← cacheAuxDecl auxDecl) with

src/Lean/CoreM.lean

@@ -219,7 +219,7 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
   unless max == 0 do
     let numHeartbeats ← IO.getNumHeartbeats
     if numHeartbeats - (← read).initHeartbeats > max then
-      throwMaxHeartbeat moduleName optionName max
+      throwMaxHeartbeat (.mkSimple moduleName) optionName max
 
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats

src/Lean/Data/HashMap.lean

@@ -116,6 +116,22 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
       else
         (expand size' buckets', false)
 
+@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
+  match m with
+  | ⟨size, buckets⟩ =>
+    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
+    let bkt    := buckets.val[i]
+    if let some b := bkt.find? a then
+      (m, some b)
+    else
+      let size'    := size + 1
+      let buckets' := buckets.update i (AssocList.cons a b bkt) h
+      if numBucketsForCapacity size' ≤ buckets.val.size then
+        ({ size := size', buckets := buckets' }, none)
+      else
+        (expand size' buckets', none)
+
+
 def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
   match m with
   | ⟨ size, buckets ⟩ =>
@@ -125,9 +141,10 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
     else m
 
 inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
-  | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
-  | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
-  | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
+  | mkWff          : ∀ n,                    WellFormed (mkHashMapImp n)
+  | insertWff      : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
+  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew m a b |>.1)
+  | eraseWff       : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
@@ -156,13 +173,22 @@ def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
     match h:m.insert a b with
     | (m', _) => ⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩
 
-/-- Similar to `insert`, but also returns a Boolean flad indicating whether an existing entry has been replaced with `a -> b`. -/
+/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
 def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
   match m with
   | ⟨ m, hw ⟩ =>
     match h:m.insert a b with
     | (m', replaced) => (⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩, replaced)
 
+/--
+Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
+If the result is `some old`, the the resulting map is equal to `m`. -/
+def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
+  match m with
+  | ⟨ m, hw ⟩ =>
+    match h:m.insertIfNew a b with
+    | (m', old) => (⟨ m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption ⟩, old)
+
 @[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
   match m with
   | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
@@ -186,6 +212,8 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
+instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/Json/Basic.lean

@@ -10,6 +10,8 @@ import Init.Data.Range
 import Init.Data.OfScientific
 import Init.Data.Hashable
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 
 -- mantissa * 10^-exponent

src/Lean/Data/JsonRpc.lean

@@ -183,6 +183,9 @@ structure ResponseError (α : Type u) where
 instance [ToJson α] : CoeOut (ResponseError α) Message :=
   ⟨fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)⟩
 
+instance : CoeOut (ResponseError Unit) Message :=
+  ⟨fun r => Message.responseError r.id r.code r.message none⟩
+
 instance : Coe String RequestID := ⟨RequestID.str⟩
 instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩
 

src/Lean/Data/Lsp/Basic.lean

@@ -52,7 +52,7 @@ instance : LE Range := leOfOrd
 structure Location where
   uri : DocumentUri
   range : Range
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 structure LocationLink where
   originSelectionRange? : Option Range

src/Lean/Data/Lsp/Diagnostics.lean

@@ -25,7 +25,7 @@ open Json
 
 inductive DiagnosticSeverity where
   | error | warning | information | hint
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
@@ -45,7 +45,7 @@ instance : ToJson DiagnosticSeverity := ⟨fun
 inductive DiagnosticCode where
   | int (i : Int)
   | string (s : String)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticCode := ⟨fun
   | num (i : Int) => return DiagnosticCode.int i
@@ -62,7 +62,7 @@ inductive DiagnosticTag where
   | unnecessary
   /-- Deprecated or obsolete code. Rendered with a strike-through. -/
   | deprecated
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
@@ -80,7 +80,7 @@ instance : ToJson DiagnosticTag := ⟨fun
 structure DiagnosticRelatedInformation where
   location : Location
   message : String
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 /-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.
 
@@ -113,6 +113,29 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
+local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
+
+/-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
+private structure DiagnosticWith.UserVisible (α : Type) where
+  range               : Range
+  fullRange?          : Option Range
+  severity?           : Option DiagnosticSeverity
+  code?               : Option DiagnosticCode
+  source?             : Option String
+  message             : α
+  tags?               : Option (Array DiagnosticTag)
+  relatedInformation? : Option (Array DiagnosticRelatedInformation)
+  deriving Ord
+
+/-- Extracts user-visible properties from the given `DiagnosticWith`. -/
+private def DiagnosticWith.UserVisible.ofDiagnostic (d : DiagnosticWith α)
+    : DiagnosticWith.UserVisible α :=
+  { d with }
+
+/-- Compares `DiagnosticWith` instances modulo non-user-facing properties. -/
+def compareByUserVisible [Ord α] (a b : DiagnosticWith α) : Ordering :=
+  compare (DiagnosticWith.UserVisible.ofDiagnostic a) (DiagnosticWith.UserVisible.ofDiagnostic b)
+
 abbrev Diagnostic := DiagnosticWith String
 
 /-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics). -/

src/Lean/Data/Lsp/Internal.lean

@@ -24,44 +24,50 @@ Identifier of a reference.
 -/
 inductive RefIdent where
   /-- Named identifier. These are used in all references that are globally available. -/
-  | const : Name → RefIdent
+  | const (moduleName : Name) (identName : Name) : RefIdent
   /-- Unnamed identifier. These are used for all local references. -/
-  | fvar  : FVarId → RefIdent
+  | fvar (moduleName : Name) (id : FVarId) : RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
-/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
-def toString : RefIdent → String
-  | RefIdent.const n => s!"c:{n}"
-  | RefIdent.fvar id => s!"f:{id.name}"
+instance : ToJson FVarId where
+  toJson id := toJson id.name
 
-/--
-Converts the string representation of a reference identifier back to a reference identifier.
-The string representation must have been created by `RefIdent.toString`.
--/
-def fromString (s : String) : Except String RefIdent := do
-  let sPrefix := s.take 2
-  let sName := s.drop 2
-  -- See `FromJson Name`
-  let name ← match sName with
-    | "[anonymous]" => pure Name.anonymous
-    | _ =>
-      let n := sName.toName
-      if n.isAnonymous then throw s!"expected a Name, got {sName}"
-      else pure n
-  match sPrefix with
-    | "c:" => return RefIdent.const name
-    | "f:" => return RefIdent.fvar <| FVarId.mk name
-    | _ => throw "string must start with 'c:' or 'f:'"
+instance : FromJson FVarId where
+  fromJson? s := return ⟨← fromJson? s⟩
+
+/-- Shortened representation of `RefIdent` for more compact serialization. -/
+inductive RefIdentJsonRepr
+  /-- Shortened representation of `RefIdent.const` for more compact serialization. -/
+  | c (m n : Name)
+  /-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/
+  | f (m : Name) (i : FVarId)
+  deriving FromJson, ToJson
+
+/-- Converts `id` to its compact serialization representation. -/
+def toJsonRepr : (id : RefIdent) → RefIdentJsonRepr
+  | const moduleName identName => .c moduleName identName
+  | fvar moduleName id => .f moduleName id
+
+/-- Converts `repr` to `RefIdent`. -/
+def fromJsonRepr : (repr : RefIdentJsonRepr) → RefIdent
+  | .c m n => const m n
+  | .f m i => fvar m i
+
+/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/
+def fromJson? (s : Json) : Except String RefIdent :=
+  return fromJsonRepr (← Lean.FromJson.fromJson? s)
+
+/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/
+def toJson (id : RefIdent) : Json :=
+  Lean.ToJson.toJson <| toJsonRepr id
 
 instance : FromJson RefIdent where
-  fromJson?
-    | (s : String) => fromString s
-    | j => Except.error s!"expected a String, got {j}"
+  fromJson? := fromJson?
 
 instance : ToJson RefIdent where
-  toJson ident := toString ident
+  toJson := toJson
 
 end RefIdent
 
@@ -84,6 +90,7 @@ structure RefInfo.Location where
   range       : Lsp.Range
   /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
   parentDecl? : Option RefInfo.ParentDecl
+deriving Inhabited
 
 /-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
 structure RefInfo where
@@ -146,17 +153,18 @@ instance : FromJson RefInfo where
 def ModuleRefs := HashMap RefIdent RefInfo
 
 instance : ToJson ModuleRefs where
-  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
+  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
 
 instance : FromJson ModuleRefs where
   fromJson? j := do
     let node ← j.getObj?
     node.foldM (init := HashMap.empty) fun m k v =>
-      return m.insert (← RefIdent.fromString k) (← fromJson? v)
+      return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
-/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
-
-Contains the file's definitions and references. -/
+/--
+Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
+Contains the definitions and references of the file managed by a worker.
+-/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
@@ -164,4 +172,22 @@ structure LeanIleanInfoParams where
   references : ModuleRefs
   deriving FromJson, ToJson
 
+/--
+Used in the `$/lean/importClosure` watchdog <- worker notification.
+Contains the full import closure of the file managed by a worker.
+-/
+structure LeanImportClosureParams where
+  /-- Full import closure of the file. -/
+  importClosure : Array DocumentUri
+  deriving FromJson, ToJson
+
+/--
+Used in the `$/lean/importClosure` watchdog -> worker notification.
+Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
+-/
+structure LeanStaleDependencyParams where
+  /-- The dependency that is stale. -/
+  staleDependency : DocumentUri
+  deriving FromJson, ToJson
+
 end Lean.Lsp

src/Lean/Data/Lsp/Ipc.lean

@@ -64,9 +64,10 @@ def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request
   (←stdout).readLspRequestAs expectedMethod α
 
 /--
-  Reads response, discarding notifications in between. This function is meant
-  purely for testing where we use `collectDiagnostics` explicitly if we do care
-  about such notifications. -/
+Reads response, discarding notifications and server-to-client requests in between.
+This function is meant purely for testing where we use `collectDiagnostics` explicitly
+if we do care about such notifications.
+-/
 partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     IpcM (Response α) := do
   let m ← (←stdout).readLspMessage
@@ -79,20 +80,28 @@ partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     else
       throw $ userError s!"Expected id {expectedID}, got id {id}"
   | .notification .. => readResponseAs expectedID α
-  | _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
+  | .request .. => readResponseAs expectedID α
+  | .responseError .. => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
 
 def waitForExit : IpcM UInt32 := do
   (←read).wait
 
-/-- Waits for the worker to emit all diagnostics for the current document version
-and returns them as a list. -/
+/--
+Waits for the worker to emit all diagnostic notifications for the current document version and
+returns the last notification, if any.
+
+We used to return all notifications but with debouncing in the server, this would not be
+deterministic anymore as what messages are dropped depends on wall-clock timing.
+ -/
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
-: IpcM (List (Notification PublishDiagnosticsParams)) := do
+: IpcM (Option (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
+  loop
+where
+  loop := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then return []
+      if id == waitForDiagnosticsId then return none
       else loop
     | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
@@ -100,10 +109,9 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
       else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
+      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", diagnosticParam⟩
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
     | _ => loop
-  loop
 
 def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do
   let proc ← Process.spawn {

src/Lean/Data/Lsp/TextSync.lean

@@ -38,7 +38,7 @@ structure DidOpenTextDocumentParams where
 
 structure TextDocumentChangeRegistrationOptions where
   documentSelector? : Option DocumentSelector := none
-  syncKind : TextDocumentSyncKind
+  syncKind          : TextDocumentSyncKind
   deriving FromJson
 
 inductive TextDocumentContentChangeEvent where
@@ -61,13 +61,18 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
     | TextDocumentContentChangeEvent.fullChange text => [⟨"text", toJson text⟩]⟩
 
 structure DidChangeTextDocumentParams where
-  textDocument : VersionedTextDocumentIdentifier
+  textDocument   : VersionedTextDocumentIdentifier
   contentChanges : Array TextDocumentContentChangeEvent
   deriving ToJson, FromJson
 
+structure DidSaveTextDocumentParams where
+  textDocument : TextDocumentIdentifier
+  text?        : Option String
+  deriving ToJson, FromJson
+
 -- TODO: missing:
 -- WillSaveTextDocumentParams, TextDocumentSaveReason,
--- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
+-- TextDocumentSaveRegistrationOptions
 
 structure SaveOptions where
   includeText : Bool
@@ -81,11 +86,11 @@ structure DidCloseTextDocumentParams where
 
 /-- NOTE: This is defined twice in the spec. The latter version has more fields. -/
 structure TextDocumentSyncOptions where
-  openClose : Bool
-  change : TextDocumentSyncKind
-  willSave : Bool
+  openClose         : Bool
+  change            : TextDocumentSyncKind
+  willSave          : Bool
   willSaveWaitUntil : Bool
-  save? : Option SaveOptions := none
+  save?             : Option SaveOptions
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Lsp/Window.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marc Huisinga
+-/
+prelude
+import Lean.Data.Json
+
+open Lean
+
+inductive MessageType where
+  | error
+  | warning
+  | info
+  | log
+
+instance : FromJson MessageType where
+  fromJson?
+    | (1 : Nat) => .ok .error
+    | (2 : Nat) => .ok .warning
+    | (3 : Nat) => .ok .info
+    | (4 : Nat) => .ok .log
+    | _         => .error "Unknown MessageType ID"
+
+instance : ToJson MessageType where
+  toJson
+    | .error   => 1
+    | .warning => 2
+    | .info    => 3
+    | .log     => 4
+
+structure ShowMessageParams where
+  type    : MessageType
+  message : String
+  deriving FromJson, ToJson
+
+structure MessageActionItem where
+  title : String
+  deriving FromJson, ToJson
+
+structure ShowMessageRequestParams where
+  type     : MessageType
+  message  : String
+  actions? : Option (Array MessageActionItem)
+  deriving FromJson, ToJson
+
+def ShowMessageResponse := Option MessageActionItem
+  deriving FromJson, ToJson

src/Lean/Data/Name.lean

@@ -7,8 +7,6 @@ prelude
 import Init.Data.Ord
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 namespace Name
 -- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
 @[export lean_name_hash_exported] def hashEx : Name → UInt64 :=

src/Lean/Data/NameMap.lean

@@ -11,8 +11,6 @@ import Lean.Data.SSet
 import Lean.Data.Name
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 def NameMap (α : Type) := RBMap Name α Name.quickCmp
 
 @[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp

src/Lean/Data/Parsec.lean

@@ -5,7 +5,7 @@ Author: Dany Fabian
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 
 namespace Lean
 
@@ -43,11 +43,19 @@ def fail (msg : String) : Parsec α := fun it =>
   error it msg
 
 @[inline]
-def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α := fun it =>
+def tryCatch (p : Parsec α)
+    (csuccess : α → Parsec β)
+    (cerror : Unit → Parsec β)
+    : Parsec β := fun it =>
   match p it with
-  | success rem a => success rem a
-  | error rem err =>
-    if it = rem then q () it else error rem err
+  | .success rem a => csuccess a rem
+  | .error rem err =>
+    -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
+    if it.pos = rem.pos then cerror () rem else .error rem err
+
+@[inline]
+def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α :=
+  tryCatch p pure q
 
 @[inline]
 def attempt (p : Parsec α) : Parsec α := λ it =>
@@ -74,8 +82,7 @@ def eof : Parsec Unit := fun it =>
 
 @[specialize]
 partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
-  (do manyCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
@@ -85,8 +92,7 @@ def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
 
 @[specialize]
 partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
-  (do manyCharsCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""

src/Lean/Data/PersistentArray.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
+import Init.Data.ToString.Macro
 
 universe u v w
 
@@ -71,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.BasicAux
+import Init.Data.ToString.Macro
 
 namespace Lean
 universe u v w w'
@@ -154,6 +155,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
@@ -226,8 +229,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let ⟨keys', keq⟩ := keys.eraseIdx' idx
-      let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)
@@ -320,6 +325,9 @@ def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α}
 def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps
 
+def toArray {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : Array (α × β) :=
+  m.foldl (init := #[]) fun ps k v => ps.push (k, v)
+
 structure Stats where
   numNodes      : Nat := 0
   numNull       : Nat := 0

src/Lean/Data/Position.lean

@@ -38,9 +38,6 @@ structure FileMap where
   The first entry is always `0` and the last always the index of the last character.
   In particular, if the last character is a newline, that index will appear twice. -/
   positions : Array String.Pos
-  /-- The line numbers associated with the `positions`.
-  Has the same length as `positions` and is always of the form `#[1, 2, …, n-1, n-1]`. -/
-  lines     : Array Nat
   deriving Inhabited
 
 class MonadFileMap (m : Type → Type) where
@@ -50,40 +47,50 @@ export MonadFileMap (getFileMap)
 
 namespace FileMap
 
+/-- The last line should always be `positions.size - 1`. -/
+def getLastLine (fmap : FileMap) : Nat :=
+  fmap.positions.size - 1
+
+/-- The line numbers associated with the `positions` of the `FileMap`.
+`fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]`
+where `n` is the `size` of `positions`. -/
+def getLine (fmap : FileMap) (x : Nat) : Nat :=
+  min (x + 1) fmap.getLastLine
+
 partial def ofString (s : String) : FileMap :=
-  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap :=
-    if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }
+  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) : FileMap :=
+    if s.atEnd i then { source := s, positions := ps.push i }
     else
       let c := s.get i
       let i := s.next i
-      if c == '\n' then loop i (line+1) (ps.push i) (lines.push (line+1))
-      else loop i line ps lines
-  loop 0 1 (#[0]) (#[1])
+      if c == '\n' then loop i (line+1) (ps.push i)
+      else loop i line ps
+  loop 0 1 (#[0])
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
-  | { source := str, positions := ps, lines := lines } =>
+  | { source := str, positions := ps } =>
     if ps.size >= 2 && pos <= ps.back then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
       let rec loop (b e : Nat) :=
         let posB := ps[b]!
-        if e == b + 1 then { line := lines.get! b, column := toColumn posB 0 }
+        if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }
         else
           let m := (b + e) / 2;
           let posM := ps.get! m;
-          if pos == posM then { line := lines.get! m, column := 0 }
+          if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
       loop 0 (ps.size -1)
-    else if lines.isEmpty then
+    else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨lines.back, (pos - ps.back).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=

src/Lean/Data/Rat.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 import Init.Data.Int.DivMod
 import Init.Data.Nat.Gcd
 namespace Lean

src/Lean/Data/Xml/Basic.lean

@@ -5,6 +5,8 @@ Author: Dany Fabian
 -/
 prelude
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 namespace Xml
 

src/Lean/DeclarationRange.lean

@@ -48,14 +48,14 @@ def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : Declaratio
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   return declRangeExt.find? (← getEnv) declName
 
-def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
+def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv
   let ranges ← if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
     findDeclarationRangesCore? declName.getPrefix
   else
     findDeclarationRangesCore? declName
   match ranges with
-  | none => return (← builtinDeclRanges.get (m := IO)).find? declName
+  | none => return (← builtinDeclRanges.get (m := BaseIO)).find? declName
   | some _ => return ranges
 
 end Lean

src/Lean/DocString.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.DeclarationRange
 import Lean.MonadEnv
+import Init.Data.String.Extra
 
 namespace Lean
 
@@ -13,12 +14,14 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
-def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
-  modifyEnv fun env => docStringExt.insert env declName (removeLeadingSpaces docString)
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
-def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with
   | some docString => addDocString declName docString
   | none => return ()

src/Lean/Elab/App.lean

@@ -1035,7 +1035,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName _ _ =>
-      let fullName := `Function ++ fieldName
+      let fullName := Name.str `Function fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
@@ -1060,9 +1060,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
+      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
         return LValResolution.const baseStructName structName fullName
-      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
+      else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
         return LValResolution.const structName' structName' fullName
       else
         throwLValError e eType
@@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   if baseName == `Function then
     return (← whnfR type).isForall
-  else if type.consumeMData.isAppOf baseName then
+  else if type.cleanupAnnotations.isAppOf baseName then
     return true
   else
     return (← whnfR type).isAppOf baseName
@@ -1199,8 +1199,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   let rec loop : Expr → List LVal → TermElabM Expr
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
-    if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
-      addDotCompletionInfo targetStx f expectedType? fieldStx
+    if let LVal.fieldName (fullRef := fullRef) .. := lval then
+      addDotCompletionInfo fullRef f expectedType?
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1340,7 +1340,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     let elabFieldName (e field : Syntax) := do
       let newLVals := field.identComponents.map fun comp =>
         -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none e
+        LVal.fieldName comp comp.getId.getString! none f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
       let some idx := idxStx.isFieldIdx? | throwError "invalid field index"

src/Lean/Elab/BuiltinCommand.lean

@@ -55,7 +55,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
 
 private def checkAnonymousScope : List Scope → Option Name
   | { header := "", .. } :: _ => none
-  | { header := h, .. }  :: _ => some h
+  | { header := h, .. }  :: _ => some <| .mkSimple h
   | _                         => some .anonymous -- should not happen
 
 private def checkEndHeader : Name → List Scope → Option Name
@@ -64,7 +64,7 @@ private def checkEndHeader : Name → List Scope → Option Name
     if h == s then
       (.str · s) <$> checkEndHeader p scopes
     else
-      some h
+      some <| .mkSimple h
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
@@ -536,7 +536,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
     -- show signature for `#check id`/`#check @id`
     if let `($id:ident) := term then
       try
-        for c in (← resolveGlobalConstWithInfos term) do
+        for c in (← realizeGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -749,7 +749,7 @@ def elabRunMeta : CommandElab := fun stx =>
     pure ()
 
 @[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
+  let options ← Elab.elabSetOption stx[1] stx[3]
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
@@ -760,7 +760,7 @@ def elabRunMeta : CommandElab := fun stx =>
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
-    let declName ← resolveGlobalConstNoOverloadWithInfo id
+    let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
       throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then

src/Lean/Elab/BuiltinTerm.lean

@@ -223,7 +223,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
 
 @[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
-  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
+  return toExpr (← realizeGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?
@@ -232,7 +232,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
   let id := stx[2].getId
-  let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
+  let id ← if stx[1].isNone then pure id else pure <| (← getCurrNamespace) ++ id
   let e := stx[3]
   withMacroExpansion stx e <| withDeclName id <| elabTerm e expectedType?
 
@@ -312,9 +312,9 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     popScope
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
+  let options ← Elab.elabSetOption stx[1] stx[3]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[4] expectedType?
+    elabTerm stx[5] expectedType?
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with