fix: fold raw Nat literals at dsimp

closes #2916

Remark: this PR also renames `Expr.natLit?` ==> `Expr.rawNatLit?`.
Motivation: consistent naming convention: `Expr.isRawNatLit`.

.github/workflows/ci.yml

@@ -98,8 +98,7 @@ 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,
@@ -107,7 +106,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",
@@ -141,10 +140,12 @@ jobs:
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
-                "CTEST_OPTIONS": "--repeat until-pass:2",
+                // also, the liasolver test hits “too many exported symbols”
+                "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
                 "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"
+                // TEMP while compiler tests are deactivated
+                "binary-check": "true"
               },
               {
                 "name": "Linux aarch64",
@@ -446,10 +447,9 @@ jobs:
     name: Build matrix complete
     runs-on: ubuntu-latest
     needs: build
-    # mark as merely cancelled not failed if builds are cancelled
-    if: ${{ !cancelled() }}
+    if: ${{ always() }}
     steps:
-    - if: contains(needs.*.result, 'failure')
+    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
       uses: actions/github-script@v7
       with:
         script: |

.github/workflows/pr-release.yml

@@ -126,19 +126,21 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            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 "$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")"
+
             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."

CODEOWNERS

@@ -13,7 +13,6 @@
 /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,16 +11,6 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
-* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
-
-  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).
-
 * New command `derive_functinal_induction`:
 
   Derived from the definition of a (possibly mutually) recursive function
@@ -41,46 +31,6 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
-* The termination checker now recognizes more recursion patterns without an
-  explicit `terminatin_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`.
-
-
-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
--/
-```
-
 v4.7.0
 ---------
 

doc/dev/ffi.md

@@ -111,15 +111,6 @@ 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.

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 -DLEAN_EXPORTING"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
     '';
   };
   mkMod = mod: deps:

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 ${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")
+  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")
 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 ${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")
+  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")
 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/Conv.lean

@@ -156,6 +156,7 @@ 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
 

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,
@@ -737,16 +737,13 @@ theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a ==
 section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
-/-- 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 :=
+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 :=
   h.rec m
 
-/-- `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 :=
+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 :=
   h.rec m
 
-/-- `HEq.ndrec` variant -/
-noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
+theorem 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 :=

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
 
-noncomputable def List.two_step_induction
+theorem List.two_step_induction
   {motive : List Nat → Sort u}
   (l : List Nat)
   (empty : motive [])

src/Init/Data/Array/Basic.lean

@@ -727,38 +727,33 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     termination_by as.size - i
   go 0 #[]
 
-/-- 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'
+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'
   else
     a.pop
-termination_by a.size - i.val
+termination_by a.size - i
 
-derive_functional_induction feraseIdx
+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 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 h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
+  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
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
@@ -814,7 +809,7 @@ where
     rfl
 
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+    cases i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, go]
 
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/BitVec/Basic.lean

@@ -73,9 +73,6 @@ 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

src/Init/Data/BitVec/Lemmas.lean

@@ -29,6 +29,8 @@ 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) :
@@ -70,7 +72,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]
+      simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
       exact i_lt
     have q_lt : w - 1 - i < w := by
       simp only [Nat.sub_sub]
@@ -456,12 +458,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 (isLt _)]
+    rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
     · cases w : decide (i < v)
       · simp at w
         simp [w]
         rw [Nat.testBit_lt_two_pow]
-        calc BitVec.toNat x < 2 ^ v := isLt _
+        calc BitVec.toNat x < 2 ^ v := toNat_lt _
           _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
       · simp
 
@@ -518,7 +520,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 x.isLt (Nat.two_pow_pos _)
+    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
   · omega
 
 @[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :

src/Init/Data/Bool.lean

@@ -431,17 +431,12 @@ theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite
 @[simp] theorem cond_self (c : Bool) (t : α) : cond c t t = t := by cases c <;> rfl
 
 /-
-This is a simp rule in Mathlib, but results in non-confluence that is difficult
-to fix as decide distributes over propositions. As an example, observe that
-`cond (decide (p ∧ q)) t f` could simplify to either:
+This is a simp rule in Mathlib, but results in non-confluence that is
+difficult to fix as decide distributes over propositions.
 
-* `if p ∧ q then t else f` via `Bool.cond_decide` or
-* `cond (decide p && decide q) t f` via `Bool.decide_and`.
-
-A possible approach to improve normalization between `cond` and `ite` would be
-to completely simplify away `cond` by making `cond_eq_ite` a `simp` rule, but
-that has not been taken since it could surprise users to migrate pure `Bool`
-operations like `cond` to a mix of `Prop` and `Bool`.
+A possible fix would be to completely simplify away `cond`, but that
+is not taken since it could result in major rewriting of code that is
+otherwise purely about `Bool`.
 -/
 theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
     cond (decide p) t e = if p then t else e := by

src/Init/Data/Channel.lean

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

src/Init/Data/Int.lean

@@ -11,4 +11,3 @@ 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,12 +160,6 @@ 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,12 +6,7 @@ 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 -/
@@ -19,37 +14,4 @@ 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

@@ -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', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
+    simp [subNatNat_of_lt h', succ_pred_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,11 +169,12 @@ 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 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]
+    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')]
 
 protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
   | (m:Nat), (n:Nat), c => aux1 ..
@@ -187,15 +188,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 [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
+    simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
 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
+    simp [add_succ]
     rw [Int.add_comm, subNatNat_add_negSucc]
-    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
+    simp [add_succ, succ_add, Nat.add_comm]
 
 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]
@@ -390,7 +391,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 [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
+      rw [succ_pred_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
@@ -405,7 +406,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 [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
+    simp [succ_pred_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)
@@ -421,12 +422,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 [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
+  | (m:Nat), -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
   | -[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 [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
+  | -[m+1],  -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
 
 protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
   simp [Int.mul_comm, Int.mul_add]
@@ -498,6 +499,33 @@ 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 -/
 
 /-!
@@ -517,4 +545,10 @@ 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

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Lemmas
 import Init.ByCases
-import Init.RCases
 
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
@@ -499,524 +498,3 @@ 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
-  · rintro i n rfl
-    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

@@ -1,44 +0,0 @@
-/-
-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/Basic.lean

@@ -458,7 +458,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 []

src/Init/Data/Nat.lean

@@ -17,5 +17,3 @@ 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,29 +10,6 @@ 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`
@@ -148,12 +125,9 @@ theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
 theorem add_one (n : Nat) : n + 1 = succ n :=
   rfl
 
-@[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
+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
@@ -235,9 +209,6 @@ 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
@@ -286,7 +257,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 only [Nat.add_succ, Nat.sub_succ, ih]
+  | succ c ih => simp [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
@@ -635,6 +606,8 @@ 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 :=
@@ -743,11 +716,6 @@ 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
@@ -770,7 +738,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_sub_self_left]; decide
+    | Or.inl h => injection h with h; subst h; rw [←Nat.add_one, 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 _ _)
@@ -784,7 +752,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 only [Nat.sub_zero, ne_eq, not_false_eq_true]
+  | 0, succ b, _ => by simp
   | 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)
 
@@ -802,7 +770,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 [← Nat.add_assoc, ih]
+  | succ k ih => simp [add_succ, add_succ, succ_sub_succ, 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]
@@ -915,7 +883,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.add_succ, Nat.sub_succ, ih]
+  | succ k ih => rw [Nat.add_succ, Nat.sub_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 [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]
+  | k + 1 => by simp [add_succ, shiftRight_add, 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,7 +6,6 @@ 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

@@ -1,57 +0,0 @@
-/-
-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,13 +10,6 @@ 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
 
@@ -35,7 +28,7 @@ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 e
   rw [Nat.div]
   rfl
 
-def div.inductionOn.{u}
+theorem 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)
@@ -102,7 +95,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]
 
-def mod.inductionOn.{u}
+theorem 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)
@@ -205,11 +198,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 only [add_one, succ_mul, false_iff, Nat.not_le]
-    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
+    simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
+    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
     exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
   | ind y k h IH =>
-    rw [Nat.add_le_add_iff_right, IH k0, succ_mul,
+    rw [← add_one, 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
@@ -293,7 +286,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 [Nat.pred_succ, mul_succ, Nat.sub_sub]
+      simp [add_one, 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
@@ -334,50 +327,4 @@ 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,10 +5,17 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
-import Init.Meta
+import Init.TacticsExtra
 
 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⟩
@@ -97,36 +104,4 @@ 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,12 +1,10 @@
 /-
 Copyright (c) 2021 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
+Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Dvd
-import Init.NotationExtra
-import Init.RCases
 
 namespace Nat
 
@@ -16,8 +14,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
@@ -71,166 +69,4 @@ 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

@@ -1,66 +0,0 @@
-/-
-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,6 +19,7 @@ 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
@@ -334,32 +335,6 @@ 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 ..)
@@ -408,6 +383,10 @@ 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 ..⟩
@@ -505,6 +484,51 @@ 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
@@ -695,17 +719,37 @@ theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
 
 /-! ### dvd -/
 
-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]
+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 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 {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_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 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
 
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
@@ -729,6 +773,18 @@ 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 =>
@@ -780,7 +836,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 [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
+  | k + 1 => by simp [add_succ, 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,13 +37,6 @@ 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/Random.lean

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

src/Init/NotationExtra.lean

@@ -9,7 +9,6 @@ prelude
 import Init.Meta
 import Init.Data.Array.Subarray
 import Init.Data.ToString
-import Init.Conv
 namespace Lean
 
 macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
@@ -124,7 +123,7 @@ calc abc
   _ = xyz := pwxyz
 ```
 
-`calc` works as a term, as a tactic or as a `conv` tactic.
+`calc` has term mode and tactic mode variants. This is the term mode variant.
 
 See [Theorem Proving in Lean 4][tpil4] for more information.
 
@@ -132,12 +131,44 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 -/
 syntax (name := calc) "calc" calcSteps : term
 
-@[inherit_doc «calc»]
-syntax (name := calcTactic) "calc" calcSteps : tactic
+/-- 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
+```
 
-@[inherit_doc «calc»]
-macro tk:"calc" steps:calcSteps : conv =>
-  `(conv| tactic => calc%$tk $steps)
+`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
+-/
+syntax (name := calcTactic) "calc" calcSteps : tactic
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())

src/Init/Omega/Int.lean

@@ -6,6 +6,7 @@ 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`.

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.Nat.Gcd
+import Init.Data.Int.Gcd
 
 namespace Lean.Omega
 

src/Init/Prelude.lean

@@ -1485,7 +1485,6 @@ 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)
@@ -2036,7 +2035,7 @@ instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
 /--
-The size of type `USize`, that is, `2^System.Platform.numBits`, which may
+The size of type `UInt16`, 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
@@ -2054,7 +2053,7 @@ instance : OfNat (Fin (n+1)) i where
   ofNat := Fin.ofNat i
 ```
 -/
-abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
+abbrev USize.size : Nat := Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 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
@@ -4581,12 +4580,6 @@ 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,10 +21,7 @@ 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]
-
-theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
-  cases propext (iff_of_true hp hq); rfl
+  funext _; simp only [true_iff, id.def, eq_iff_iff]
 
 /-! ## not -/
 

src/Init/Tactics.lean

@@ -369,14 +369,6 @@ macro "rfl" : tactic => `(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, 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).

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)
 
-noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
+theorem 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 noncomputable def strongInductionOn
+protected theorem 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 noncomputable def caseStrongInductionOn
+protected theorem caseStrongInductionOn
     {motive : Nat → Sort u}
     (a : Nat)
     (zero : motive 0)

src/Lean.lean

@@ -24,7 +24,6 @@ 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/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.realizeGlobalConstNoOverloadWithInfo fnNameStx
+    let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo 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.realizeGlobalConstNoOverloadWithInfo initFnName
+        let initFnName ← Elab.resolveGlobalConstNoOverloadWithInfo 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/Data/HashMap.lean

@@ -116,22 +116,6 @@ 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 ⟩ =>
@@ -141,10 +125,9 @@ 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)
-  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew 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)
+  | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
@@ -173,22 +156,13 @@ 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 flag indicating whether an existing entry has been replaced with `a -> b`. -/
+/-- Similar to `insert`, but also returns a Boolean flad 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 ⟩

src/Lean/Data/JsonRpc.lean

@@ -183,9 +183,6 @@ 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/Internal.lean

@@ -24,50 +24,44 @@ Identifier of a reference.
 -/
 inductive RefIdent where
   /-- Named identifier. These are used in all references that are globally available. -/
-  | const (moduleName : Name) (identName : Name) : RefIdent
+  | const : Name → RefIdent
   /-- Unnamed identifier. These are used for all local references. -/
-  | fvar (moduleName : Name) (id : FVarId) : RefIdent
+  | fvar  : FVarId → RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
-instance : ToJson FVarId where
-  toJson id := toJson id.name
+/-- 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 : 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
+/--
+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 RefIdent where
-  fromJson? := fromJson?
+  fromJson?
+    | (s : String) => fromString s
+    | j => Except.error s!"expected a String, got {j}"
 
 instance : ToJson RefIdent where
-  toJson := toJson
+  toJson ident := toString ident
 
 end RefIdent
 
@@ -90,7 +84,6 @@ 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
@@ -153,13 +146,13 @@ instance : FromJson RefInfo where
 def ModuleRefs := HashMap RefIdent RefInfo
 
 instance : ToJson ModuleRefs where
-  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
+  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, 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.fromJson? (← Json.parse k)) (← fromJson? v)
+      return m.insert (← RefIdent.fromString k) (← fromJson? v)
 
 /-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
 

src/Lean/Data/Lsp/Ipc.lean

@@ -64,10 +64,9 @@ def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request
   (←stdout).readLspRequestAs expectedMethod α
 
 /--
-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.
--/
+  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. -/
 partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     IpcM (Response α) := do
   let m ← (←stdout).readLspMessage
@@ -80,28 +79,20 @@ partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     else
       throw $ userError s!"Expected id {expectedID}, got id {id}"
   | .notification .. => readResponseAs expectedID α
-  | .request .. => readResponseAs expectedID α
-  | .responseError .. => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
+  | _ => 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 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.
- -/
+/-- Waits for the worker to emit all diagnostics for the current document version
+and returns them as a list. -/
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
-: IpcM (Option (Notification PublishDiagnosticsParams)) := do
+: IpcM (List (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  loop
-where
-  loop := do
+  let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then return none
+      if id == waitForDiagnosticsId then return []
       else loop
     | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
@@ -109,9 +100,10 @@ where
       else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", diagnosticParam⟩
+      | Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
       | 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/Window.lean

@@ -1,48 +0,0 @@
-/-
-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/PersistentHashMap.lean

@@ -226,10 +226,8 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      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)
+      let ⟨keys', keq⟩ := keys.eraseIdx' idx
+      let ⟨vals', veq⟩ := vals.eraseIdx' (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)

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 BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
+def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO 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 := BaseIO)).find? declName
+  | none => return (← builtinDeclRanges.get (m := IO)).find? declName
   | some _ => return ranges
 
 end Lean

src/Lean/Elab/BuiltinCommand.lean

@@ -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 (← realizeGlobalConstWithInfos term) do
+        for c in (← resolveGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -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 ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
+    let declName ← resolveGlobalConstNoOverloadWithInfo 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 (← realizeGlobalConstNoOverloadWithInfo stx[2])
+  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?

src/Lean/Elab/Command.lean

@@ -141,8 +141,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
-    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
+    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap (.joinSep traceMsg.toList "\n") .information pos endPos
   return log
 
 private def addTraceAsMessages : CommandElabM Unit := do
@@ -269,6 +268,11 @@ instance : MonadRecDepth CommandElabM where
   getRecDepth      := return (← read).currRecDepth
   getMaxRecDepth   := return (← get).maxRecDepth
 
+register_builtin_option showPartialSyntaxErrors : Bool := {
+  defValue := false
+  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
+}
+
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
@@ -317,6 +321,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages
     let mut msgs := (← get).messages
+    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
+    if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
+      -- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
+      msgs := ⟨msgs.msgs.filter fun msg =>
+        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder || tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
     modify fun st => { st with

src/Lean/Elab/DeclModifiers.lean

@@ -27,8 +27,6 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{declName}' has already been declared"
     | some declName => throwError "private declaration '{declName}' has already been declared"
-  if isReservedName env declName then
-    throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
     throwError "a private declaration '{declName}' has already been declared"

src/Lean/Elab/Declaration.lean

@@ -42,7 +42,7 @@ private def isNamedDef (stx : Syntax) : Bool :=
     let decl := stx[1]
     let k := decl.getKind
     k == ``Lean.Parser.Command.abbrev ||
-    k == ``Lean.Parser.Command.definition ||
+    k == ``Lean.Parser.Command.def ||
     k == ``Lean.Parser.Command.theorem ||
     k == ``Lean.Parser.Command.opaque ||
     k == ``Lean.Parser.Command.axiom ||
@@ -166,7 +166,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  let classes ← getOptDerivingClasses decl[6]
   return {
     ref             := decl
     shortDeclName   := name
@@ -354,7 +354,7 @@ def elabMutual : CommandElab := fun stx => do
     -/
     let declNames ←
        try
-         realizeGlobalConst ident
+         resolveGlobalConst ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then

src/Lean/Elab/DefView.lean

@@ -142,7 +142,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
   declKind == ``Parser.Command.abbrev ||
-  declKind == ``Parser.Command.definition ||
+  declKind == ``Parser.Command.def ||
   declKind == ``Parser.Command.theorem ||
   declKind == ``Parser.Command.opaque ||
   declKind == ``Parser.Command.instance ||
@@ -152,7 +152,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
   let declKind := stx.getKind
   if declKind == ``Parser.Command.«abbrev» then
     return mkDefViewOfAbbrev modifiers stx
-  else if declKind == ``Parser.Command.definition then
+  else if declKind == ``Parser.Command.def then
     return mkDefViewOfDef modifiers stx
   else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx

src/Lean/Elab/Deriving/Basic.lean

@@ -100,10 +100,10 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
-     let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
+     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
+         let className ← resolveGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,12 +118,12 @@ structure DerivingClassView where
   className : Name
   args? : Option (TSyntax ``Parser.Term.structInst)
 
-def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
+def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
   match optDeriving with
   | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
     let mut ret := #[]
     for cls in classes, args? in argss? do
-      let className ← realizeGlobalConstNoOverloadWithInfo cls
+      let className ← resolveGlobalConstNoOverloadWithInfo cls
       ret := ret.push { ref := cls, className := className, args? }
     return ret
   | _ => return #[]

src/Lean/Elab/Frontend.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Language.Lean
+import Lean.Elab.Import
+import Lean.Elab.Command
 import Lean.Util.Profile
 import Lean.Server.References
 
@@ -39,19 +40,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
 
 def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
   runCommandElabM do
-    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     Command.elabCommandTopLevel stx
-    let mut msgs := (← get).messages
-    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check
-    -- in general
-    if !Language.Lean.showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors &&
-        stx.hasMissing then
-      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
-      -- parse error
-      msgs := ⟨msgs.msgs.filter fun msg =>
-        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
-          tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
-    modify ({ · with messages := initMsgs ++ msgs })
 
 def updateCmdPos : FrontendM Unit := do
   modify fun s => { s with cmdPos := s.parserState.pos }
@@ -97,8 +86,12 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   pure (s.commandState.env, s.commandState.messages)
 
 builtin_initialize
+  registerOption `printMessageEndPos { defValue := false, descr := "print end position of each message in addition to start position" }
   registerTraceClass `Elab.info
 
+def getPrintMessageEndPos (opts : Options) : Bool :=
+  opts.getBool `printMessageEndPos false
+
 @[export lean_run_frontend]
 def runFrontend
     (input : String)
@@ -109,50 +102,26 @@ def runFrontend
     (ileanFileName? : Option String := none)
     : IO (Environment × Bool) := do
   let inputCtx := Parser.mkInputContext input fileName
-  -- TODO: replace with `#lang` processing
-  if /- Lean #lang? -/ true then
-    -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-    -- overhead of passing the environment between snapshots until we actually make good use of it
-    -- outside the server
-    let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    -- allow `env` to be leaked, which would live until the end of the process anyway
-    let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-    let env := env.setMainModule mainModuleName
-    let mut commandState := Command.mkState env messages opts
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  -- allow `env` to be leaked, which would live until the end of the process anyway
+  let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
+  let env := env.setMainModule mainModuleName
+  let mut commandState := Command.mkState env messages opts
 
-    if ileanFileName?.isSome then
-      -- Collect InfoTrees so we can later extract and export their info to the ilean file
-      commandState := { commandState with infoState.enabled := true }
+  if ileanFileName?.isSome then
+    -- Collect InfoTrees so we can later extract and export their info to the ilean file
+    commandState := { commandState with infoState.enabled := true }
 
-    let s ← IO.processCommands inputCtx parserState commandState
-    for msg in s.commandState.messages.toList do
-      IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
+  let s ← IO.processCommands inputCtx parserState commandState
+  for msg in s.commandState.messages.toList do
+    IO.print (← msg.toString (includeEndPos := getPrintMessageEndPos opts))
 
-    if let some ileanFileName := ileanFileName? then
-      let trees := s.commandState.infoState.trees.toArray
-      let references ←
-        Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
-      let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
-      IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
-
-    return (s.commandState.env, !s.commandState.messages.hasErrors)
-
-  let ctx := { inputCtx with mainModuleName, opts, trustLevel }
-  let processor := Language.Lean.process
-  let snap ← processor none ctx
-  let snaps := Language.toSnapshotTree snap
-  snaps.runAndReport opts
   if let some ileanFileName := ileanFileName? then
-    let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
+    let trees := s.commandState.infoState.trees.toArray
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
 
-  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
-  -- TODO: remove default when reworking cmdline interface in Lean; currently the only case
-  -- where we use the environment despite errors in the file is `--stats`
-  let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
-  pure (env, !hasErrors)
-
+  pure (s.commandState.env, !s.commandState.messages.hasErrors)
 
 end Lean.Elab

src/Lean/Elab/GenInjective.lean

@@ -10,8 +10,8 @@ import Lean.Meta.Injective
 namespace Lean.Elab.Command
 
 @[builtin_command_elab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do
+  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
-    let declName ← realizeGlobalConstNoOverloadWithInfo stx[1]
     Meta.mkInjectiveTheorems declName
 
 end Lean.Elab.Command

src/Lean/Elab/GuardMsgs.lean

@@ -73,28 +73,9 @@ structure GuardMsgFailure where
   res : String
 deriving TypeName
 
-/--
-Makes trailing whitespace visible and protectes them against trimming by the editor, by appending
-the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid
-ambiguities in the case the message already had that symbol).
--/
-def revealTrailingWhitespace (s : String) : String :=
-  s.replace "⏎\n" "⏎⏎\n" |>.replace "\t\n" "\t⏎\n" |>.replace " \n" " ⏎\n"
-
-/- The inverse of `revealTrailingWhitespace` -/
-def removeTrailingWhitespaceMarker (s : String) : String :=
-  s.replace "⏎\n" "\n"
-
-/--
-Strings are compared up to newlines, to allow users to break long lines.
--/
-def equalUpToNewlines (exp res : String) : Bool :=
-  exp.replace "\n" " " == res.replace "\n" " "
-
 @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
   | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
-    let expected : String := (← dc?.mapM (getDocStringText ·)).getD ""
-        |>.trim |> removeTrailingWhitespaceMarker
+    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
     let specFn ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     elabCommandTopLevel cmd
@@ -107,7 +88,8 @@ def equalUpToNewlines (exp res : String) : Bool :=
       | .drop        => pure ()
       | .passthrough => toPassthrough := toPassthrough.add msg
     let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    if equalUpToNewlines expected res then
+    -- We do some whitespace normalization here to allow users to break long lines.
+    if expected.replace "\n" " " == res.replace "\n" " " then
       -- Passed. Only put toPassthrough messages back on the message log
       modify fun st => { st with messages := initMsgs ++ toPassthrough }
     else
@@ -137,7 +119,6 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
     lazy? := some do
       let some start := stx.getPos? true | return eager
       let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
-      let res := revealTrailingWhitespace res
       let newText := if res.isEmpty then
         ""
       else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?

src/Lean/Elab/InfoTree/Main.lean

@@ -6,7 +6,6 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Meta.PPGoal
-import Lean.ReservedNameAction
 
 namespace Lean.Elab.CommandContextInfo
 
@@ -95,18 +94,16 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa
     | none      => hole id
     | some tree => substitute tree assignment
 
-/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
-def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
+def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
+  let x := x.run { lctx := lctx } { mctx := info.mctx }
   /-
     We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
     have been used in `lctx` and `info.mctx`.
   -/
-  (·.1) <$>
+  let ((a, _), _) ←
     x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
            { env := info.env, ngen := info.ngen }
-
-def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-  (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
+  return a
 
 def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext :=
   { env  := info.env, mctx := info.mctx, lctx := lctx,
@@ -282,28 +279,31 @@ def addConstInfo [MonadEnv m] [MonadError m]
     expectedType?
   }
 
-/-- This does the same job as `realizeGlobalConstNoOverload`; resolving an identifier
+/-- This does the same job as `resolveGlobalConstNoOverload`; resolving an identifier
 syntax to a unique fully resolved name or throwing if there are ambiguities.
 But also adds this resolved name to the infotree. This means that when you hover
 over a name in the sourcefile you will see the fully resolved name in the hover info.-/
-def realizeGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
-  let n ← realizeGlobalConstNoOverload id
+def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
+  let n ← resolveGlobalConstNoOverload id
   if (← getInfoState).enabled then
     -- we do not store a specific elaborator since identifiers are special-cased by the server anyway
     addConstInfo id n expectedType?
   return n
 
-/-- Similar to `realizeGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
-def realizeGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
-  let ns ← realizeGlobalConst id
+/-- Similar to `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
+def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
+  let ns ← resolveGlobalConst id
   if (← getInfoState).enabled then
     for n in ns do
       addConstInfo id n expectedType?
   return ns
 
-/-- Similar to `realizeGlobalName`, but it also adds the resolved name to the info tree. -/
-def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
-  let ns ← realizeGlobalName id
+/-- Similar to `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
+def resolveGlobalNameWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (ref : Syntax) (id : Name) : m (List (Name × List String)) := do
+  let ns ← resolveGlobalName id
   if (← getInfoState).enabled then
     for (n, _) in ns do
       addConstInfo ref n

src/Lean/Elab/InheritDoc.lean

@@ -20,7 +20,7 @@ builtin_initialize
       | `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
-        let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
+        let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
         if (← findDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findDocString? (← getEnv) declName

src/Lean/Elab/MutualDef.lean

@@ -68,6 +68,8 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
     throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
   if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
     throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
+  if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then
+    throwError "'noncomputable unsafe' is not allowed"
   if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
     throwError "'noncomputable partial' is not allowed"
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
@@ -644,9 +646,6 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
     let termination := termination.rememberExtraParams header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
-    if header.kind.isTheorem then
-      unless (← isProp type) do
-        throwErrorAt header.ref "type of theorem '{header.declName}' is not a proposition{indentExpr type}"
     return preDefs.push {
       ref         := getDeclarationSelectionRef header.ref
       kind        := header.kind
@@ -660,14 +659,10 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
   letRecClosures.foldlM (init := preDefs) fun preDefs c => do
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
+    -- Convert any proof let recs inside a `def` to `theorem` kind
     let kind ← if kind.isDefOrAbbrevOrOpaque then
-      -- Convert any proof let recs inside a `def` to `theorem` kind
       withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind
-    else if kind.isTheorem then
-      -- Convert any non-proof let recs inside a `theorem` to `def` kind
-      withLCtx c.toLift.lctx c.toLift.localInstances do
-        return if (← inferType c.toLift.type).isProp then .theorem else .def
     else
       pure kind
     return preDefs.push {
@@ -833,7 +828,7 @@ where
     for header in headers, view in views do
       if let some classNamesStx := view.deriving? then
         for classNameStx in classNamesStx do
-          let className ← realizeGlobalConstNoOverload classNameStx
+          let className ← resolveGlobalConstNoOverload classNameStx
           withRef classNameStx do
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -317,6 +317,14 @@ def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCo
 def tryContradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.contradictionCore { genDiseq := true }
 
+structure UnfoldEqnExtState where
+  map : PHashMap Name Name := {}
+  deriving Inhabited
+
+/- We generate the unfold equation on demand, and do not save them on .olean files. -/
+builtin_initialize unfoldEqnExt : EnvExtension UnfoldEqnExtState ←
+  registerEnvExtension (pure {})
+
 /--
   Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.
   `mvarId` is the goal to be proved. It is a goal of the form
@@ -362,8 +370,9 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
+  let env ← getEnv
   withOptions (tactic.hygienic.set · false) do
-    let baseName := declName
+    let baseName := mkPrivateName env declName
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -371,7 +380,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := baseName ++ `def
+      let name := baseName ++ `_unfold
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
@@ -379,8 +388,13 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       return name
 
 def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
-  if let some info := getInfo? () then
-    return some (← mkUnfoldEq declName info)
+  let env ← getEnv
+  if let some eq := unfoldEqnExt.getState env |>.map.find? declName then
+    return some eq
+  else if let some info := getInfo? () then
+    let eq ← mkUnfoldEq declName info
+    modifyEnv fun env => unfoldEqnExt.modifyState env fun s => { s with map := s.map.insert declName eq }
+    return some eq
   else
     return none
 

src/Lean/Elab/PreDefinition/Main.lean

@@ -105,7 +105,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       See issue #2321
       -/
       let preDef ← eraseRecAppSyntax preDefs[0]!
-      ensureEqnReservedNamesAvailable preDef.declName
       if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -63,12 +63,12 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes #[info.declName] goal.mvarId!
-  let baseName := info.declName
+  let baseName := mkPrivateName (← getEnv) info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
@@ -81,7 +81,6 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
-  ensureEqnReservedNamesAvailable preDef.declName
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -8,7 +8,6 @@ import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
-import Lean.Meta.ArgsPacker.Basic
 
 namespace Lean.Elab.WF
 open Meta
@@ -18,7 +17,6 @@ structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
   fixedPrefixSize : Nat
-  argsPacker      : ArgsPacker
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -109,7 +107,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
-  let baseName := declName
+  let baseName := mkPrivateName (← getEnv) declName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -119,7 +117,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
@@ -131,9 +129,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) : MetaM Unit := do
-  preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
   /-
   See issue #2327.
   Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
@@ -144,8 +140,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       let declNames := preDefs.map (·.declName)
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
-          eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
+          eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -8,12 +8,12 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Cleanup
-import Lean.Meta.ArgsPacker
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 namespace Lean.Elab.WF
@@ -172,28 +172,26 @@ know which function is making the call.
 The close coupling with how arguments are packed and termination goals look like is not great,
 but it works for now.
 -/
-def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
+def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
   let mut r := mkArray numFuncs #[]
   for goal in goals do
-    let type ← goal.getType
-    let (.mdata _ (.app _ param)) := type
-        | throwError "MVar does not look like a recursive call:{indentExpr type}"
-    let (funidx, _) ← argsPacker.unpack param
+    let (.mdata _ (.app _ param)) ← goal.getType
+        | throwError "MVar does not look like like a recursive call"
+    let (funidx, _) ← unpackMutualArg numFuncs param
     r := r.modify funidx (·.push goal)
   return r
 
-def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
+def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
   let goals ← assignSubsumed goals
-  let goalss ← groupGoalsByFunction argsPacker decrTactics.size goals
+  let goalss ← groupGoalsByFunction decrTactics.size goals
   for goals in goalss, decrTactic? in decrTactics do
     Lean.Elab.Term.TermElabM.run' do
     match decrTactic? with
     | none => do
       for goal in goals do
-        let type ← goal.getType
         let some ref := getRecAppSyntax? (← goal.getType)
-          | throwError "MVar not annotated as a recursive call:{indentExpr type}"
+          | throwError "MVar does not look like like a recursive call"
         withRef ref <| applyDefaultDecrTactic goal
     | some decrTactic => withRef decrTactic.ref do
       unless goals.isEmpty do -- unlikely to be empty
@@ -207,8 +205,8 @@ def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option
           Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
-def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
-    (wfRel : Expr) (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
+def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
+    (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
@@ -231,7 +229,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsP
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do
         processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
-      let val ← solveDecreasingGoals argsPacker decrTactics val
+      let val ← solveDecreasingGoals decrTactics val
       mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -9,20 +9,19 @@ import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.TryThis
-import Lean.Meta.ArgsPacker
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 
 /-!
 This module finds lexicographic termination arguments for well-founded recursion.
 
-Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
-(e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
+Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations
 until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
 if given, or the default `decreasing_tactic`.
 
@@ -60,10 +59,6 @@ The following optimizations are applied to make this feasible:
 The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”
 by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5
 <https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf>.
-
-We got the idea of considering the measure `e₂ - e₁` if we see `e₁ < e₂` from
-“Termination Analysis with Calling Context Graphs” by Panagiotis Manolios &
-Daron Vroon, https://doi.org/10.1007/11817963_36.
 -/
 
 set_option autoImplicit false
@@ -89,11 +84,11 @@ def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
   lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
 /--
-Given the original parameter names from `originalVarNames`, find
+Given the original paramter names from `originalVarNames`, remove the fixed prefix and find
 good variable names to be used when talking about termination arguments:
 Use user-given parameter names if present; use x1...xn otherwise.
 
-The names ought to accessible (no macro scopes) and fresh wrt to the current environment,
+The names ought to accessible (no macro scopes) and new names  fresh wrt to the current environment,
 so that with `showInferredTerminationBy` we can print them to the user reliably.
 We do that by appending `'` as needed.
 
@@ -102,7 +97,8 @@ shadow each other, and the guessed relation refers to the wrong one. In that
 case, the user gets to keep both pieces (and may have to rename variables).
 -/
 partial
-def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
+def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do
+  let xs := xs.extract fixedPrefixSize xs.size
   let mut ns : Array Name := #[]
   for h : i in [:xs.size] do
     let n := xs[i]
@@ -119,77 +115,6 @@ def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
       else
         freshen ns (n.appendAfter "'")
 
-/-- A termination measure with extra fields for use within GuessLex -/
-structure Measure extends TerminationArgument where
-  /--
-  Like `.fn`, but unconditionally with `sizeOf` at the right type.
-  We use this one when in `evalRecCall`
-  -/
-  natFn : Expr
-deriving Inhabited
-
-/-- String desription of this measure -/
-def Measure.toString (measure : Measure) : MetaM String := do
-  lambdaTelescope measure.fn fun xs e => do
-    let e ← mkLambdaFVars xs[measure.arity:] e -- undo overshooting
-    return (← ppExpr e).pretty
-
-/--
-Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.
-
-For non-mutual definitions, we omit `sizeOf` when the argument does not depend on
-the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.
-
-For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of
-type `Nat` (else we'd have to worry about differently-typed measures from different functions to
-line up).
--/
-def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool := do
-  let t ← inferType x
-  if is_mutual
-  then
-    withReducible (isDefEq t (.const `Nat []))
-  else
-    try
-      if t.hasAnyFVar (fun fvar => args.contains (.fvar fvar)) then
-        pure false
-      else
-        let u ← getLevel t
-        let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
-        let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
-        isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi)
-    catch _ =>
-      pure false
-
-/-- Sets the user names for the given freevars in `xs`. -/
-def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
-  let mut lctx ←  getLCtx
-  for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
-  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
-
-/-- Create one measure for each (eligible) parameter of the given predefintion.  -/
-def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-    (userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := do
-  let is_mutual : Bool := preDefs.size > 1
-  preDefs.mapIdxM fun funIdx preDef => do
-    lambdaTelescope preDef.value fun xs _ => do
-      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
-        let mut ret : Array Measure := #[]
-        for x in xs[fixedPrefixSize:] do
-          -- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
-          -- `Type`), then ignore this parameter
-          let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
-          if sizeOf.isLit then continue
-
-          let natFn ← mkLambdaFVars xs (← mkAppM ``sizeOf #[x])
-          -- Determine if we need to exclude `sizeOf` in the measure we show/pass on.
-          let fn ←
-            if  ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
-            then mkLambdaFVars xs x
-            else pure natFn
-          let extraParams := preDef.termination.extraParams
-          ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams }
-        return ret
 
 /-- Internal monad used by `withRecApps` -/
 abbrev M (recFnName : Name) (α β : Type) : Type :=
@@ -300,11 +225,11 @@ structure RecCallWithContext where
   ref : Syntax
   /-- Function index of caller -/
   caller : Nat
-  /-- Parameters of caller (including fixed prefix) -/
+  /-- Parameters of caller -/
   params : Array Expr
   /-- Function index of callee -/
   callee : Nat
-  /-- Arguments to callee (including fixed prefix) -/
+  /-- Arguments to callee -/
   args : Array Expr
   ctxt : SavedLocalContext
 
@@ -336,72 +261,25 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
           return (false, true)
     return (true, true)
 
-/--
-Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
+/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
 call site.
 -/
-def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do
+def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat)
+    : MetaM (Array RecCallWithContext) := withoutModifyingState do
   addAsAxiom unaryPreDef
   lambdaTelescope unaryPreDef.value fun xs body => do
     unless xs.size == fixedPrefixSize + 1 do
       -- Maybe cleaner to have lambdaBoundedTelescope?
       throwError "Unexpected number of lambdas in unary pre-definition"
-    let ys := xs[:fixedPrefixSize]
     let param := xs[fixedPrefixSize]!
     withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
       unless args.size ≥ fixedPrefixSize + 1 do
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let (caller, params) ← argsPacker.unpack param
-      let (callee, args) ← argsPacker.unpack arg
-      RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
-
-/-- Is the expression a `<`-like comparison of `Nat` expressions -/
-def isNatCmp (e : Expr) : Option (Expr × Expr) :=
-  match_expr e with
-  | LT.lt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
-  | LE.le α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
-  | GT.gt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
-  | GE.ge α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
-  | _ => none
-
-def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-    (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
-    MetaM (Array (Array Measure)) := do
-  preDefs.mapIdxM fun funIdx preDef => do
-    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
-    let mut measures := #[]
-    for rc in recCalls do
-      -- Only look at calls from the current function
-      unless rc.caller = funIdx do continue
-      -- Only look at calls where the parameters have not been refined
-      unless rc.params.all (·.isFVar) do continue
-      let xs := rc.params.map (·.fvarId!)
-      let varyingParams : Array FVarId := xs[fixedPrefixSize:]
-      measures ← rc.ctxt.run do
-        withUserNames rc.params[fixedPrefixSize:] userVarNamess[funIdx]! do
-        trace[Elab.definition.wf] "rc: {rc.caller} ({rc.params}) → {rc.callee} ({rc.args})"
-        let mut measures := measures
-        for ldecl in ← getLCtx do
-          if let some (e₁, e₂) := isNatCmp ldecl.type then
-            -- We only want to consider these expressions if they depend only on the function's
-            -- immediate arguments, so check that
-            if e₁.hasAnyFVar (! xs.contains ·) then continue
-            if e₂.hasAnyFVar (! xs.contains ·) then continue
-            -- If e₁ does not depend on any varying parameters, simply ignore it
-            let e₁_is_const := ! e₁.hasAnyFVar (varyingParams.contains ·)
-            let body := if e₁_is_const then e₂ else mkNatSub e₂ e₁
-            -- Avoid adding simple measures
-            unless body.isFVar do
-              let fn ← mkLambdaFVars rc.params body
-              -- Avoid duplicates
-              unless ← measures.anyM (isDefEq ·.fn fn) do
-                let extraParams := preDef.termination.extraParams
-                measures := measures.push { ref := .missing, fn, natFn := fn, arity, extraParams }
-        return measures
-    return measures
+      let (caller, params) ← unpackArg arities param
+      let (callee, args) ← unpackArg arities arg
+      RecCallWithContext.create (← getRef) caller params callee args
 
 /-- A `GuessLexRel` described how a recursive call affects a measure; whether it
 decreases strictly, non-strictly, is equal, or else.  -/
@@ -424,18 +302,27 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr
   | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
   | no_idea => unreachable!
 
+/-- Given an expression `e`, produce `sizeOf e` with a suitable instance. -/
+def mkSizeOf (e : Expr) : MetaM Expr := do
+  let ty ← inferType e
+  let lvl ← getLevel ty
+  let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty])
+  let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty,  inst, e]
+  check res
+  return res
+
 /--
 For a given recursive call, and a choice of parameter and argument index,
 try to prove equality, < or ≤.
 -/
-def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure)
-  (rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
+def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
+    MetaM GuessLexRel := do
   rcc.ctxt.run do
-    let callerMeasure := callerMeasures[callerMeasureIdx]!
-    let calleeMeasure := calleeMeasures[calleeMeasureIdx]!
-    let param := callerMeasure.natFn.beta rcc.params
-    let arg := calleeMeasure.natFn.beta rcc.args
+    let param := rcc.params[paramIdx]!
+    let arg := rcc.args[argIdx]!
     trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})"
+    let arg ← mkSizeOf rcc.args[argIdx]!
+    let param ← mkSizeOf rcc.params[paramIdx]!
     for rel in [GuessLexRel.eq, .lt, .le] do
       let goalExpr := mkAppN rel.toNatRel #[arg, param]
       trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}"
@@ -468,35 +355,32 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasur
 /- A cache for `evalRecCall` -/
 structure RecCallCache where mk'' ::
   decrTactic? : Option DecreasingBy
-  callerMeasures : Array Measure
-  calleeMeasures : Array Measure
   rcc : RecCallWithContext
   cache : IO.Ref (Array (Array (Option GuessLexRel)))
 
 /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
-def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure))
+def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
     (rcc : RecCallWithContext) :
     BaseIO RecCallCache := do
   let decrTactic? := decrTactics[rcc.caller]!
-  let callerMeasures := measuress[rcc.caller]!
-  let calleeMeasures := measuress[rcc.callee]!
-  let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
-  return { decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
+  let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
+  return { decrTactic?, rcc, cache }
 
 /-- Run `evalRecCall` and cache there result -/
-def RecCallCache.eval (rc: RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
+def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
   -- Check the cache first
-  if let Option.some res := (← rc.cache.get)[callerMeasureIdx]![calleeMeasureIdx]! then
+  if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then
     return res
   else
-    let res ← evalRecCall rc.decrTactic? rc.callerMeasures rc.calleeMeasures rc.rcc callerMeasureIdx calleeMeasureIdx
-    rc.cache.modify (·.modify callerMeasureIdx (·.set! calleeMeasureIdx res))
+    let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx
+    rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
     return res
 
+
 /-- Print a single cache entry as a string, without forcing it -/
-def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM String := do
+def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
   let cachedEntries ← rcc.cache.get
-  return match cachedEntries[callerMeasureIdx]![calleeMeasureIdx]! with
+  return match cachedEntries[paramIdx]![argIdx]! with
   | .some rel => toString rel
   | .none => "_"
 
@@ -510,10 +394,10 @@ inductive MutualMeasure where
 
 /-- Evaluate a recursive call at a given `MutualMeasure` -/
 def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
-  | .args taIdxs => do
-    let callerMeasureIdx := taIdxs[rc.rcc.caller]!
-    let calleeMeasureIdx := taIdxs[rc.rcc.callee]!
-    rc.eval callerMeasureIdx calleeMeasureIdx
+  | .args argIdxs => do
+    let paramIdx := argIdxs[rc.rcc.caller]!
+    let argIdx := argIdxs[rc.rcc.callee]!
+    rc.eval paramIdx argIdx
   | .func funIdx => do
     if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
       return .lt
@@ -522,29 +406,56 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
     else
       return .eq
 
+/--
+Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`,
+where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
+This is the case for types such as `Prop`, `Type u`, etc.
+These arguments should not be considered when guessing a well-founded relation.
+See `generateCombinations?`
+-/
+def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
+  lambdaTelescope preDef.value fun xs _ => do
+    let mut result := #[]
+    for x in xs[fixedPrefixSize:], i in [:xs.size] do
+      try
+        let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
+        if sizeOf.isLit then
+         result := result.push i
+      catch _ =>
+        result := result.push i
+    return result
+
 
 /--
-Generate all combination of measures. Assumes we have numbered the measures of each function,
-and their counts is in `numMeasures`.
+Generate all combination of arguments, skipping those that are forbidden.
 
-This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
+Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
 try first, when the mutually recursive functions have similar argument structures
 -/
-partial def generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) :
-    Option (Array (Array Nat)) :=
+partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat)
+    (threshold : Nat := 32) : Option (Array (Array Nat)) :=
   (do goUniform 0; go 0 #[]) |>.run #[] |>.2
 where
+  isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
+    if h : fidx < forbiddenArgs.size then
+       forbiddenArgs[fidx] |>.contains argIdx
+    else
+      false
+
   -- Enumerate all permissible uniform combinations
-  goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
-    if numMeasures.all (idx < ·) then
-      modify (·.push (Array.mkArray numMeasures.size idx))
-      goUniform (idx + 1)
+  goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
+    if numArgs.all (argIdx < ·) then
+      unless forbiddenArgs.any (·.contains argIdx) do
+        modify (·.push (Array.mkArray numArgs.size argIdx))
+      goUniform (argIdx + 1)
 
   -- Enumerate all other permissible combinations
   go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
-    if h : fidx < numMeasures.size then
-      let n := numMeasures[fidx]
-      for idx in [:n] do withReader (·.push idx) (go (fidx + 1))
+    if h : fidx < numArgs.size then
+      let n := numArgs[fidx]
+      for argIdx in [:n] do
+        unless isForbidden fidx argIdx do
+          withReader (·.push argIdx) (go (fidx + 1))
     else
       let comb ← read
       unless comb.all (· == comb[0]!) do
@@ -552,19 +463,19 @@ where
       if (← get).size > threshold then
         failure
 
-/--
-Enumerate all meausures we want to try.
 
-All arguments (resp. combinations thereof) and
+/--
+Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and
 possible orderings of functions (if more than one)
 -/
-def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do
-  let some arg_measures := generateCombinations? numTermArgs
+def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) :
+    MetaM (Array MutualMeasure) := do
+  let some arg_measures := generateCombinations? forbiddenArgs arities
       | throwError "Too many combinations"
 
   let func_measures :=
-    if numTermArgs.size > 1 then
-      (List.range numTermArgs.size).toArray
+    if arities.size > 1 then
+      (List.range arities.size).toArray
     else
       #[]
 
@@ -609,6 +520,58 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
     -- None found, we have to give up
     return .none
 
+/--
+Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
+-/
+def mkTupleSyntax : Array Term → MetaM Term
+  | #[]  => `(())
+  | #[e] => return e
+  | es   => `(($(es[0]!), $(es[1:]),*))
+
+/--
+Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
+combination of these measures. The parameters are
+
+* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
+  the fixed prefix.  Used to determine if we need to fully qualify `sizeOf`.
+* `varNamess`: For each function in the clique, the parameter names to be used in the
+  termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
+* `measures`: The measures to be used.
+-/
+def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
+  (measures : Array MutualMeasure) : MetaM TerminationWF := do
+  varNamess.mapIdxM fun funIdx varNames => do
+    let idents := varNames.map mkIdent
+    let measureStxs ← measures.mapM fun
+      | .args varIdxs => do
+          let varIdx := varIdxs[funIdx]!
+          let v := idents[varIdx]!
+          -- Print `sizeOf` as such, unless it is shadowed.
+          -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
+          -- But it could also be shadowed by an earlier parameter (including the fixed prefix),
+          -- so look for unqualified (single tick) occurrences in `originalVarNames`
+          let sizeOfIdent :=
+            if originalVarNamess[funIdx]!.any (· = `sizeOf) then
+              mkIdent ``sizeOf -- fully qualified
+            else
+              mkIdent (← unresolveNameGlobal ``sizeOf)
+          `($sizeOfIdent $v)
+      | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
+    let body ← mkTupleSyntax measureStxs
+    return { ref := .missing, vars := idents, body, synthetic := true }
+
+/--
+The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
+syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
+syntax with more information, or valid syntax with (possibly) unresolved variable names?
+The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
+we do that.
+-/
+def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
+  elems.mapIdx fun funIdx elem => { elem with
+    vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size]
+    synthetic := false }
+
 /--
 Given a matrix (row-major) of strings, arranges them in tabular form.
 First column is left-aligned, others right-aligned.
@@ -653,43 +616,21 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
   return s!"{position.line}:{position.column}{endPosStr}"
 
 
-/-- How to present the measure in the table header, possibly abbreviated. -/
-def measureHeader (measure : Measure) : StateT (Nat × String) MetaM String := do
-  let s ← measure.toString
-  if s.length > 5 then
-    let (i, footer) ← get
-    let i := i + 1
-    let footer := footer ++ s!"#{i}: {s}\n"
-    set (i, footer)
-    pure s!"#{i}"
-  else
-    pure s
-
-def collectHeaders {α} (a : StateT (Nat × String) MetaM α) : MetaM (α × String) := do
-  let (x, (_, footer)) ← a.run (0, "")
-  pure (x,footer)
-
-
 /-- Explain what we found out about the recursive calls (non-mutual case) -/
-def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do
-  let (header, footer) ← collectHeaders (measures.mapM measureHeader)
+def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
+  let header := varNames.map (·.eraseMacroScopes.toString)
   let mut table : Array (Array String) := #[#[""] ++ header]
   for i in [:rcs.size], rc in rcs do
     let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
-    for argIdx in [:measures.size] do
+    for argIdx in [:varNames.size] do
       row := row.push (← rc.prettyEntry argIdx argIdx)
     table := table.push row
-  let out := formatTable table
-  if footer.isEmpty then
-    return out
-  else
-    return out ++ "\n\n" ++ footer
+
+  return formatTable table
 
 /-- Explain what we found out about the recursive calls (mutual case) -/
-def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure))
+def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
     (rcs : Array RecCallCache) : MetaM Format := do
-  let (headerss, footer) ← collectHeaders (measuress.mapM (·.mapM measureHeader))
-
   let mut r := Format.nil
 
   for rc in rcs do
@@ -698,74 +639,40 @@ def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Meas
     r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
       f!"at {← rc.rcc.posString}:\n"
 
-    let mut table : Array (Array String) := #[#[""] ++ headerss[caller]!]
+    let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
+    let mut table : Array (Array String) := #[#[""] ++ header]
     if caller = callee then
       -- For self-calls, only the diagonal is interesting, so put it into one row
       let mut row := #[""]
-      for argIdx in [:measuress[caller]!.size] do
+      for argIdx in [:varNamess[caller]!.size] do
         row := row.push (← rc.prettyEntry argIdx argIdx)
       table := table.push row
     else
-      for argIdx in [:measuress[callee]!.size] do
+      for argIdx in [:varNamess[callee]!.size] do
         let mut row := #[]
-        row := row.push headerss[callee]![argIdx]!
-        for paramIdx in [:measuress[caller]!.size] do
+        row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
+        for paramIdx in [:varNamess[caller]!.size] do
           row := row.push (← rc.prettyEntry paramIdx argIdx)
         table := table.push row
     r := r ++ formatTable table ++ "\n"
 
-  unless footer.isEmpty do
-    r := r ++ "\n\n" ++ footer
-
   return r
 
-def explainFailure (declNames : Array Name) (measuress : Array (Array Measure))
+def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
     (rcs : Array RecCallCache) : MetaM Format := do
   let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
     "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
   if declNames.size = 1 then
-    r := r ++ (← explainNonMutualFailure measuress[0]! rcs)
+    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
   else
-    r := r ++ (← explainMutualFailure declNames measuress rcs)
+    r := r ++ (← explainMutualFailure declNames varNamess rcs)
   return r
 
-/--
-For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
--/
-def mkProdElem (xs : Array Expr) : MetaM Expr := do
-  match xs.size with
-  | 0 => return default
-  | 1 => return xs[0]!
-  | _ =>
-    let n := xs.size
-    xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
+end Lean.Elab.WF.GuessLex
 
-def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-    (userVarNamess : Array (Array Name)) (measuress : Array (Array Measure))
-    (solution : Array MutualMeasure) : MetaM TerminationArguments := do
-  preDefs.mapIdxM fun funIdx preDef => do
-    let measures := measuress[funIdx]!
-    lambdaTelescope preDef.value fun xs _ => do
-      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
-        let args := solution.map fun
-          | .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
-          | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
-        let fn ← mkLambdaFVars xs (← mkProdElem args)
-        let extraParams := preDef.termination.extraParams
-        return { ref := .missing, arity := xs.size, extraParams, fn}
+namespace Lean.Elab.WF
 
-/--
-Shows the inferred termination argument to the user, and implements `termination_by?`
--/
-def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
-  for preDef in preDefs, termArg in termArgs do
-    if showInferredTerminationBy.get (← getOptions) then
-      logInfoAt preDef.ref m!"Inferred termination argument:\n{← termArg.delab}"
-    if let some ref := preDef.termination.terminationBy?? then
-      Tactic.TryThis.addSuggestion ref (← termArg.delab)
-
-end GuessLex
-open GuessLex
+open Lean.Elab.WF.GuessLex
 
 /--
 Main entry point of this module:
@@ -774,41 +681,45 @@ Try to find a lexicographic ordering of the arguments for which the recursive de
 terminates. See the module doc string for a high-level overview.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
-    (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
-    MetaM TerminationArguments := do
-  let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
-  trace[Elab.definition.wf] "varNames is: {userVarNamess}"
+    (fixedPrefixSize : Nat) :
+    MetaM TerminationWF := do
+  let extraParamss := preDefs.map (·.termination.extraParams)
+  let originalVarNamess ← preDefs.mapM originalVarNames
+  let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·)
+  let arities := varNamess.map (·.size)
+  trace[Elab.definition.wf] "varNames is: {varNamess}"
 
-  -- Collect all recursive calls and extract their context
-  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker
-  let recCalls := filterSubsumed recCalls
-
-  -- For every function, the measures we want to use
-  -- (One for each non-forbiddend arg)
-  let meassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
-  let meassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
-  let measuress := Array.zipWith meassures₁ meassures₂ (· ++ ·)
+  let forbiddenArgs ← preDefs.mapM fun preDef =>
+    getForbiddenByTrivialSizeOf fixedPrefixSize preDef
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last
-  let measures ← generateMeasures (measuress.map (·.size))
+  let measures ← generateMeasures forbiddenArgs arities
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution]
-    reportTermArgs preDefs termArgs
-    return termArgs
+    return ← buildTermWF originalVarNamess varNamess #[solution]
 
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·)
+  -- Collect all recursive calls and extract their context
+  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
+  let recCalls := filterSubsumed recCalls
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution
-    reportTermArgs preDefs termArgs
-    return termArgs
+    let wf ← buildTermWF originalVarNamess varNamess solution
+
+    let wf' := trimTermWF extraParamss wf
+    for preDef in preDefs, term in wf' do
+      if showInferredTerminationBy.get (← getOptions) then
+        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
+      if let some ref := preDef.termination.terminationBy?? then
+        Tactic.TryThis.addSuggestion ref (← term.unexpand)
+
+    return wf
   | .none =>
-    let explanation ← explainFailure (preDefs.map (·.declName)) measuress rcs
+    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
     Lean.throwError <| "Could not find a decreasing measure.\n" ++
       explanation ++ "\n" ++
       "Please use `termination_by` to specify a decreasing measure."

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -5,7 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
+import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.PackDomain
 import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.PreDefinition.WF.Preprocess
 import Lean.Elab.PreDefinition.WF.Rel
@@ -18,15 +19,29 @@ namespace Lean.Elab
 open WF
 open Meta
 
-private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition)  : TermElabM Unit := do
+private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) (fixedPrefixSize : Nat) : TermElabM Unit := do
   let us := preDefNonRec.levelParams.map mkLevelParam
   let all := preDefs.toList.map (·.declName)
   for fidx in [:preDefs.size] do
     let preDef := preDefs[fidx]!
-    let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
-      let value := mkAppN (mkConst preDefNonRec.declName us) xs
-      let value ← argsPacker.curryProj value fidx
-      mkLambdaFVars xs value
+    let value ← lambdaTelescope preDef.value fun xs _ => do
+      let packedArgs : Array Expr := xs[fixedPrefixSize:]
+      let mkProd (type : Expr) : MetaM Expr := do
+        mkUnaryArg type packedArgs
+      let rec mkSum (i : Nat) (type : Expr) : MetaM Expr := do
+        if i == preDefs.size - 1 then
+          mkProd type
+        else
+          (← whnfD type).withApp fun f args => do
+            assert! args.size == 2
+            if i == fidx then
+              return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! (← mkProd args[0]!)
+            else
+              let r ← mkSum (i+1) args[1]!
+              return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
+      let Expr.forallE _ domain _ _ := (← instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable!
+      let arg ← mkSum 0 domain
+      mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg)
     trace[Elab.definition.wf] "{preDef.declName} := {value}"
     addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all)
 
@@ -66,49 +81,25 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
   else
     return false
 
-/--
-Collect the names of the varying variables (after the fixed prefix); this also determines the
-arity for the well-founded translations, and is turned into an `ArgsPacker`.
-We use the term to determine the arity, but take the name from the type, for better names in the
-```
-fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
-```
-idiom.
--/
-def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do
-  -- We take the arity from the term, but the names from the types
-  let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size
-  assert! fixedPrefixSize ≤ arity
-  if arity = fixedPrefixSize then
-    throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
-  forallBoundedTelescope preDef.type arity fun xs _ => do
-    assert! xs.size = arity
-    let xs : Array Expr := xs[fixedPrefixSize:]
-    xs.mapM (·.fvarId!.getUserName)
-
 def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
-  let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
+  let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef
     let fixedPrefixSize ← getFixedPrefix preDefs
     trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}"
-    let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·)
-    let argsPacker := { varNamess }
     let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
-    return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
+    let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
+    return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
-  let wf : TerminationArguments ← do
+  let wf ← do
     let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
-      guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
+      guessLex preDefs unaryPreDef fixedPrefixSize
     else if preDefsWithout.isEmpty then
-      preDefsWith.mapIdxM fun funIdx predef => do
-        let arity := fixedPrefixSize + argsPacker.varNamess[funIdx]!.size
-        let hints := predef.termination
-        TerminationArgument.elab predef.declName predef.type arity hints.extraParams hints.terminationBy?.get!
+      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -118,14 +109,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
 
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
-    unless type.isForall do
-      throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.termination.decreasingBy?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
@@ -137,12 +126,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   else
     withEnableInfoTree false do
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
+    addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize
   for preDef in preDefs do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 

src/Lean/Elab/PreDefinition/WF/PackDomain.lean

@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Cases
+import Lean.Elab.PreDefinition.Basic
+
+namespace Lean.Elab.WF
+open Meta
+
+/--
+  Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
+  Return an array containing its "elements".
+  Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`.
+  -/
+private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do
+  let mut result := #[]
+  let mut t := t
+  for _ in [:arity - 1] do
+    result := result.push (mkProj ``PSigma 0 t)
+    t := mkProj ``PSigma 1 t
+  result.push t
+
+/-- Create a unary application by packing the given arguments using `PSigma.mk` -/
+partial def mkUnaryArg (type : Expr) (args : Array Expr) : MetaM Expr := do
+  go 0 type
+where
+  go (i : Nat) (type : Expr) : MetaM Expr := do
+    if i < args.size - 1 then
+      let arg := args[i]!
+      assert! type.isAppOfArity ``PSigma 2
+      let us := type.getAppFn.constLevels!
+      let α := type.appFn!.appArg!
+      let β := type.appArg!
+      assert! β.isLambda
+      let type := β.bindingBody!.instantiate1 arg
+      let rest ← go (i+1) type
+      return mkApp4 (mkConst ``PSigma.mk us) α β arg rest
+    else
+      return args[i]!
+
+/-- Unpacks a unary packed argument created with `mkUnaryArg`. -/
+def unpackUnaryArg {m} [Monad m] [MonadError m] (arity : Nat) (e : Expr) : m (Array Expr) := do
+  let mut e := e
+  let mut args := #[]
+  while args.size + 1 < arity do
+    if e.isAppOfArity ``PSigma.mk 4 then
+      args := args.push (e.getArg! 2)
+      e := e.getArg! 3
+    else
+      throwError "Unexpected expression while unpacking n-ary argument"
+  args := args.push e
+  return args
+
+private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Expr) (value : Expr) : MetaM Expr := do
+  let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
+  let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do
+    if ys.size < xs.size - 1 then
+      let xDecl  ← xs[ys.size]!.fvarId!.getDecl
+      let xDecl' ← xs[ys.size + 1]!.fvarId!.getDecl
+      let #[s] ← mvarId.cases y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable!
+      go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!)
+    else
+      let ys := ys.push (mkFVar y)
+      mvarId.assign (value.replaceFVars xs ys)
+  go mvar.mvarId! y.fvarId! #[]
+  instantiateMVars mvar
+
+/--
+  Convert the given pre-definitions into unary functions.
+  We "pack" the arguments using `PSigma`.
+-/
+partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := do
+  let mut preDefsNew := #[]
+  let mut arities := #[]
+  let mut modified := false
+  for preDef in preDefs do
+    let (preDefNew, arity, modifiedCurr) ← lambdaTelescope preDef.value fun xs _ => do
+      if xs.size == fixedPrefix then
+        throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
+      let arity := xs.size
+      if arity > fixedPrefix + 1 then
+        let bodyType ← instantiateForall preDef.type xs
+        let mut d ← inferType xs.back
+        let ys : Array Expr := xs[:fixedPrefix]
+        let xs : Array Expr := xs[fixedPrefix:]
+        for x in xs.pop.reverse do
+          d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)]
+        withLocalDeclD (← mkFreshUserName `_x) d fun tuple => do
+          let elems := mkTupleElems tuple xs.size
+          let codomain := bodyType.replaceFVars xs elems
+          let preDefNew:= { preDef with
+            declName := preDef.declName ++ `_unary
+            type := (← mkForallFVars (ys.push tuple) codomain)
+          }
+          addAsAxiom preDefNew
+          return (preDefNew, arity, true)
+      else
+        return (preDef, arity, false)
+    modified := modified || modifiedCurr
+    arities := arities.push arity
+    preDefsNew := preDefsNew.push preDefNew
+  if !modified then
+    return preDefs
+  -- Update values
+  for i in [:preDefs.size] do
+    let preDef := preDefs[i]!
+    let preDefNew := preDefsNew[i]!
+    let valueNew ← lambdaTelescope preDef.value fun xs body => do
+      let ys : Array Expr := xs[:fixedPrefix]
+      let xs : Array Expr := xs[fixedPrefix:]
+      let type ← instantiateForall preDefNew.type ys
+      forallBoundedTelescope type (some 1) fun z codomain => do
+        let z := z[0]!
+        let newBody ← mkPSigmaCasesOn z codomain xs body
+        mkLambdaFVars (ys.push z) (← packApplications newBody arities preDefsNew)
+    let isBad (e : Expr) : Bool :=
+      match isAppOfPreDef? e with
+      | none   => false
+      | some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i]!.declName != preDefs[i]!.declName
+    if let some bad := valueNew.find? isBad then
+      if let some i := isAppOfPreDef? bad then
+        throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i]!.declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]!}"
+    preDefsNew := preDefsNew.set! i { preDefNew with value := valueNew }
+  return preDefsNew
+where
+  /-- Return `some i` if `e` is a `preDefs[i]` application -/
+  isAppOfPreDef? (e : Expr) : Option Nat := do
+    let f := e.getAppFn
+    guard f.isConst
+    preDefs.findIdx? (·.declName == f.constName!)
+
+  packApplications (e : Expr) (arities : Array Nat) (preDefsNew : Array PreDefinition) : MetaM Expr := do
+    let pack (e : Expr) (funIdx : Nat) : MetaM Expr := do
+      let f := e.getAppFn
+      let args := e.getAppArgs
+      let fNew := mkConst preDefsNew[funIdx]!.declName f.constLevels!
+      let fNew := mkAppN fNew args[:fixedPrefix]
+      let Expr.forallE _ d .. ← whnf (← inferType fNew) | unreachable!
+      -- NB: Use whnf in case the type is not a manifest forall, but a definition around it
+      let argNew ← mkUnaryArg d args[fixedPrefix:]
+      return mkApp fNew argNew
+    let rec
+      visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do
+        checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
+          match e with
+          | Expr.lam n d b c =>
+            withLocalDecl n c (← visit d) fun x => do
+              mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
+          | Expr.forallE n d b c =>
+            withLocalDecl n c (← visit d) fun x => do
+              mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
+          | Expr.letE n t v b _  =>
+            withLetDecl n (← visit t) (← visit v) fun x => do
+              mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
+          | Expr.proj n i s .. => return mkProj n i (← visit s)
+          | Expr.mdata d b     => return mkMData d (← visit b)
+          | Expr.app ..        => visitApp e
+          | Expr.const ..      => visitApp e
+          | e                  => return e,
+      visitApp (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := e.withApp fun f args => do
+        let args ← args.mapM visit
+        if let some funIdx := isAppOfPreDef? f then
+          let numArgs := args.size
+          let arity   := arities[funIdx]!
+          if numArgs < arity then
+            -- Partial application
+            let extra := arity - numArgs
+            withDefault do forallBoundedTelescope (← inferType e) extra fun xs _ => do
+              if xs.size != extra then
+                return (mkAppN f args) -- It will fail later
+              else
+                mkLambdaFVars xs (← pack (mkAppN (mkAppN f args) xs) funIdx)
+          else if numArgs > arity then
+            -- Over application
+            let r ← pack (mkAppN f args[:arity]) funIdx
+            let rType ← inferType r
+            -- Make sure the new auxiliary definition has only one argument.
+            withLetDecl (← mkFreshUserName `aux) rType r fun aux =>
+              mkLetFVars #[aux] (mkAppN aux args[arity:])
+          else
+            pack (mkAppN f args) funIdx
+        else if args.isEmpty then
+          return f
+        else
+          return mkAppN (← visit f) args
+    visit e |>.run
+
+end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -4,28 +4,93 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.ArgsPacker
+import Lean.Meta.Tactic.Cases
 import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.WF.PackDomain
 
 namespace Lean.Elab.WF
 open Meta
 
+/-- Combine different function domains `ds` using `PSum`s -/
+private def mkNewDomain (ds : Array Expr) : MetaM Expr := do
+  let mut r := ds.back
+  for d in ds.pop.reverse do
+    r ← mkAppM ``PSum #[d, r]
+  return r
+
+private def getCodomainLevel (preDefType : Expr) : MetaM Level :=
+  forallBoundedTelescope preDefType (some 1) fun _ body => getLevel body
 
 /--
-Checks that all codomians have the same level, throws an error otherwise.
+  Return the universe level for the codomain of the given definitions.
+  This method produces an error if the codomains are in different universe levels.
 -/
-private def checkCodomainsLevel (fixedPrefixSize : Nat) (arities : Array Nat)
-    (preDefs : Array PreDefinition) : MetaM Unit := do
-  forallBoundedTelescope preDefs[0]!.type  (fixedPrefixSize + arities[0]!)  fun _ type₀ => do
-    let u₀ ← getLevel type₀
-    for i in [1:preDefs.size] do
-      forallBoundedTelescope preDefs[i]!.type  (fixedPrefixSize + arities[i]!) fun _ typeᵢ =>
-      unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
+private def getCodomainsLevel (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) : MetaM Level := do
+  let r ← getCodomainLevel preDefTypes[0]!
+  for i in [1:preDefTypes.size] do
+    let preDef := preDefTypes[i]!
+    unless (← isLevelDefEq r (← getCodomainLevel preDef)) do
+      let arity₀ ← lambdaTelescope preDefsOriginal[0]!.value fun xs _ => return xs.size
+      let arityᵢ ← lambdaTelescope preDefsOriginal[i]!.value fun xs _ => return xs.size
+      forallBoundedTelescope preDefsOriginal[0]!.type arity₀ fun _ type₀ =>
+      forallBoundedTelescope preDefsOriginal[i]!.type arityᵢ fun _ typeᵢ =>
         withOptions (fun o => pp.sanitizeNames.set o false) do
-          throwError m!"invalid mutual definition, result types must be in the same universe " ++
-            m!"level, resulting type " ++
-            m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
-            m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
+          throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
+  return r
+
+/--
+  Create the codomain for the new function that "combines" different `preDef` types
+  See: `packMutual`
+-/
+private partial def mkNewCoDomain (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) (x : Expr) : MetaM Expr := do
+  let u ← getCodomainsLevel preDefsOriginal preDefTypes
+  let rec go (x : Expr) (i : Nat) : MetaM Expr := do
+    if i < preDefTypes.size - 1 then
+      let xType ← whnfD (← inferType x)
+      assert! xType.isAppOfArity ``PSum 2
+      let xTypeArgs := xType.getAppArgs
+      let casesOn := mkConst (mkCasesOnName ``PSum) (mkLevelSucc u :: xType.getAppFn.constLevels!)
+      let casesOn := mkAppN casesOn xTypeArgs -- parameters
+      let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive
+      let casesOn := mkApp casesOn x -- major
+      let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x => do
+        mkLambdaFVars #[x] ((← whnf preDefTypes[i]!).bindingBody!.instantiate1 x)
+      let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1]! fun x => do
+        mkLambdaFVars #[x] (← go x (i+1))
+      return mkApp2 casesOn minor1 minor2
+    else
+      return (← whnf preDefTypes[i]!).bindingBody!.instantiate1 x
+  go x 0
+
+/--
+  Combine/pack the values of the different definitions in a single value
+  `x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`.
+  See: `packMutual`.
+  Remark: this method does not replace the nested recursive `preDefValues` applications.
+  This step is performed by `transform` with the following `post` method.
+ -/
+private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do
+  let varNames := preDefValues.map fun val =>
+    assert! val.isLambda
+    val.bindingName!
+  let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
+  let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do
+    if i < preDefValues.size - 1 then
+      /-
+        Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions).
+      -/
+      let givenNames : Array AltVarNames :=
+         if i == preDefValues.size - 2 then
+           #[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }]
+         else
+           #[{ varNames := [varNames[i]!] }]
+       let #[s₁, s₂] ← mvarId.cases x (givenNames := givenNames) | unreachable!
+      s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta
+      go s₂.mvarId s₂.fields[0]!.fvarId! (i+1)
+    else
+      mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta
+  go mvar.mvarId! x.fvarId! 0
+  instantiateMVars mvar
 
 /--
   Pass the first `n` arguments of `e` to the continuation, and apply the result to the
@@ -47,54 +112,141 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr :
       mkLambdaFVars xs e'
 
 /--
-A `post` for `Meta.transform` to replace recursive calls to the original `preDefs` with calls
-to the new unary function `newfn`.
+If `arg` is the argument to the `fidx`th of the `numFuncs` in the recursive group,
+then `mkMutualArg` packs that argument in `PSum.inl` and `PSum.inr` constructors
+to create the mutual-packed argument of type `domain`.
 -/
-private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name)
-    (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
+partial def mkMutualArg (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr := do
+  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+    if i == numFuncs - 1 then
+      return arg
+    else
+      (← whnfD type).withApp fun f args => do
+        assert! args.size == 2
+        if i == fidx then
+          return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg
+        else
+          let r ← go (i+1) args[1]!
+          return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
+  go 0 domain
+
+/--
+Unpacks a mutually packed argument, returning the argument and function index.
+Inverse of `mkMutualArg`.  Cf. `unpackUnaryArg` and `unpackArg`, which does both
+-/
+def unpackMutualArg {m} [Monad m] [MonadError m] (numFuncs : Nat) (e : Expr) : m (Nat × Expr) := do
+  let mut funidx := 0
+  let mut e := e
+  while funidx + 1 < numFuncs do
+    if e.isAppOfArity ``PSum.inr 3 then
+      e := e.getArg! 2
+      funidx := funidx + 1
+    else if e.isAppOfArity ``PSum.inl 3 then
+      e := e.getArg! 2
+      break
+    else
+      throwError "Unexpected expression while unpacking mutual argument"
+  return (funidx, e)
+
+/--
+Given the packed argument of a (possibly) mutual and (possibly) nary call,
+return the function index that is called and the arguments individually.
+
+We expect precisely the expressions produced by `packMutual`, with manifest
+`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
+rather than using projectinos.
+-/
+def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
+    m (Nat × Array Expr) := do
+  let (funidx, e) ← unpackMutualArg arities.size e
+  let args ← unpackUnaryArg arities[funidx]! e
+  return (funidx, args)
+
+
+/--
+Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`.
+See: `packMutual`
+-/
+private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
   let f := e.getAppFn
   if !f.isConst then
     return TransformStep.done e
   let declName := f.constName!
   let us       := f.constLevels!
-  if let some fidx := funNames.getIdx? declName then
-    let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
-    let e' ← withAppN arity e fun args => do
+  if let some fidx := preDefs.findIdx? (·.declName == declName) then
+    let e' ← withAppN (fixedPrefix + 1) e fun args => do
       let fixedArgs := args[:fixedPrefix]
-      let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:]
+      let arg := args[fixedPrefix]!
+      let packedArg ← mkMutualArg preDefs.size domain fidx arg
       return mkApp (mkAppN (mkConst newFn us) fixedArgs) packedArg
     return TransformStep.done e'
   return TransformStep.done e
 
+partial def withFixedPrefix (fixedPrefix : Nat) (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → Array Expr → MetaM α) : MetaM α :=
+  go fixedPrefix #[] (preDefs.map (·.value))
+where
+  go (i : Nat) (fvars : Array Expr) (vals : Array Expr) : MetaM α := do
+    match i with
+    | 0 => k fvars (← preDefs.mapM fun preDef => instantiateForall preDef.type fvars) vals
+    | i+1 =>
+      withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
+        go i (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
+
 /--
-Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker`
-module.
--/
-def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
-  let arities := argsPacker.arities
-  if let #[1] := arities then return preDefs[0]!
-  let newFn := if argsPacker.numFuncs > 1 then preDefs[0]!.declName ++ `_mutual
-                                          else preDefs[0]!.declName ++ `_unary
+  If `preDefs.size > 1`, combine different functions in a single one using `PSum`.
+  This method assumes all `preDefs` have arity 1, and have already been processed using `packDomain`.
+  Here is a small example. Suppose the input is
+  ```
+  f x :=
+    match x.2.1, x.2.2.1, x.2.2.2 with
+    | 0, a, b => a
+    | Nat.succ n, a, b => (g ⟨x.1, n, a, b⟩).fst
+  g x :=
+    match x.2.1, x.2.2.1, x.2.2.2 with
+    | 0, a, b => (a, b)
+    | Nat.succ n, a, b => (h ⟨x.1, n, a, b⟩, a)
+  h x =>
+    match x.2.1, x.2.2.1, x.2.2.2 with
+    | 0, a, b => b
+    | Nat.succ n, a, b => f ⟨x.1, n, a, b⟩
+  ```
+  this method produces the following pre definition
+  ```
+  f._mutual x :=
+    PSum.casesOn x
+      (fun val =>
+        match val.2.1, val.2.2.1, val.2.2.2 with
+        | 0, a, b => a
+        | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst
+      fun val =>
+        PSum.casesOn val
+          (fun val =>
+            match val.2.1, val.2.2.1, val.2.2.2 with
+            | 0, a, b => (a, b)
+            | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a)
+          fun val =>
+            match val.2.1, val.2.2.1, val.2.2.2 with
+            | 0, a, b => b
+            | Nat.succ n, a, b =>
+              f._mutual (PSum.inl ⟨val.1, n, a, b⟩)
+  ```
 
-  checkCodomainsLevel fixedPrefix argsPacker.arities preDefs
-  -- Bring the fixed Prefix into scope
-  forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do
-    let types ← preDefs.mapM (instantiateForall ·.type ys)
-    let vals ← preDefs.mapM (instantiateLambda ·.value ys)
-
-    let type ← argsPacker.uncurryType types
-    let packedDomain := type.bindingDomain!
-
-    -- Temporarily add the unary function as an axiom, so that all expressions
-    -- are still type correct
-    let type ← mkForallFVars ys type
-    let preDefNew := { preDefs[0]! with declName := newFn, type }
-    addAsAxiom preDefNew
-
-    let value ← argsPacker.uncurry vals
-    let value ← transform value (skipConstInApp := true)
-      (post := post fixedPrefix argsPacker (preDefs.map (·.declName)) packedDomain newFn)
-    let value ← mkLambdaFVars ys value
-    return { preDefNew with value }
+  Remark: `preDefsOriginal` is used for error reporting, it contains the definitions before applying `packDomain`.
+ -/
+def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
+  if preDefs.size == 1 then return preDefs[0]!
+  withFixedPrefix fixedPrefix preDefs fun ys types vals => do
+    let domains ← types.mapM fun type => do pure (← whnf type).bindingDomain!
+    let domain ← mkNewDomain domains
+    withLocalDeclD (← mkFreshUserName `_x) domain fun x => do
+      let codomain ← mkNewCoDomain preDefsOriginal types x
+      let type ← mkForallFVars (ys.push x) codomain
+      let value ← packValues x codomain vals
+      let newFn := preDefs[0]!.declName ++ `_mutual
+      let preDefNew := { preDefs[0]! with declName := newFn, type, value }
+      addAsAxiom preDefNew
+      let value ← transform value (skipConstInApp := true) (post := post fixedPrefix preDefs domain newFn)
+      let value ← mkLambdaFVars (ys.push x) value
+      return { preDefNew with value }
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -9,58 +9,76 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationArgument
-import Lean.Meta.ArgsPacker
+import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.WF
 open Meta
 open Term
 
-/--
-The termination arguments must not depend on the varying parameters of the function, and in
-a mutual clique, they must be the same for all functions.
+private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
+  let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
+    if i < preDefs.size - 1 then
+      let #[s₁, s₂] ←  mvarId.cases fvarId | unreachable!
+      go (i + 1) s₂.mvarId s₂.fields[0]!.fvarId! (result.push (s₁.fields[0]!.fvarId!, s₁.mvarId))
+    else
+      return result.push (fvarId, mvarId)
+  go 0 mvarId fvarId #[]
 
-This ensures the preconditions for `ArgsPacker.uncurryND`.
--/
-def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat)
-    (termArgs : TerminationArguments) : TermElabM Expr := do
-  let mut codomains := #[]
-  for name in names, arity in arities, termArg in termArgs do
-    let type ← inferType (termArg.fn.beta prefixArgs)
-    let codomain ← forallBoundedTelescope type arity fun xs codomain => do
-      let fvars := xs.map (·.fvarId!)
-      if codomain.hasAnyFVar (fvars.contains ·) then
-        throwErrorAt termArg.ref  m!"The termination argument's type must not depend on the " ++
-          m!"function's varying parameters, but {name}'s termination argument does:{indentExpr type}\n" ++
-          "Try using `sizeOf` explicitly"
-      pure codomain
-    codomains := codomains.push codomain
+private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
+    (fvarId : FVarId) (element : TerminationBy) : TermElabM MVarId := do
+  element.checkVars preDef.declName preDef.termination.extraParams
+  -- If `synthetic := false`, then this is user-provided, and should be interpreted
+  -- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
+  -- (Not pretty, but it works for now)
+  let implicit_underscores :=
+    if element.synthetic then 0 else preDef.termination.extraParams - element.vars.size
+  let varNames ← lambdaTelescope preDef.value fun xs _ => do
+    let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
+    for h : i in [:element.vars.size] do
+      let varStx := element.vars[i]
+      if let `($ident:ident) := varStx then
+        let j := varNames.size - implicit_underscores - element.vars.size + i
+        varNames := varNames.set! j ident.getId
+    return varNames
+  let mut mvarId := mvarId
+  for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
+    unless localDecl.userName == varName do
+      mvarId ← mvarId.rename localDecl.fvarId varName
+  let numPackedArgs := varNames.size - prefixSize
+  let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do
+    trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}"
+    if i < numPackedArgs - 1 then
+      let #[s] ← mvarId.cases fvarId #[{ varNames := [varNames[prefixSize + i]!] }] | unreachable!
+      go (i+1) s.mvarId s.fields[1]!.fvarId!
+    else
+      mvarId.rename fvarId varNames.back
+  go 0 mvarId fvarId
 
-  let codomain0 := codomains[0]!
-  for h : i in [1 : codomains.size] do
-    unless ← isDefEqGuarded codomain0 codomains[i] do
-      throwErrorAt termArgs[i]!.ref m!"The termination arguments of mutually recursive functions " ++
-        m!"must have the same return type, but the termination argument of {names[0]!} has type" ++
-        m!"{indentExpr codomain0}\n" ++
-        m!"while the termination argument of {names[i]!} has type{indentExpr codomains[i]}\n" ++
-        "Try using `sizeOf` explicitly"
-  return codomain0
-
-/--
-If the `termArgs` map the packed argument `argType` to `β`, then this function passes to the
-continuation a value of type `WellFoundedRelation argType` that is derived from the instance
-for `WellFoundedRelation β` using `invImage`.
--/
-def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
-    (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
-    (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
+def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
+    (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
-  let v ← getLevel β
-  let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
-  let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)
-  let rel ← instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst)
-  k rel
+  let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
+  trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
+  withDeclName unaryPreDefName do
+    let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
+    let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
+    let (d, fMVarId) ← fMVarId.intro1
+    let subgoals ← unpackMutual preDefs fMVarId d
+    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
+      mvarId.withContext do
+        let errorMsgHeader? := if preDefs.size > 1 then
+          "The termination argument types differ for the different functions, or depend on the " ++
+          "function's varying parameters. Try using `sizeOf` explicitly:\nThe termination argument"
+        else
+          "The termination argument depends on the function's varying parameters. Try using " ++
+          "`sizeOf` explicitly:\nThe termination argument"
+        let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+            (errorMsgHeader? := errorMsgHeader?)
+        mvarId.assign value
+    let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
+    wfRelMVarId.assign wfRelVal
+    k (← instantiateMVars (mkMVar mainMVarId))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean

@@ -1,106 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Joachim Breitner
--/
-prelude
-
-import Lean.Parser.Term
-import Lean.Elab.Term
-import Lean.Elab.Binders
-import Lean.Elab.SyntheticMVars
-import Lean.Elab.PreDefinition.WF.TerminationHint
-import Lean.PrettyPrinter.Delaborator
-
-/-!
-This module contains the data type `TerminationArgument`, the elaborated form of a `TerminationBy`
-clause, the `TerminationArguments` type for a clique and the elaboration functions.
--/
-
-set_option autoImplicit false
-
-namespace Lean.Elab.WF
-
-open Lean Meta Elab Term
-
-/--
-Elaborated form for a `termination_by` clause.
-
-The `fn` has the same (value) arity as the recursive functions (stored in
-`arity`), and maps its arguments (including fixed prefix, in unpacked form) to
-the termination argument.
--/
-structure TerminationArgument where
-  ref : Syntax
-  arity : Nat
-  extraParams : Nat
-  fn : Expr
-deriving Inhabited
-
-/-- A complete set of `TerminationArgument`s, as applicable to a single clique.  -/
-abbrev TerminationArguments := Array TerminationArgument
-
-/--
-Elaborates a `TerminationBy` to an `TerminationArgument`.
-
-* `type` is the full type of the original recursive function, including fixed prefix.
-* `arity` is the value arity of the recursive function; the termination argument cannot take more.
-* `extraParams` is the the number of parameters the function has after the colon; together with
-  `arity` indicates how many parameters of the function are before the colon and thus in scope.
-* `hint : TerminationBy` is the syntactic `TerminationBy`.
--/
-def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
-    (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
-  assert! extraParams ≤ arity
-
-  if hint.vars.size > extraParams then
-    let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
-      m!"{funName} only binds {parameters extraParams}."
-    if let `($ident:ident) := hint.vars[0]! then
-      if ident.getId.isSuffixOf funName then
-          msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
-            "expects the function name here.)"
-    throwErrorAt hint.ref msg
-
-  -- Bring parameters before the colon into scope
-  let r ← withoutErrToSorry <|
-    forallBoundedTelescope type (arity - extraParams) fun ys type' => do
-      -- Bring the variables bound by `termination_by` into scope.
-      elabFunBinders hint.vars (some type') fun xs type' => do
-        -- Elaborate the body in this local environment
-        let body ← Lean.Elab.Term.withSynthesize <| elabTermEnsuringType hint.body none
-        -- Now abstract also over the remaining extra parameters
-        forallBoundedTelescope type'.get! (extraParams - hint.vars.size) fun zs _ => do
-          mkLambdaFVars (ys ++ xs ++ zs) body
-  -- logInfo m!"elabTermValue: {r}"
-  check r
-  pure { ref := hint.ref, arity, extraParams, fn := r}
-  where
-    parameters : Nat → MessageData
-    | 1 => "one parameter"
-    | n => m!"{n} parameters"
-
-open PrettyPrinter Delaborator SubExpr Parser.Termination Parser.Term in
-def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax ``terminationBy) := do
-  lambdaTelescope termArg.fn fun ys e => do
-    let e ← mkLambdaFVars ys[termArg.arity - termArg.extraParams:] e -- undo overshooting by lambdaTelescope
-    pure (← delabCore e (delab := go termArg.extraParams #[])).1
-  where
-    go : Nat → TSyntaxArray [`ident, `Lean.Parser.Term.hole] → DelabM (TSyntax ``terminationBy)
-    | 0, vars => do
-      -- drop trailing underscores
-      let mut vars := vars
-      while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
-      if vars.isEmpty then
-        `(terminationBy|termination_by $(← Delaborator.delab))
-      else
-        `(terminationBy|termination_by $vars* => $(← Delaborator.delab))
-    | i+1, vars => do
-      let e ← getExpr
-      unless e.isLambda do return ← go 0 vars -- should not happen
-
-      -- Delaborate unused parameters with `_`
-      if e.bindingBody!.hasLooseBVar 0 then
-        withBindingBodyUnusedName fun n => go i (vars.push ⟨n⟩)
-      else
-        descend e.bindingBody! 1 (go i (vars.push (← `(hole|_))))

src/Lean/Elab/PreDefinition/WF/TerminationHint.lean

@@ -26,6 +26,18 @@ structure TerminationBy where
   synthetic : Bool := false
   deriving Inhabited
 
+open Parser.Termination in
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
+  -- TODO: Why can I not just use $wf.vars in the quotation below?
+  let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
+  if vars.isEmpty then
+    `(terminationBy|termination_by $wf.body)
+  else
+    `(terminationBy|termination_by $vars* => $wf.body)
+
+/-- A complete set of `termination_by` hints, as applicable to a single clique.  -/
+abbrev TerminationWF := Array TerminationBy
+
 /-- A single `decreasing_by` clause -/
 structure DecreasingBy where
   ref       : Syntax

src/Lean/Elab/Print.lean

@@ -80,7 +80,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
 
 private def printId (id : Syntax) : CommandElabM Unit := do
   addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
-  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
+  let cs ← resolveGlobalConstWithInfos id
   cs.forM printIdCore
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
@@ -125,7 +125,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do
-    let cs ← liftCoreM <| realizeGlobalConstWithInfos id
+    let cs ← resolveGlobalConstWithInfos id
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax
 
@@ -140,7 +140,7 @@ private def printEqnsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printEqns»] def elabPrintEqns : CommandElab := fun stx => do
   let id := stx[2]
-  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
+  let cs ← resolveGlobalConstWithInfos id
   cs.forM printEqnsOf
 
 end Lean.Elab.Command

src/Lean/Elab/Quotation/Precheck.lean

@@ -92,7 +92,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
        notation "x++" => x.foo
        ```
     -/
-    if let _::_ ← realizeGlobalNameWithInfos stx val then
+    if let _::_ ← resolveGlobalNameWithInfos stx val then
       return
     if (← read).quotLCtx.contains val then
       return

src/Lean/Elab/Structure.lean

@@ -892,7 +892,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   let exts      := stx[3]
   let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
   let optType   := stx[4]
-  let derivingClassViews ← liftCoreM <| getOptDerivingClasses stx[6]
+  let derivingClassViews ← getOptDerivingClasses stx[6]
   let type ← if optType.isNone then `(Sort _) else pure optType[0][1]
   let declName ←
     runTermElabM fun scopeVars => do

src/Lean/Elab/Tactic.lean

@@ -38,4 +38,3 @@ import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
 import Lean.Elab.Tactic.ShowTerm
-import Lean.Elab.Tactic.Rfl

src/Lean/Elab/Tactic/Conv/Delta.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
-  let declNames ← stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
+  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
   let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 

src/Lean/Elab/Tactic/Conv/Unfold.lean

@@ -12,7 +12,7 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
+    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
     applySimpResult (← unfold (← getLhs) declName)
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Delta.lean

@@ -29,7 +29,7 @@ def deltaTarget (declNames : Array Name) : TacticM Unit := do
 
 /-- "delta " ident+ (location)? -/
 @[builtin_tactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
-  let declNames ← stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
+  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
   let loc := expandOptLocation stx[2]
   withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
     (throwTacticEx `delta · m!"did not delta reduce {declNames}")

src/Lean/Elab/Tactic/Ext.lean

@@ -153,7 +153,7 @@ elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
 @[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
   match stx with
   | `(ext_type%  $flat:term $struct:ident) => do
-    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
       let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
         mkForall f BinderInfo.default h ty
       mkForallFVars (params |>.push x |>.push y) ty
@@ -166,7 +166,7 @@ elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
 @[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
   match stx with
   | `(ext_iff_type% $flat:term $struct:ident) => do
-    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
       mkForallFVars (params |>.push x |>.push y) <|
         mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Induction.lean

@@ -534,9 +534,9 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
       return e
 
 -- `optElimId` is of the form `("using" term)?`
-private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
+private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool): TacticM ElimInfo := do
   if optElimId.isNone then
-    if let some elimName ← getCustomEliminator? targets induction then
+    if let some elimName ← getCustomEliminator? targets then
       return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"

src/Lean/Elab/Tactic/NormCast.lean

@@ -268,7 +268,7 @@ open Command in
   match stx with
   | `(norm_cast_add_elim $id:ident) =>
     Elab.Command.liftCoreM do MetaM.run' do
-     addElim (← realizeGlobalConstNoOverload id)
+     addElim (← resolveGlobalConstNoOverload id)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.NormCast

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -5,10 +5,8 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.BinderPredicates
-import Init.Data.Int.Order
-import Init.Data.List.Lemmas
-import Init.Data.Nat.MinMax
 import Init.Data.Option.Lemmas
+import Init.Data.Nat.Bitwise.Lemmas
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -7,9 +7,8 @@ prelude
 import Init.Omega.LinearCombo
 import Init.Omega.Int
 import Init.Omega.Logic
-import Init.Data.BitVec.Basic
+import Init.Data.BitVec
 import Lean.Meta.AppBuilder
-import Lean.Meta.Canonicalizer
 
 /-!
 # The `OmegaM` state monad.
@@ -55,7 +54,7 @@ structure State where
   atoms : HashMap Expr Nat := {}
 
 /-- An intermediate layer in the `OmegaM` monad. -/
-abbrev OmegaM' := StateRefT State (ReaderT Context CanonM)
+abbrev OmegaM' := StateRefT State (ReaderT Context MetaM)
 
 /--
 Cache of expressions that have been visited, and their reflection as a linear combination.
@@ -71,7 +70,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
 
 /-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
 def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
-  m.run' HashMap.empty |>.run' {} { cfg } |>.run
+  m.run' HashMap.empty |>.run' {} { cfg }
 
 /-- Retrieve the user-specified configuration options. -/
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
@@ -177,7 +176,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
       | _, (``BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const ``BitVec.isLt []) n x)
+        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with
@@ -245,7 +244,6 @@ Return its index, and, if it is new, a collection of interesting facts about the
 -/
 def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do
   let c ← getThe State
-  let e ← canon e
   match c.atoms.find? e with
   | some i => return (i, none)
   | none =>

src/Lean/Elab/Tactic/Rewrite.lean

@@ -51,13 +51,11 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             x symm term
           else
             -- Try to get equation theorems for `id`.
-            let declName ← try realizeGlobalConstNoOverload id catch _ => return (← x symm term)
+            let declName ← try resolveGlobalConstNoOverload id catch _ => return (← x symm term)
             let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
             let rec go : List Name →  TacticM Unit
               | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
-              -- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
-              -- See test: `rwPrioritizesLCtxOverEnv.lean`
-              | eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms
+              | eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
             go eqThms.toList
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
         match term with

src/Lean/Elab/Tactic/Rfl.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2022 Newell Jensen. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Newell Jensen, Thomas Murrills
--/
-prelude
-import Lean.Meta.Tactic.Rfl
-import Lean.Elab.Tactic.Basic
-
-/-!
-# `rfl` tactic extension for reflexive relations
-
-This extends the `rfl` tactic so that it works on any reflexive relation,
-provided the reflexivity lemma has been marked as `@[refl]`.
--/
-
-namespace Lean.Elab.Tactic.Rfl
-
-/--
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
--/
-elab_rules : tactic
-  | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-
-@[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
-  match stx with
-  | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.Rfl

src/Lean/Elab/Tactic/ShowTerm.lean

@@ -7,7 +7,7 @@ prelude
 import Lean.Elab.ElabRules
 import Lean.Meta.Tactic.TryThis
 
-namespace Lean.Elab.Tactic.ShowTerm
+namespace Std.Tactic
 open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
 
 @[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
@@ -26,5 +26,3 @@ open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
     addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
     pure e
   | _, _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/Simp.lean

@@ -179,7 +179,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let id := arg[1]
-            let declNames? ← try pure (some (← realizeGlobalConst id)) catch _ => pure none
+            let declNames? ← try pure (some (← resolveGlobalConst id)) catch _ => pure none
             if let some declNames := declNames? then
               let declName ← ensureNonAmbiguous id declNames
               if (← Simp.isSimproc declName) then

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -56,8 +56,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
   | _ => throwUnsupportedSyntax
 
 /-- Implementation of `dsimp?`. -/
-def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
-    TacticM Simp.UsedSimps := do
+def dsimpLocation' (ctx : Simp.Context) (loc : Location) : TacticM Simp.UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -70,8 +69,8 @@ where
   /-- Implementation of `dsimp?`. -/
   go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
-      (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, usedSimps) ←
+      dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
@@ -84,9 +83,8 @@ where
       `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, simprocs, .. } ←
-      withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let usedSimps ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
+    let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+    let usedSimps ← dsimpLocation' ctx <| (loc.map expandLocation).getD (.targets #[] true)
     let stx ← mkSimpCallStx stx usedSimps
     addSuggestion tk stx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simpa.lean

@@ -18,7 +18,7 @@ register_option linter.unnecessarySimpa : Bool := {
   descr := "enable the 'unnecessary simpa' linter"
 }
 
-namespace Lean.Elab.Tactic.Simpa
+namespace Std.Tactic.Simpa
 
 open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 
@@ -86,5 +86,3 @@ deriving instance Repr for UseImplicitLambdaResult
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
     | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.Simpa

src/Lean/Elab/Tactic/Simproc.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
-import Lean.ReservedNameAction
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
@@ -38,16 +37,16 @@ namespace Command
 
 @[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
   let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
-    let declName ← realizeGlobalConstNoOverload declName
     discard <| checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     registerSimproc declName keys
 
 @[builtin_command_elab Lean.Parser.simprocPatternBuiltin] def elabSimprocPatternBuiltin : CommandElab := fun stx => do
   let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
-    let declName ← realizeGlobalConstNoOverload declName
     let dsimp ← checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc

src/Lean/Elab/Tactic/Unfold.lean

@@ -24,7 +24,7 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
     go declNameId loc
 where
   go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
-    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
+    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
     withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
 
 end Lean.Elab.Tactic

src/Lean/Elab/Term.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.ReservedNameAction
 import Lean.Meta.AppBuilder
 import Lean.Meta.CollectMVars
 import Lean.Meta.Coe
@@ -794,10 +793,10 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
     | _            => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
 
 /--
-If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
+  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
+  If they are not, then try coercions.
 
-Argument `f?` is used only for generating error messages when inserting coercions fails.
--/
+  Argument `f?` is used only for generating error messages. -/
 def ensureHasType (expectedType? : Option Expr) (e : Expr)
     (errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
   let some expectedType := expectedType? | return e
@@ -1433,22 +1432,9 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
   withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
 
-/--
-Similar to `Lean.Elab.Term.elabTerm`, but ensures that the type of the elaborated term is `expectedType?`
-by inserting coercions if necessary.
-
-If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
-Otherwise, it throws the error.
--/
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
-  try
-    withRef stx <| ensureHasType expectedType? e errorMsgHeader?
-  catch ex =>
-    if (← read).errToSorry && ex matches .error .. then
-      exceptionToSorry ex expectedType?
-    else
-      throw ex
+  withRef stx <| ensureHasType expectedType? e errorMsgHeader?
 
 /-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`. -/
 def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
@@ -1654,7 +1640,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
     return [(e, projs)]  -- section variables should shadow global decls
   if preresolved.isEmpty then
-    process (← realizeGlobalName n)
+    process (← resolveGlobalName n)
   else
     process preresolved
 where

src/Lean/Environment.lean

@@ -209,13 +209,8 @@ def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
 
 def isConstructor (env : Environment) (declName : Name) : Bool :=
   match env.find? declName with
-  | some (.ctorInfo _) => true
-  | _                  => false
-
-def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
-  match env.find? declName with
-  | some (.defnInfo { safety := .safe, .. }) => true
-  | _ => false
+  | ConstantInfo.ctorInfo _ => true
+  | _                       => false
 
 def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
   env.header.moduleNames.findIdx? (· == moduleName)
@@ -235,7 +230,6 @@ inductive KernelException where
   | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
   | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
   | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
-  | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr)
   | other            (msg : String)
   | deterministicTimeout
   | excessiveMemory
@@ -775,33 +769,6 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       moduleNames := s.moduleNames.push i.module
     }
 
-/--
-Return `true` if `cinfo₁` and `cinfo₂` are theorems with the same name, universe parameters,
-and types. We allow different modules to prove the same theorem.
-
-Motivation: We want to generate equational theorems on demand and potentially
-in different files, and we want them to have non-private names.
-We may add support for other kinds of definitions in the future. For now, theorems are
-sufficient for our purposes.
-
-We may have to revise this design decision and eagerly generate equational theorems when
-we implement the module system.
-
-Remark: we do not check whether the theorem `value` field match. This feature is useful and
-ensures the proofs for equational theorems do not need to be identical. This decision
-relies on the fact that theorem types are propositions, we have proof irrelevance,
-and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems
-during type-checking, but we are assuming this is not an issue in practice,
-and we are planning to address this issue in the future.
--/
-private def equivInfo (cinfo₁ cinfo₂ : ConstantInfo) : Bool := Id.run do
-  let .thmInfo tval₁ := cinfo₁ | false
-  let .thmInfo tval₂ := cinfo₂ | false
-  return tval₁.name == tval₂.name
-    && tval₁.type == tval₂.type
-    && tval₁.levelParams == tval₂.levelParams
-    && tval₁.all == tval₂.all
-
 /--
   Construct environment from `importModulesCore` results.
 
@@ -820,13 +787,11 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   for h:modIdx in [0:s.moduleData.size] do
     let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
-      match constantMap.insertIfNew cname cinfo with
-      | (constantMap', cinfoPrev?) =>
+      match constantMap.insert' cname cinfo with
+      | (constantMap', replaced) =>
         constantMap := constantMap'
-        if let some cinfoPrev := cinfoPrev? then
-          -- Recall that the map has not been modified when `cinfoPrev? = some _`.
-          unless equivInfo cinfoPrev cinfo do
-            throwAlreadyImported s const2ModIdx modIdx cname
+        if replaced then
+          throwAlreadyImported s const2ModIdx modIdx cname
       const2ModIdx := const2ModIdx.insert cname modIdx
     for cname in mod.extraConstNames do
       const2ModIdx := const2ModIdx.insert cname modIdx

src/Lean/Expr.lean

@@ -2007,10 +2007,6 @@ private def natAddFn : Expr :=
   let nat := mkConst ``Nat
   mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHAdd [0]) nat (mkConst ``instAddNat))
 
-private def natSubFn : Expr :=
-  let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHSub [0]) nat (mkConst ``instSubNat))
-
 private def natMulFn : Expr :=
   let nat := mkConst ``Nat
   mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHMul [0]) nat (mkConst ``instMulNat))
@@ -2023,10 +2019,6 @@ def mkNatSucc (a : Expr) : Expr :=
 def mkNatAdd (a b : Expr) : Expr :=
   mkApp2 natAddFn a b
 
-/-- Given `a b : Nat`, returns `a - b` -/
-def mkNatSub (a b : Expr) : Expr :=
-  mkApp2 natSubFn a b
-
 /-- Given `a b : Nat`, returns `a * b` -/
 def mkNatMul (a b : Expr) : Expr :=
   mkApp2 natMulFn a b