fix: fold raw Nat literals at dsimp

closes #2916

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

RELEASES.md

@@ -11,10 +11,6 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
-* 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
@@ -35,33 +31,6 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
-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.

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

@@ -809,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/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/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/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.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n

src/Init/PropLemmas.lean

@@ -21,7 +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]
+  funext _; simp only [true_iff, id.def, eq_iff_iff]
 
 /-! ## not -/
 

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/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/Elab/BuiltinCommand.lean

@@ -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 <| resolveGlobalConstNoOverloadWithInfo 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/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

@@ -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
-         resolveGlobalConst' ident
+         resolveGlobalConst ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then

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 resolveGlobalConstNoOverloadWithInfo
+     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← liftCoreM <| resolveGlobalConstNoOverloadWithInfo cls
+         let className ← resolveGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,7 +118,7 @@ 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 := #[]

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 ← resolveGlobalConstNoOverloadWithInfo 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
 
@@ -284,24 +283,27 @@ def addConstInfo [MonadEnv m] [MonadError m]
 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 resolveGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
-  let n ← resolveGlobalConstNoOverload' 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 `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
-def resolveGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
-  let ns ← resolveGlobalConst' id
+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 `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
-def resolveGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
-  let ns ← resolveGlobalName' id
+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/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 ← resolveGlobalConstNoOverload' 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

@@ -370,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
@@ -379,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

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

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

@@ -107,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
@@ -117,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

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

@@ -302,11 +302,7 @@ 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.
-NB: We must use the instance of the type of the function parameter!
-The concrete argument at hand may have a different (still def-eq) typ.
--/
+/-- 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
@@ -319,8 +315,8 @@ def mkSizeOf (e : Expr) : MetaM Expr := do
 For a given recursive call, and a choice of parameter and argument index,
 try to prove equality, < or ≤.
 -/
-def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext)
-  (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
+def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
+    MetaM GuessLexRel := do
   rcc.ctxt.run do
     let param := rcc.params[paramIdx]!
     let arg := rcc.args[argIdx]!
@@ -411,7 +407,7 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
       return .eq
 
 /--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
+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.
@@ -429,47 +425,6 @@ def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition)
         result := result.push i
     return result
 
-/--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
-where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff the
-`WellFoundedRelation` of `aᵢ` goes via `SizeOf`, and `aᵢ` does not depend on `y₁`….
-
-These are the parameters for which we omit an explicit call to `sizeOf` in the termination argument.
-
-We only use this in the non-mutual case; in the mutual case we would have to additional check
-if the parameters that line up in the actual `TerminationWF` have the same type.
--/
-def getSizeOfParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let xs  : Array Expr := xs[fixedPrefixSize:]
-    let mut result := #[]
-    for x in xs, i in [:xs.size] do
-      try
-        let t ← inferType x
-        if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then continue
-        let u ← getLevel t
-        let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
-        let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
-        if ← isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) then
-          result := result.push i
-      catch _ =>
-        pure ()
-    return result
-
-/--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
-where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `aᵢ` is `Nat`.
-These are parameters where we can definitely omit the call to `sizeOf`.
--/
-def getNatParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let xs  : Array Expr := xs[fixedPrefixSize:]
-    let mut result := #[]
-    for x in xs, i in [:xs.size] do
-      let t ← inferType x
-      if ← withReducible (isDefEq t (.const `Nat [])) then
-        result := result.push i
-    return result
 
 /--
 Generate all combination of arguments, skipping those that are forbidden.
@@ -584,26 +539,23 @@ combination of these measures. The parameters are
 * `measures`: The measures to be used.
 -/
 def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
-  (needsNoSizeOf : Array (Array Nat)) (measures : Array MutualMeasure) : MetaM TerminationWF := do
+  (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]!
-          if needsNoSizeOf[funIdx]!.contains varIdx then
-            `($v)
-          else
-            -- 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)
+          -- 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 }
@@ -716,20 +668,11 @@ def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
     r := r ++ (← explainMutualFailure declNames varNamess rcs)
   return r
 
-/--
-Shows the termination measure used to the user, and implements `termination_by?`
--/
-def reportWF (preDefs : Array PreDefinition) (wf : TerminationWF) : MetaM Unit := do
-  let extraParamss := preDefs.map (·.termination.extraParams)
-  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)
+end Lean.Elab.WF.GuessLex
 
-end GuessLex
-open GuessLex
+namespace Lean.Elab.WF
+
+open Lean.Elab.WF.GuessLex
 
 /--
 Main entry point of this module:
@@ -740,17 +683,14 @@ terminates. See the module doc string for a high-level overview.
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (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}"
 
-  let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize)
-  let needsNoSizeOf ←
-    if preDefs.size = 1 then
-      preDefs.mapM (getSizeOfParams fixedPrefixSize)
-    else
-      preDefs.mapM (getNatParams fixedPrefixSize)
+  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
@@ -758,9 +698,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf #[solution]
-    reportWF preDefs wf
-    return wf
+    return ← buildTermWF originalVarNamess varNamess #[solution]
 
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
@@ -770,8 +708,15 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf solution
-    reportWF preDefs wf
+    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)) varNamess rcs

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 <| resolveGlobalConstWithInfos 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 <| resolveGlobalConstWithInfos 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 <| resolveGlobalConstWithInfos id
+  let cs ← resolveGlobalConstWithInfos id
   cs.forM printEqnsOf
 
 end Lean.Elab.Command

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/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 => resolveGlobalConstNoOverloadWithInfo stx
+  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
   let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 

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 => resolveGlobalConstNoOverloadWithInfo 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/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 (← resolveGlobalConstNoOverload' 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,7 +51,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             x symm term
           else
             -- Try to get equation theorems for `id`.
-            let declName ← try resolveGlobalConstNoOverload' 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}'"

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 (← resolveGlobalConst' 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/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 ← resolveGlobalConstNoOverload' 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 ← resolveGlobalConstNoOverload' declName
     let dsimp ← checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc

src/Lean/Elab/Term.lean

@@ -793,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
@@ -1432,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

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/Message.lean

@@ -366,7 +366,6 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   | appTypeMismatch  env lctx e fnType argType =>
     mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}"
   | invalidProj env lctx e              => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}"
-  | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{constName}' is not a proposition{indentExpr type}"
   | other msg                           => m!"(kernel) {msg}"
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"

src/Lean/Meta.lean

@@ -48,4 +48,3 @@ import Lean.Meta.Iterator
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
 import Lean.Meta.CheckTactic
-import Lean.Meta.Canonicalizer

src/Lean/Meta/Canonicalizer.lean

@@ -1,146 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Util.ShareCommon
-import Lean.Data.HashMap
-import Lean.Meta.Basic
-import Lean.Meta.FunInfo
-
-namespace Lean.Meta
-namespace Canonicalizer
-
-/-!
-Applications have implicit arguments. Thus, two terms that may look identical when pretty-printed can be structurally different.
-For example, `@id (Id Nat) x` and `@id Nat x` are structurally different but are both pretty-printed as `id x`.
-Moreover, these two terms are definitionally equal since `Id Nat` reduces to `Nat`. This may create situations
-that are counterintuitive to our users. Furthermore, several tactics (e.g., `omega`) need to collect unique atoms in a goal.
-One simple approach is to maintain a list of atoms found so far, and whenever a new atom is discovered, perform a
-linear scan to test whether it is definitionally equal to a previously found one. However, this method is too costly,
-even if the definitional equality test were inexpensive.
-
-This module aims to efficiently identify terms that are structurally different, definitionally equal, and structurally equal
-when we disregard implicit arguments like `@id (Id Nat) x` and `@id Nat x`. The procedure is straightforward. For each atom,
-we create a new abstracted atom by erasing all implicit information. We refer to this abstracted atom as a 'key.' For the two
-terms mentioned, the key would be `@id _ x`, where `_` denotes a placeholder for a dummy term. To preserve any
-pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while constructing the key, we employ
-unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from keys to lists of terms, where each
-list contains terms sharing the same key but not definitionally equal. We posit that these lists will be small in practice.
--/
-
-/--
-Auxiliary structure for creating a pointer-equality mapping from `Expr` to `Key`.
-We use this mapping to ensure we preserve the dag-structure of input expressions.
--/
-structure ExprVisited where
-  e : Expr
-  deriving Inhabited
-
-unsafe instance : BEq ExprVisited where
-  beq a b := ptrAddrUnsafe a == ptrAddrUnsafe b
-
-unsafe instance : Hashable ExprVisited where
-  hash a := USize.toUInt64 (ptrAddrUnsafe a)
-
-abbrev Key := ExprVisited
-
-/--
-State for the `CanonM` monad.
--/
-structure State where
-  /-- "Set" of all keys created so far. This is a hash-consing helper structure available in Lean. -/
-  keys       : ShareCommon.State.{0} Lean.ShareCommon.objectFactory := ShareCommon.State.mk Lean.ShareCommon.objectFactory
-  /-- Mapping from `Expr` to `Key`. See comment at `ExprVisited`. -/
-  -- We use `HashMapImp` to ensure we don't have to tag `State` as `unsafe`.
-  cache      : HashMapImp ExprVisited Key := mkHashMapImp
-  /--
-  Given a key `k` and `keyToExprs.find? k = some es`, we have that all `es` share key `k`, and
-  are not definitionally equal modulo the transparency setting used. -/
-  keyToExprs : HashMapImp Key (List Expr) := mkHashMapImp
-
-instance : Inhabited State where
-  default := {}
-
-abbrev CanonM := ReaderT TransparencyMode $ StateRefT State MetaM
-
-/--
-The definitionally equality tests are performed using the given transparency mode.
-We claim `TransparencyMode.instances` is a good setting for most applications.
--/
-def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) : MetaM α :=
-  StateRefT'.run' (x transparency) {}
-
-private def shareCommon (a : α) : CanonM α :=
-  modifyGet fun { keys, cache, keyToExprs } =>
-    let (a, keys) := ShareCommon.State.shareCommon keys a
-    (a, { keys, cache, keyToExprs })
-
-private partial def mkKey (e : Expr) : CanonM Key := do
-  if let some key := unsafe (← get).cache.find? { e } then
-    return key
-  else
-    let key ← match e with
-      | .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. =>
-        pure { e := (← shareCommon e) }
-      | .mvar .. =>
-        -- We instantiate assigned metavariables because the
-        -- pretty-printer also instantiates them.
-        let eNew ← instantiateMVars e
-        if eNew == e then pure { e := (← shareCommon e) }
-        else mkKey eNew
-      | .mdata _ a => mkKey a
-      | .app .. =>
-        let f := (← mkKey e.getAppFn).e
-        if f.isMVar then
-          let eNew ← instantiateMVars e
-          unless eNew == e do
-            return (← mkKey eNew)
-        let info ← getFunInfo f
-        let args ← e.getAppArgs.mapIdxM fun i arg => do
-          if h : i < info.paramInfo.size then
-            let info := info.paramInfo[i]
-            if info.isExplicit then
-              pure (← mkKey arg).e
-            else
-              pure (mkSort 0) -- some dummy value for erasing implicit
-          else
-            pure (← mkKey arg).e
-        pure { e := (← shareCommon (mkAppN f args)) }
-      | .lam n t b i =>
-        pure { e := (← shareCommon (.lam n (← mkKey t).e (← mkKey b).e i)) }
-      | .forallE n t b i =>
-        pure { e := (← shareCommon (.forallE n (← mkKey t).e (← mkKey b).e i)) }
-      | .letE n t v b d =>
-        pure { e := (← shareCommon (.letE n (← mkKey t).e (← mkKey v).e (← mkKey b).e d)) }
-      | .proj t i s =>
-        pure { e := (← shareCommon (.proj t i (← mkKey s).e)) }
-    unsafe modify fun { keys, cache, keyToExprs} => { keys, keyToExprs, cache := cache.insert { e } key |>.1 }
-    return key
-
-/--
-"Canonicalize" the given expression.
--/
-def canon (e : Expr) : CanonM Expr := do
-  let k ← mkKey e
-  -- Find all expressions canonicalized before that have the same key.
-  if let some es' := unsafe (← get).keyToExprs.find? k then
-    withTransparency (← read) do
-      for e' in es' do
-        -- Found an expression `e'` that is definitionally equal to `e` and share the same key.
-        if (← isDefEq e e') then
-          return e'
-      -- `e` is not definitionally equal to any expression in `es'`. We claim this should be rare.
-      unsafe modify fun { keys, cache, keyToExprs } => { keys, cache, keyToExprs := keyToExprs.insert k (e :: es') |>.1 }
-      return e
-  else
-    -- `e` is the first expression we found with key `k`.
-    unsafe modify fun { keys, cache, keyToExprs } => { keys, cache, keyToExprs := keyToExprs.insert k [e] |>.1 }
-    return e
-
-end Canonicalizer
-
-export Canonicalizer (CanonM canon)
-
-end Lean.Meta

src/Lean/Meta/DiscrTree.lean

@@ -69,36 +69,21 @@ instance : LT Key := ⟨fun a b => Key.lt a b⟩
 instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
 
 def Key.format : Key → Format
-  | .star            => "*"
-  | .other           => "◾"
-  | .lit (.natVal v) => Std.format v
-  | .lit (.strVal v) => repr v
-  | .const k _       => Std.format k
-  | .proj s i _      => Std.format s ++ "." ++ Std.format i
-  | .fvar k _        => Std.format k.name
-  | .arrow           => "→"
+  | .star                   => "*"
+  | .other                  => "◾"
+  | .lit (Literal.natVal v) => Std.format v
+  | .lit (Literal.strVal v) => repr v
+  | .const k _              => Std.format k
+  | .proj s i _             => Std.format s ++ "." ++ Std.format i
+  | .fvar k _               => Std.format k.name
+  | .arrow                  => "→"
 
 instance : ToFormat Key := ⟨Key.format⟩
 
 def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a
-  /-
-  Remark: `.arrow` used to have arity 2, and was used to encode non-dependent arrows.
-  However, this feature was a recurrent source of bugs. For example, a theorem about
-  a dependent arrow can be applied to a non-dependent one. The reverse direction may
-  also happen. See issue #2835.
-  ```
-  -- A theorem about the non-dependent arrow `a → a`
-  theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
-
-  -- can be applied to the dependent one `(h : P a) → P (f h)`.
-  example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
-    simp only [imp_self']
-  ```
-  Thus, we now index dependent and non-dependent arrows using the key `.arrow` with arity 0.
-  -/
-  | .arrow      => 0
+  | .arrow      => 2
   | .proj _ _ a => 1 + a
   | _           => 0
 
@@ -285,12 +270,39 @@ partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
 -/
 private def isBadKey (fn : Expr) : Bool :=
   match fn with
-  | .lit ..     => false
-  | .const ..   => false
-  | .fvar ..    => false
-  | .proj ..    => false
-  | .forallE .. => false
-  | _           => true
+  | .lit ..   => false
+  | .const .. => false
+  | .fvar ..  => false
+  | .proj ..  => false
+  | .forallE _ _ b _ => b.hasLooseBVars
+  | _ => true
+
+/--
+  Try to eliminate loose bound variables by performing beta-reduction.
+  We use this method when processing terms in discrimination trees.
+  These trees distinguish dependent arrows from nondependent ones.
+  Recall that dependent arrows are indexed as `.other`, but nondependent arrows as `.arrow ..`.
+  Motivation: we want to "discriminate" implications and simple arrows in our index.
+
+  Now suppose we add the term `Foo (Nat → Nat)` to our index. The nested arrow appears as
+  `.arrow ..`. Then, suppose we want to check whether the index contains
+  `(x : Nat) → (fun _ => Nat) x`, but it will fail to retrieve `Foo (Nat → Nat)` because
+  it assumes the nested arrow is a dependent one and uses `.other`.
+
+  We use this method to address this issue by beta-reducing terms containing loose bound variables.
+  See issue #2232.
+
+  Remark: we expect the performance impact will be minimal.
+-/
+private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
+  Core.transform e
+    (pre := fun e => do
+      if !e.hasLooseBVars then
+        return .done e
+      else if e.isHeadBetaTarget then
+        return .visit e.headBeta
+      else
+        return .continue)
 
 /--
   Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
@@ -314,6 +326,7 @@ def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
+
 /--
 Append `n` wildcards to `todo`
 -/
@@ -377,8 +390,15 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
         return (.other, todo)
       else
         return (.star, todo)
-    | .forallE .. => return (.arrow, todo)
-    | _ => return (.other, todo)
+    | .forallE _ d b _ =>
+      -- See comment at elimLooseBVarsByBeta
+      let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
+      if b.hasLooseBVars then
+        return (.other, todo)
+      else
+        return (.arrow, todo.push d |>.push b)
+    | _ =>
+      return (.other, todo)
 
 @[inherit_doc pushArgs]
 partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
@@ -536,8 +556,15 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .proj s i a .. =>
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE .. => return (.arrow, #[])
-  | _ => return (.other, #[])
+  | .forallE _ d b _ =>
+    -- See comment at elimLooseBVarsByBeta
+    let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
+    if b.hasLooseBVars then
+      return (.other, #[])
+    else
+      return (.arrow, #[d, b])
+  | _ =>
+    return (.other, #[])
 
 private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
   getKeyArgs e (isMatch := true) (root := root) (config := config)
@@ -581,6 +608,12 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       let result ← visitStar result
       match k with
       | .star  => return result
+      /-
+        Note: dep-arrow vs arrow
+        Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are `(Key.arrow, #[a, b])`.
+        A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`). Thus, we also visit the `Key.other` child.
+      -/
+      | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
       | _      => visitNonStar k args result
 
 private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) :=
@@ -594,6 +627,8 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig)
     let (k, args) ← getMatchKeyArgs e (root := true) config
     match k with
     | .star  => return (k, result)
+    /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
+    | .arrow => return (k, (← getMatchRoot d k args (← getMatchRoot d .other #[] result config) config))
     | _      => return (k, (← getMatchRoot d k args result config))
 
 /--
@@ -673,6 +708,8 @@ where
           | some c => process 0 (todo ++ args) c.2 result
         match k with
         | .star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
+        -- See comment a `getMatch` regarding non-dependent arrows vs dependent arrows
+        | .arrow => visitNonStar .other #[] (← visitNonStar k args (← visitStar result))
         | _      => visitNonStar k args (← visitStar result)
 
 namespace Trie

src/Lean/Meta/Eqns.lean

@@ -4,65 +4,46 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.ReservedNameAction
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
-/--
-Returns `true` if  `name` is of the form `f.def` and `f.eq_<idx>` where `f` is a safe definition.
--/
-def isEqnReservedName (env : Environment) (name : Name) : Bool :=
-  match name with
-  | .str p s =>
-    if s == "def" then
-      env.isSafeDefinition p
-    else if "eq_".isPrefixOf s && (s.drop 3).isNat then
-      env.isSafeDefinition p
-    else
-      false
-  | _ => false
-
-/--
-Ensures that `f.def` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
--/
-builtin_initialize registerReservedNamePredicate isEqnReservedName
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))
 
 private builtin_initialize getEqnsFnsRef : IO.Ref (List GetEqnsFn) ← IO.mkRef []
 
 /--
-Registers a new function for retrieving equation theorems.
-We generate equations theorems on demand, and they are generated by more than one module.
-For example, the structural and well-founded recursion modules generate them.
-Most recent getters are tried first.
+  Register a new function for retrieving equation theorems.
+  We generate equations theorems on demand, and they are generated by more than one module.
+  For example, the structural and well-founded recursion modules generate them.
+  Most recent getters are tried first.
 
-A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
-Otherwise, it is a sequence of theorem names where each one of them corresponds to
-an alternative. Example: the definition
+  A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
+  Otherwise, it is a sequence of theorem names where each one of them corresponds to
+  an alternative. Example: the definition
 
-```
-def f (xs : List Nat) : List Nat :=
-  match xs with
-  | [] => []
-  | x::xs => (x+1)::f xs
-```
-should have two equational theorems associated with it
-```
-f [] = []
-```
-and
-```
-(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
-```
+  ```
+  def f (xs : List Nat) : List Nat :=
+    match xs with
+    | [] => []
+    | x::xs => (x+1)::f xs
+  ```
+  should have two equational theorems associated with it
+  ```
+  f [] = []
+  ```
+  and
+  ```
+  (x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
+  ```
 -/
 def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
   getEqnsFnsRef.modify (f :: ·)
 
-/-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
+/-- Return true iff `declName` is a definition and its type is not a proposition. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     return !(← isProp info.type)
@@ -79,15 +60,15 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {})
 
 /--
-Simple equation theorem for nonrecursive definitions.
+  Simple equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) (suffix := `def) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
       let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)
-      let name := declName ++ suffix
+      let name := mkPrivateName (← getEnv) declName ++ `_eq_1
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
@@ -112,9 +93,9 @@ private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit
   }
 
 /--
-Returns equation theorems for the given declaration.
-By default, we do not create equation theorems for nonrecursive definitions.
-You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
+  Returns equation theorems for the given declaration.
+  By default, we do not create equation theorems for nonrecursive definitions.
+  You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
 def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do
   if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
@@ -136,29 +117,29 @@ def GetUnfoldEqnFn := Name → MetaM (Option Name)
 private builtin_initialize getUnfoldEqnFnsRef : IO.Ref (List GetUnfoldEqnFn) ← IO.mkRef []
 
 /--
-Registers a new function for retrieving a "unfold" equation theorem.
+  Register a new function for retrieving a "unfold" equation theorem.
 
-We generate this kind of equation theorem on demand, and it is generated by more than one module.
-For example, the structural and well-founded recursion modules generate it.
-Most recent getters are tried first.
+  We generate this kind of equation theorem on demand, and it is generated by more than one module.
+  For example, the structural and well-founded recursion modules generate it.
+  Most recent getters are tried first.
 
-A getter returns an `Option Name`. The result is `none` if the getter failed.
-Otherwise, it is a theorem name. Example: the definition
+  A getter returns an `Option Name`. The result is `none` if the getter failed.
+  Otherwise, it is a theorem name. Example: the definition
 
-```
-def f (xs : List Nat) : List Nat :=
-  match xs with
-  | [] => []
-  | x::xs => (x+1)::f xs
-```
-should have the theorem
-```
-(xs : Nat) →
-  f xs =
+  ```
+  def f (xs : List Nat) : List Nat :=
     match xs with
     | [] => []
     | x::xs => (x+1)::f xs
-```
+  ```
+  should have the theorem
+  ```
+  (xs : Nat) →
+    f xs =
+      match xs with
+      | [] => []
+      | x::xs => (x+1)::f xs
+  ```
 -/
 def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   unless (← initializing) do
@@ -180,11 +161,4 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
       return some eqThm
    return none
 
-builtin_initialize
-  registerReservedNameAction fun name => do
-    if isEqnReservedName (← getEnv) name then
-      throwError "Eqn action is WIP"
-    else
-      return false
-
 end Lean.Meta

src/Lean/Meta/SynthInstance.lean

@@ -321,26 +321,6 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
     subgoals := inst.synthOrder.map (mvars[·]!) |>.toList
   }
 
-/--
-Similar to `mkLambdaFVars`, but ensures result is eta-reduced.
-For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
-the result is `inst` instead of `fun x y => inst x y`.
-
-We added this auxiliary function because of aliases such as `DecidablePred`. For example,
-consider the following definition.
-```
-def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
-  match xs with
-  | [] => []
-  | x :: xs' => if p x then x :: filter p xs' else filter p xs'
-```
-Without `mkLambdaFVars'`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
-Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
-we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
--/
-private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
-  return (← mkLambdaFVars xs e).eta
-
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.
   Remark: `mctx` is set using `withMCtx`.
@@ -355,7 +335,7 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
-      let instVal ← mkLambdaFVars' xs instVal
+      let instVal ← mkLambdaFVars xs instVal
       if (← isDefEq mvar instVal) then
         return some ((← getMCtx), subgoals)
     return none
@@ -468,7 +448,7 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
         let ys := ys.toArray
         let mvarType' ← mkForallFVars ys body
         withLocalDeclD `redf mvarType' fun f => do
-          let transformer ← mkLambdaFVars' #[f] (← mkLambdaFVars' xs (mkAppN f ys))
+          let transformer ← mkLambdaFVars #[f] (← mkLambdaFVars xs (mkAppN f ys))
           trace[Meta.synthInstance.unusedArgs] "{mvarType}\nhas unused arguments, reduced type{indentExpr mvarType'}\nTransformer{indentExpr transformer}"
           return some (mvarType', transformer)
 

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -123,18 +123,17 @@ where
       return (implicits, targets')
 
 structure CustomEliminator where
-  induction : Bool
   typeNames : Array Name
   elimName  : Name -- NB: Do not store the ElimInfo, it can contain MVars
   deriving Inhabited, Repr
 
 structure CustomEliminators where
-  map : SMap (Bool × Array Name) Name := {}
+  map : SMap (Array Name) Name := {}
   deriving Inhabited, Repr
 
 def addCustomEliminatorEntry (es : CustomEliminators) (e : CustomEliminator) : CustomEliminators :=
   match es with
-  | { map := map } => { map := map.insert (e.induction, e.typeNames) e.elimName }
+  | { map := map } => { map := map.insert e.typeNames e.elimName }
 
 builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminator CustomEliminators ←
   registerSimpleScopedEnvExtension {
@@ -143,7 +142,7 @@ builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminat
     finalizeImport := fun { map := map } => { map := map.switch }
   }
 
-def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomEliminator := do
+def mkCustomEliminator (elimName : Name) : MetaM CustomEliminator := do
   let elimInfo ← getElimInfo elimName
   let info ← getConstInfo elimName
   forallTelescopeReducing info.type fun xs _ => do
@@ -165,46 +164,29 @@ def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomElimin
         let xType ← inferType x
         let .const typeName .. := xType.getAppFn | throwError "unexpected eliminator target type{indentExpr xType}"
         typeNames := typeNames.push typeName
-    return { induction, typeNames, elimName }
+    return { typeNames, elimName}
 
-def addCustomEliminator (declName : Name) (attrKind : AttributeKind) (induction : Bool) : MetaM Unit := do
-  let e ← mkCustomEliminator declName induction
+def addCustomEliminator (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  let e ← mkCustomEliminator declName
   customEliminatorExt.add e attrKind
 
 builtin_initialize
   registerBuiltinAttribute {
-    name  := `induction_eliminator
-    descr := "custom `rec`-like eliminator for the `induction` tactic"
+    name  := `eliminator
+    descr := "custom eliminator for `cases` and `induction` tactics"
     add   := fun declName _ attrKind => do
-      discard <| addCustomEliminator declName attrKind (induction := true) |>.run {} {}
+      discard <| addCustomEliminator declName attrKind |>.run {} {}
   }
 
-builtin_initialize
-  registerBuiltinAttribute {
-    name  := `cases_eliminator
-    descr := "custom `casesOn`-like eliminator for the `cases` tactic"
-    add   := fun declName _ attrKind => do
-      discard <| addCustomEliminator declName attrKind (induction := false) |>.run {} {}
-  }
-
-/-- Gets all the eliminators defined using the `@[induction_eliminator]` and `@[cases_eliminator]` attributes. -/
 def getCustomEliminators : CoreM CustomEliminators := do
   return customEliminatorExt.getState (← getEnv)
 
-/--
-Gets an eliminator appropriate for the provided array of targets.
-If `induction` is `true` then returns a matching eliminator defined using the `@[induction_eliminator]` attribute
-and otherwise returns one defined using the `@[cases_eliminator]` attribute.
-
-The `@[induction_eliminator]` attribute is for the `induction` tactic
-and the `@[cases_eliminator]` attribute is for the `cases` tactic.
--/
-def getCustomEliminator? (targets : Array Expr) (induction : Bool) : MetaM (Option Name) := do
+def getCustomEliminator? (targets : Array Expr) : MetaM (Option Name) := do
   let mut key := #[]
   for target in targets do
     let targetType := (← instantiateMVars (← inferType target)).headBeta
     let .const declName .. := targetType.getAppFn | return none
     key := key.push declName
-  return customEliminatorExt.getState (← getEnv) |>.map.find? (induction, key)
+  return customEliminatorExt.getState (← getEnv) |>.map.find? key
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -50,10 +50,6 @@ def foldRawNatLit (e : Expr) : SimpM Expr := do
       return toExpr n
   | none   => return e
 
-/-- Return true if `e` is of the form `ofScientific n b m` where `n` and `m` are kernel Nat literals. -/
-def isOfScientificLit (e : Expr) : Bool :=
-  e.isAppOfArity ``OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit
-
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -414,27 +410,19 @@ private def dsimpReduce : DSimproc := fun e => do
     eNew ← reduceFVar (← getConfig) (← getSimpTheorems) eNew
   if eNew != e then return .visit eNew else return .done e
 
-/-- Helper `dsimproc` for `doNotVisitOfNat` and `doNotVisitOfScientific` -/
-private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fun e => do
-  if pred e then
-    if (← readThe Simp.Context).isDeclToUnfold declName then
-      return .continue e
-    else
-      return .done e
-  else
-    return .continue e
-
 /--
 Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
 This is the `dsimp` equivalent of the approach used at `visitApp`.
 Recall that we fold orphan raw Nat literals.
 -/
-private def doNotVisitOfNat : DSimproc := doNotVisit isOfNatNatLit ``OfNat.ofNat
-
-/--
-Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
--/
-private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
+private def doNotVisitOfNat : DSimproc := fun e => do
+  if isOfNatNatLit e then
+    if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then
+      return .continue e
+    else
+      return .done e
+  else
+    return .continue e
 
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
@@ -442,7 +430,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   unless cfg.dsimp do
     return e
   let m ← getMethods
-  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific
+  let pre := m.dpre >> doNotVisitOfNat
   let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -562,8 +550,8 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  if isOfNatNatLit e || isOfScientificLit e then
-    -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
+  if isOfNatNatLit e then
+    -- Recall that we expand "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else
     congr e

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -285,7 +285,7 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
   /-
-  If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
+  If `thmId` is an equational theorem (e.g., `foo._eq_1`), we should record `foo` instead.
   See issue #3547.
   -/
   let thmId ← match thmId with

src/Lean/Parser/Term.lean

@@ -97,6 +97,55 @@ end Tactic
 def darrow : Parser := " => "
 def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
 
+namespace Termination
+
+/-
+Termination suffix parsers, typically thought of as part of a command, but due to
+letrec we need them here already.
+-/
+
+/--
+Specify a termination argument for well-founded termination:
+```
+termination_by a - b
+```
+indicates that termination of the currently defined recursive function follows
+because the difference between the the arguments `a` and `b`.
+
+If the fuction takes further argument after the colon, you can name them as follows:
+```
+def example (a : Nat) : Nat → Nat → Nat :=
+termination_by b c => a - b
+```
+
+If omitted, a termination argument will be inferred. If written as `termination_by?`,
+the inferrred termination argument will be suggested.
+-/
+def terminationBy := leading_parser
+  "termination_by " >>
+  optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
+  termParser
+
+@[inherit_doc terminationBy]
+def terminationBy? := leading_parser
+  "termination_by?"
+
+/--
+Manually prove that the termination argument (as specified with `termination_by` or inferred)
+decreases at each recursive call.
+
+By default, the tactic `decreasing_tactic` is used.
+-/
+def decreasingBy := leading_parser
+  ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
+
+/--
+Termination hints are `termination_by` and `decreasing_by`, in that order.
+-/
+def suffix := leading_parser
+  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
+
+end Termination
 
 namespace Term
 
@@ -547,59 +596,6 @@ def attrInstance     := ppGroup $ leading_parser attrKind >> attrParser
 
 def attributes       := leading_parser
   "@[" >> withoutPosition (sepBy1 attrInstance ", ") >> "] "
-
-end Term
-namespace Termination
-
-/-
-Termination suffix parsers, typically thought of as part of a command, but due to
-letrec we need them here already.
--/
-
-/--
-Specify a termination argument for well-founded termination:
-```
-termination_by a - b
-```
-indicates that termination of the currently defined recursive function follows
-because the difference between the the arguments `a` and `b`.
-
-If the fuction takes further argument after the colon, you can name them as follows:
-```
-def example (a : Nat) : Nat → Nat → Nat :=
-termination_by b c => a - b
-```
-
-If omitted, a termination argument will be inferred. If written as `termination_by?`,
-the inferrred termination argument will be suggested.
--/
-def terminationBy := leading_parser
-  "termination_by " >>
-  optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >>
-  termParser
-
-@[inherit_doc terminationBy]
-def terminationBy? := leading_parser
-  "termination_by?"
-
-/--
-Manually prove that the termination argument (as specified with `termination_by` or inferred)
-decreases at each recursive call.
-
-By default, the tactic `decreasing_tactic` is used.
--/
-def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
-
-/--
-Termination hints are `termination_by` and `decreasing_by`, in that order.
--/
-def suffix := leading_parser
-  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
-
-end Termination
-namespace Term
-
 /-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
 a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
 def letRecDecl       := leading_parser

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1082,85 +1082,41 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options)
 @[implemented_by evalSyntaxConstantUnsafe]
 private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
 
-/--
-Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`.
-
-If `universes` is `false`, then the universe level parameters are omitted.
--/
-partial def delabConstWithSignature (universes : Bool := true) : Delab := do
+/-- Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`. -/
+partial def delabConstWithSignature : Delab := do
   let e ← getExpr
   -- use virtual expression node of arity 2 to separate name and type info
   let idStx ← descend e 0 <|
-    withOptions (pp.universes.set · universes |> (pp.fullNames.set · true)) <|
+    withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
       delabConst
   descend (← inferType e) 1 <|
-    delabParams {} idStx #[]
+    delabParams idStx #[] #[]
 where
-  /--
-  For types in the signature, we want to be sure pi binder types are pretty printed.
-  -/
-  delabTy : DelabM Term := withOptions (pp.piBinderTypes.set · true) delab
-  /-
-  Similar to `delabBinders`, but does not uniquify binder names (since for named arguments we want to know the name),
-  and it always merges binder groups when possible.
-  Once it reaches a binder with an inaccessible name, or a name that has already been used,
-  the remaining binders appear in pi types after the `:` of the declaration.
-  -/
-  delabParams (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) := do
-    let e ← getExpr
-    if e.isForall && e.binderInfo.isInstImplicit && e.bindingName!.hasMacroScopes then
-      -- Assumption: this instance can be found by instance search, so it does not need to be named.
-      -- The oversight here is that this inaccessible name can appear in the pretty printed expression.
-      -- We could check to see whether the instance appears in the type and avoid omitting the instance name,
-      -- but this would be the usual case.
-      let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)])
-      withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group)
-    else if e.isForall && !e.bindingName!.hasMacroScopes && !bindingNames.contains e.bindingName! then
-      delabParamsAux bindingNames idStx groups #[]
+  -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
+  delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
+    if let .forallE n d _ i ← getExpr then
+      let stxN ← annotateCurPos (mkIdent n)
+      let curIds := curIds.push ⟨stxN⟩
+      if ← shouldGroupWithNext then
+        withBindingBody n <| delabParams idStx groups curIds
+      else
+        let delabTy := withOptions (pp.piBinderTypes.set · true) delab
+        let group ← withBindingDomain do
+          match i with
+          | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
+          | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
+          | .instImplicit   => `(bracketedBinderF|[$curIds.back : $(← delabTy)])
+          | _ =>
+            if d.isOptParam then
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+            else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+              let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+            else
+              `(bracketedBinderF|($curIds* : $(← delabTy)))
+        withBindingBody n <| delabParams idStx (groups.push group) #[]
     else
-      let type ← delabTy
+      let type ← delab
       `(declSigWithId| $idStx:ident $groups* : $type)
-  /--
-  Inner loop for `delabParams`, collecting binders.
-  Invariants:
-  - The current expression is a forall.
-  - It has a name that's not inaccessible.
-  - It has a name that hasn't been used yet.
-  -/
-  delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
-    let e@(.forallE n d e' i) ← getExpr | unreachable!
-    let bindingNames := bindingNames.insert n
-    let stxN := mkIdent n
-    let curIds := curIds.push ⟨stxN⟩
-    if shouldGroupWithNext bindingNames e e' then
-      withBindingBody n <| delabParamsAux bindingNames idStx groups curIds
-    else
-      let group ← withBindingDomain do
-        match i with
-        | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
-        | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
-        | .instImplicit   => `(bracketedBinderF|[$stxN : $(← delabTy)])
-        | _ =>
-          if d.isOptParam then
-            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
-          else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
-            let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
-            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
-          else
-            `(bracketedBinderF|($curIds* : $(← delabTy)))
-      withBindingBody n <| delabParams bindingNames idStx (groups.push group)
-  /-
-  Given the forall `e` with body `e'`, determines if the binder from `e'` (if it is a forall) should be grouped with `e`'s binder.
-  -/
-  shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool :=
-    e'.isForall &&
-    -- At the first sign of an inaccessible name, stop merging binders:
-    !e'.bindingName!.hasMacroScopes &&
-    -- If it's a name that has already been used, stop merging binders:
-    !bindingNames.contains e'.bindingName! &&
-    e.binderInfo == e'.binderInfo &&
-    e.bindingDomain! == e'.bindingDomain! &&
-    -- Inst implicits can't be grouped:
-    e'.binderInfo != BinderInfo.instImplicit
 
 end Lean.PrettyPrinter.Delaborator

src/Lean/ReservedNameAction.lean

@@ -1,79 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.CoreM
-
-namespace Lean
-
-/--
-When trying to resolve a reserved name, an action can be executed to generate the actual definition/theorem.
-The action returns `true` if it "handled" the given name.
-
-Remark: usually when one install a reserved name predicate, an associated action is also installed.
--/
-def ReservedNameAction := Name → CoreM Bool
-
-private builtin_initialize reservedNameActionsRef : IO.Ref (Array ReservedNameAction) ← IO.mkRef #[]
-
-/--
-Register a new function that is invoked when trying to resolve a reserved name.
--/
-def registerReservedNameAction (act : ReservedNameAction) : IO Unit := do
-  unless (← initializing) do
-    throw (IO.userError "failed to register reserved name action, this kind of extension can only be registered during initialization")
-  reservedNameActionsRef.modify (·.push act)
-
-/--
-Execute a registered reserved action for the given reserved name.
-The result is `true` if a handler for the given reserved name was found.
-Note that the handler can throw an exception.
--/
-def executeReservedNameAction (name : Name) : CoreM Bool := do
-  for act in (← reservedNameActionsRef.get) do
-    if (← act name) then
-      return true
-  return false
-
-/--
-Similar to `resolveGlobalName`, but also executes reserved name actions.
--/
-def resolveGlobalName' (id : Name) : CoreM (List (Name × List String)) := do
-  let cs ← resolveGlobalName id
-  for (c, _) in cs do
-    unless (← getEnv).contains c do
-      if (← executeReservedNameAction c) then
-        unless (← getEnv).contains c do
-          throwError "'{id}' is a reserved name, but reserved name code generator failed"
-      else
-        throwError "'{id}' is a reserved name, but none of the installed reserved name code generators is applicable"
-  return cs
-
-/--
-Similar to `resolveGlobalConstCore`, but also executes reserved name actions.
--/
-def resolveGlobalConstCore' (n : Name) : CoreM (List Name) := do
-  let cs ← resolveGlobalName' n
-  filterFieldList n cs
-
-/--
-Similar to `resolveGlobalConstNoOverloadCore`, but also executes reserved name actions.
--/
-def resolveGlobalConstNoOverloadCore' (n : Name) : CoreM Name := do
-  ensureNoOverload n (← resolveGlobalConstCore' n)
-
-/--
-Similar to `resolveGlobalConst`, but also executes reserved name actions.
--/
-def resolveGlobalConst' (stx : Syntax) : CoreM (List Name) :=
-  preprocessSyntaxAndResolve stx resolveGlobalConstCore'
-
-/--
-Similar to `resolveGlobalConstNoOverload`, but also executes reserved name actions.
--/
-def resolveGlobalConstNoOverload' (id : Syntax) : CoreM Name := do
-  ensureNonAmbiguous id (← resolveGlobalConst' id)
-
-end Lean

src/Lean/ResolveName.lean

@@ -10,36 +10,6 @@ import Lean.Modifiers
 import Lean.Exception
 
 namespace Lean
-/-!
-Reserved names.
-
-We use reserved names for automatically generated theorems (e.g., equational theorems).
-Automation may register new reserved name predicates. In this model, we just check the
-registered predicates, but do not trigger actions associated with them. For example,
-give a definition `foo`, we have the reserved name `foo.def` associated with it, and
-an action for creating a theorem that states that `foo` is equal to its definition.
--/
-
-/-- Global reference containing all reserved name predicates. -/
-builtin_initialize reservedNamePredicatesRef : IO.Ref (Array (Environment → Name → Bool)) ← IO.mkRef #[]
-
-/--
-Registers a new reserved name predicate.
--/
-def registerReservedNamePredicate (p : Environment → Name → Bool) : IO Unit := do
-  unless (← initializing) do
-    throw (IO.userError "failed to reserved name predicate, this operation can only be performed during initialization")
-  reservedNamePredicatesRef.modify fun ps => ps.push p
-
-builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment → Name → Bool)) ←
-  registerEnvExtension reservedNamePredicatesRef.get
-
-/--
-Returns `true` if `name` is a reserved name.
--/
-def isReservedName (env : Environment) (name : Name) : Bool :=
-  reservedNamePredicatesExt.getState env |>.any (· env name)
-
 /-!
   We use aliases to implement the `export <id> (<id>+)` command.
   An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`.
@@ -143,13 +113,6 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl →
         resolvedIds
     resolveOpenDecls env id openDecls resolvedIds
 
-/--
-Primitive global name resolution procedure. It does 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.
--/
 def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
   -- decode macro scopes from name before recursion
   let extractionResult := extractMacroScopes id
@@ -164,9 +127,9 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
         match resolveExact env id with
         | some newId => [(newId, projs)]
         | none =>
-          let resolvedIds := if env.contains id || isReservedName env id then [id] else []
+          let resolvedIds := if env.contains id then [id] else []
           let idPrv       := mkPrivateName env id
-          let resolvedIds := if env.contains idPrv || isReservedName env idPrv then [idPrv] ++ resolvedIds else resolvedIds
+          let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
           let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
           let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds
           match resolvedIds with
@@ -220,27 +183,27 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   getOpenDecls     := liftM (m:=m) getOpenDecls
 
 /--
-Given a name `n`, return a list of possible interpretations.
-Each interpretation is a pair `(declName, fieldList)`, where `declName`
-is the name of a declaration in the current environment, and `fieldList` are
-(potential) field names.
-The pair is needed because in Lean `.` may be part of a qualified name or
-a field (aka dot-notation).
-As an example, consider the following definitions
-```
-def Boo.x   := 1
-def Foo.x   := 2
-def Foo.x.y := 3
-```
-After `open Foo`, we have
-- `resolveGlobalName x`     => `[(Foo.x, [])]`
-- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
-- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`
+  Given a name `n`, return a list of possible interpretations.
+  Each interpretation is a pair `(declName, fieldList)`, where `declName`
+  is the name of a declaration in the current environment, and `fieldList` are
+  (potential) field names.
+  The pair is needed because in Lean `.` may be part of a qualified name or
+  a field (aka dot-notation).
+  As an example, consider the following definitions
+  ```
+  def Boo.x   := 1
+  def Foo.x   := 2
+  def Foo.x.y := 3
+  ```
+  After `open Foo`, we have
+  - `resolveGlobalName x`     => `[(Foo.x, [])]`
+  - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
+  - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`
 
-After `open Foo open Boo`, we have
-- `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
-- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
-- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
+  After `open Foo open Boo`, we have
+  - `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
+  - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
+  - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
 -/
 def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do
   return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
@@ -273,44 +236,24 @@ def resolveUniqueNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadErr
   | [ns] => return ns
   | nss => throwError s!"ambiguous namespace '{id.getId}', possible interpretations: '{nss}'"
 
-/-- Helper function for `resolveGlobalConstCore`. -/
-def filterFieldList [Monad m] [MonadError m] (n : Name) (cs : List (Name × List String)) : m (List Name) := do
-  let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
-  if cs.isEmpty then throwUnknownConstant n
-  return cs.map (·.1)
-
 /-- Given a name `n`, return a list of possible interpretations for global constants.
 
 Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty.
 For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/
-private def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do
+def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do
   let cs ← resolveGlobalName n
-  filterFieldList n cs
+  let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
+  if cs.isEmpty then throwUnknownConstant n
+  return cs.map (·.1)
 
-/-- Helper function for `resolveGlobalConstNoOverloadCore` -/
-def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Name := do
+/-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names. -/
+def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
+  let cs ← resolveGlobalConstCore n
   match cs with
   | [c] => pure c
   | _   => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
 
-/-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names. -/
-def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
-  ensureNoOverload n (← resolveGlobalConstCore n)
-
-def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
-  match stx with
-  | .ident _ _ n pre => do
-    let pre := pre.filterMap fun
-      | .decl n [] => some n
-      | _          => none
-    if pre.isEmpty then
-      withRef stx <| k n
-    else
-      return pre
-  | _ => throwErrorAt stx s!"expected identifier"
-
-/--
-Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
+/-- Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
 constant names that it could be referring to based on the currently open namespaces.
 This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax
 because `Syntax` objects may have names that have already been resolved.
@@ -331,8 +274,16 @@ After `open Foo open Boo`, we have
 - `resolveGlobalConst x.y`   => `[Foo.x.y]`
 - `resolveGlobalConst x.z.w` => error: unknown constant
 -/
-def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (List Name) :=
-  preprocessSyntaxAndResolve stx resolveGlobalConstCore
+def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m (List Name)
+  | stx@(Syntax.ident _ _ n pre) => do
+    let pre := pre.filterMap fun
+      | .decl n [] => some n
+      | _          => none
+    if pre.isEmpty then
+      withRef stx <| resolveGlobalConstCore n
+    else
+      return pre
+  | stx => throwErrorAt stx s!"expected identifier"
 
 /--
 Given a list of names produced by `resolveGlobalConst`, throw an error if the list does not contain

src/Lean/Util/Trace.lean

@@ -140,13 +140,16 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
     let msg ← mkMsg
     addTrace cls msg
 
+private def addTraceNodeCore (oldTraces : PersistentArray TraceElem)
+    (cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
+  modifyTraces fun newTraces =>
+    oldTraces.push { ref, msg := .trace cls msg (newTraces.toArray.map (·.msg)) collapsed }
+
 private def addTraceNode (oldTraces : PersistentArray TraceElem)
     (cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
   withRef ref do
-  let msg := .trace cls msg ((← getTraces).toArray.map (·.msg)) collapsed
   let msg ← addMessageContext msg
-  modifyTraces fun _ =>
-    oldTraces.push { ref, msg }
+  addTraceNodeCore oldTraces cls ref msg collapsed
 
 def withSeconds [Monad m] [MonadLiftT BaseIO m] (act : m α) : m (α × Float) := do
   let start ← IO.monoNanosNow
@@ -304,7 +307,6 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
     return (← k)
   let oldTraces ← getResetTraces
   let ref ← getRef
-  -- make sure to preserve context *before* running `k`
   let msg ← withRef ref do addMessageContext (← msg)
   let (res, secs) ← withSeconds <| observing k
   let aboveThresh := trace.profiler.get opts && secs > trace.profiler.threshold.getSecs opts
@@ -314,7 +316,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
   let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
   if profiler.get opts || aboveThresh then
     msg := m!"[{secs}s] {msg}"
-  addTraceNode oldTraces cls ref msg collapsed
+  addTraceNodeCore oldTraces cls ref msg collapsed
   MonadExcept.ofExcept res
 
 end Lean

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -164,7 +164,7 @@ where
       let more := chopUpChildren cls blockSize children[blockSize:]
       children[:blockSize].toArray.push <|
         .trace (collapsed := true) cls
-          f!"{children.size - blockSize} more entries..." more
+          f!"{dbgTraceVal <| children.size - blockSize} more entries..." more
     else children
 
 partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do

src/kernel/environment.cpp

@@ -178,8 +178,6 @@ environment environment::add_theorem(declaration const & d, bool check) const {
     if (check) {
         // TODO(Leo): we must add support for handling tasks here
         type_checker checker(*this);
-        if (!checker.is_prop(v.get_type()))
-            throw theorem_type_is_not_prop(*this, v.get_name(), v.get_type());
         check_constant_val(*this, v.to_constant_val(), checker);
         check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
         expr val_type = checker.check(v.get_value(), v.get_lparams());

src/kernel/kernel_exception.h

@@ -66,16 +66,6 @@ public:
     expr const & get_expr() const { return m_expr; }
 };
 
-class theorem_type_is_not_prop : public kernel_exception {
-    name m_name;
-    expr m_type;
-public:
-    theorem_type_is_not_prop(environment const & env, name const & n, expr const & type):
-        kernel_exception(env), m_name(n), m_type(type) {}
-    name const & get_decl_name() const { return m_name; }
-    expr const & get_type() const { return m_type; }
-};
-
 class kernel_exception_with_lctx : public kernel_exception {
     local_ctx m_lctx;
 public:
@@ -195,24 +185,21 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (invalid_proj_exception & ex) {
         // 10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
         return mk_cnstr(0, mk_cnstr(10, ex.env(), ex.get_local_ctx(), ex.get_proj())).steal();
-    } catch (theorem_type_is_not_prop & ex) {
-        // 11 | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr)
-        return mk_cnstr(0, mk_cnstr(11, ex.env(), ex.get_decl_name(), ex.get_type())).steal();
     } catch (exception & ex) {
-        // 12 | other            (msg : String)
-        return mk_cnstr(0, mk_cnstr(12, string_ref(ex.what()))).steal();
+        // 11 | other            (msg : String)
+        return mk_cnstr(0, mk_cnstr(11, string_ref(ex.what()))).steal();
     } catch (heartbeat_exception & ex) {
-        // 13 | deterministicTimeout
-        return mk_cnstr(0, box(13)).steal();
+        // 12 | deterministicTimeout
+        return mk_cnstr(0, box(12)).steal();
     } catch (memory_exception & ex) {
-        // 14 | excessiveMemory
-        return mk_cnstr(0, box(14)).steal();
+        // 13 | excessiveMemory
+        return mk_cnstr(0, box(13)).steal();
     } catch (stack_space_exception & ex) {
-        // 15 | deepRecursion
-        return mk_cnstr(0, box(15)).steal();
+        // 14 | deepRecursion
+        return mk_cnstr(0, box(14)).steal();
     } catch (interrupted & ex) {
-        // 16 | interrupted
-        return mk_cnstr(0, box(16)).steal();
+        // 15 | interrupted
+        return mk_cnstr(0, box(15)).steal();
     }
 }
 }

src/lake/Lake/Build/Monad.lean

@@ -17,7 +17,7 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : IO BuildContext :=
     toBuildConfig := config,
     startedBuilds := ← IO.mkRef 0
     finishedBuilds := ← IO.mkRef 0,
-    leanTrace := Hash.ofString ws.lakeEnv.leanGithash
+    leanTrace := Hash.ofString ws.lakeEnv.lean.githash
   }
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α

src/lake/Lake/Config/Env.lean

@@ -25,9 +25,7 @@ structure Env where
   lean : LeanInstall
   /-- The Elan installation (if any) of the environment. -/
   elan? : Option ElanInstall
-  /-- Overrides the detected Lean's githash as the string Lake uses for Lean traces. -/
-  githashOverride : String
-  /-- A name-to-URL mapping of URL overrides for the named packages. -/
+  /-- A name-to-URL mapping of URL overwrites for the named packages. -/
   pkgUrlMap : NameMap String
   /-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/
   initToolchain : String
@@ -48,7 +46,6 @@ def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstal
   return {
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
-    githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
     initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
@@ -62,17 +59,6 @@ where
     | .ok urlMap => return urlMap
     | .error e => throw s!"'LAKE_PKG_URL_MAP' has invalid JSON: {e}"
 
-/--
-The string Lake uses to identify Lean in traces.
-Either the environment-specified `LEAN_GITHASH` or the detected Lean's githash.
-
-The override allows one to replace the Lean version used by a library
-(e.g., Mathlib) without completely rebuilding it, which is useful for testing
-custom builds of Lean.
--/
-def leanGithash (env : Env) : String :=
-  if env.githashOverride.isEmpty then env.lean.githash else env.githashOverride
-
 /--
 The preferred toolchain of the environment. May be empty.
 Tries `env.initToolchain` first and then Lake's `Lean.toolchain`.
@@ -127,7 +113,6 @@ def baseVars (env : Env) : Array (String × Option String)  :=
     ("LAKE", env.lake.lake.toString),
     ("LAKE_HOME", env.lake.home.toString),
     ("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
-    ("LEAN_GITHASH", env.leanGithash),
     ("LEAN_SYSROOT", env.lean.sysroot.toString),
     ("LEAN_AR", env.lean.ar.toString),
     ("LEAN_CC", env.lean.leanCc?)

src/lake/Lake/Load/Elab.lean

@@ -156,7 +156,7 @@ Import the `.olean` for the configuration file if `reconfigure` is not set and
 an up-to-date one exists (i.e., one with matching configuration and on the same
 toolchain). Otherwise, elaborate the configuration and save it to the `.olean`.
 -/
-def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts : NameMap String)
+def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
 (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do
   let some configName := FilePath.mk <$> configFile.fileName
     | error "invalid configuration file name"
@@ -181,6 +181,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
   handle, and acquires an exclusive lock on the trace. It then releases its
   lock on the lock file. writes the new lock data.
   -/
+
   let acquireTrace h : IO IO.FS.Handle := id do
     let hLock ← IO.FS.Handle.mk lockFile .write
     /-
@@ -222,7 +223,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
     match (← IO.FS.removeFile olean |>.toBaseIO) with
     | .ok _ | .error (.noFileOrDirectory ..) =>
       h.putStrLn <| Json.pretty <| toJson
-        {platform := System.Platform.target, leanHash := lakeEnv.leanGithash,
+        {platform := System.Platform.target, leanHash := Lean.githash,
           configHash, options := lakeOpts : ConfigTrace}
       h.truncate
       let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
@@ -244,7 +245,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts
         | error "compiled configuration is invalid; run with '-R' to reconfigure"
       let upToDate :=
         (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
-        trace.leanHash = lakeEnv.leanGithash ∧ trace.configHash = configHash
+        trace.leanHash = Lean.githash ∧ trace.configHash = configHash
       if upToDate then
         let env ← importConfigFileCore olean leanOpts
         h.unlock

src/lake/Lake/Load/Main.lean

@@ -31,10 +31,10 @@ Elaborate a dependency's configuration file into a `Package`.
 The resulting package does not yet include any dependencies.
 -/
 def MaterializedDep.loadPackage (dep : MaterializedDep)
-(wsDir : FilePath) (lakeEnv : Lake.Env) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do
+(wsDir : FilePath) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
   let lakeDir := dir / defaultLakeDir
-  let configEnv ← importConfigFile dir lakeDir lakeEnv dep.configOpts leanOpts (dir / dep.configFile) reconfigure
+  let configEnv ← importConfigFile dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
     dir
@@ -51,7 +51,7 @@ Does not resolve dependencies.
 def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.env.leanSearchPath
   let configEnv ← importConfigFile
-    config.rootDir (config.rootDir / defaultLakeDir) config.env
+    config.rootDir (config.rootDir / defaultLakeDir)
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let root := {
@@ -145,7 +145,7 @@ def Workspace.updateAndMaterialize (ws : Workspace)
           return pkg
         else
           -- Load the package
-          let depPkg ← dep.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure
+          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts reconfigure
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
@@ -220,7 +220,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
       let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
         if let some entry := pkgEntries.find? dep.name then
           let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
-          result.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure
+          result.loadPackage ws.dir pkg.leanOpts reconfigure
         else if topLevel then
           error <|
             s!"dependency '{dep.name}' not in manifest; " ++

src/lake/tests/env/test.sh

@@ -13,7 +13,6 @@ $LAKE env | grep ".*=.*"
 # NOTE: `printenv` exits with code 1 if the variable is not set
 $LAKE env printenv LAKE
 $LAKE env printenv LAKE_HOME
-$LAKE env printenv LEAN_GITHASH
 $LAKE env printenv LEAN_SYSROOT
 $LAKE env printenv LEAN_AR | grep ar
 $LAKE env printenv LEAN_PATH
@@ -24,7 +23,6 @@ $LAKE -d ../../examples/hello env printenv PATH | grep examples/hello
 
 # Test that `env` preserves the input environment for certain variables
 test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
-test "`LEAN_GITHASH=foo $LAKE env printenv LEAN_GITHASH`" = foo
 test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo
 test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo
 

src/lean.mk.in

@@ -123,18 +123,9 @@ else
 	$(LEANC) -o "$@" $^ $(LEANC_OPTS) $(LINK_OPTS)
 endif
 
-ifeq (@CMAKE_SYSTEM_NAME@, Windows)
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(LIB_OUT)
 	@rm -f $@
-	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
-	@$(LEAN_AR) rcs $@ @$@.in
-	@rm -f $@.in
-else
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(LIB_OUT)
-	@rm -f $@
-# no response file support on macOS, but also no need for them
 	@$(LEAN_AR) rcs $@ $^
-endif
 
 clean:
 	rm -rf $(OUT)

src/runtime/compact.cpp

@@ -342,7 +342,7 @@ void object_compactor::operator()(object * o) {
             g_tag_counters[lean_ptr_tag(curr)]++;
 #endif
             switch (lean_ptr_tag(curr)) {
-            case LeanClosure:         lean_internal_panic("closures cannot be compacted. One possible cause of this error is trying to store a function in a persistent environment extension.");
+            case LeanClosure:         lean_internal_panic("closures cannot be compacted");
             case LeanArray:           r = insert_array(curr); break;
             case LeanScalarArray:     insert_sarray(curr); break;
             case LeanString:          insert_string(curr); break;

src/runtime/thread.cpp

@@ -46,26 +46,18 @@ void reset_thread_local() {
 
 using runnable = std::function<void()>;
 
-extern "C" LEAN_EXPORT void lean_initialize_thread() {
+static void thread_main(void * p) {
 #ifdef LEAN_SMALL_ALLOCATOR
     init_thread_heap();
 #endif
-}
-
-extern "C" LEAN_EXPORT void lean_finalize_thread() {
-    run_thread_finalizers();
-    run_post_thread_finalizers();
-}
-
-static void thread_main(void * p) {
-    lean_initialize_thread();
     std::unique_ptr<runnable> f;
     f.reset(reinterpret_cast<runnable *>(p));
 
     (*f)();
     f.reset();
 
-    lean_finalize_thread();
+    run_thread_finalizers();
+    run_post_thread_finalizers();
 }
 
 #if defined(LEAN_MULTI_THREAD)

src/runtime/thread.h

@@ -217,14 +217,9 @@ static T & GETTER_NAME() {                                              \
 }
 
 namespace lean {
-// module initializer pair (NOT for initializing individual threads!)
 void initialize_thread();
 void finalize_thread();
 
-// thread initializer pair, for reverse FFI
-extern "C" LEAN_EXPORT void lean_initialize_thread();
-extern "C" LEAN_EXPORT void lean_finalize_thread();
-
 typedef void (*thread_finalizer)(void *); // NOLINT
 LEAN_EXPORT void register_post_thread_finalizer(thread_finalizer fn, void * p);
 LEAN_EXPORT void register_thread_finalizer(thread_finalizer fn, void * p);

src/shell/CMakeLists.txt

@@ -119,18 +119,14 @@ ENDFOREACH(T)
 
 # LEAN BENCHMARK TESTS
 # do not test all .lean files in bench/
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
-else()
-  file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
-  FOREACH(T_OUT ${LEANBENCHTESTS})
-    string(REPLACE ".expected.out" "" T ${T_OUT})
-    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-    add_test(NAME "leanbenchtest_${T_NAME}"
-             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
-             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
-  ENDFOREACH(T_OUT)
-endif()
+file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
+FOREACH(T_OUT ${LEANBENCHTESTS})
+  string(REPLACE ".expected.out" "" T ${T_OUT})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanbenchtest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
+           COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
+ENDFOREACH(T_OUT)
 
 file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
 FOREACH(T ${LEANINTERPTESTS})
@@ -150,19 +146,15 @@ FOREACH(T ${LEANT0TESTS})
 ENDFOREACH(T)
 
 # LEAN PACKAGE TESTS
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
-else()
-  file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
-  FOREACH(T ${LEANPKGTESTS})
-    if(IS_DIRECTORY ${T})
-      GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-      add_test(NAME "leanpkgtest_${T_NAME}"
-              WORKING_DIRECTORY "${T}"
-              COMMAND bash -c "${TEST_VARS} ./test.sh")
-    endif()
-  ENDFOREACH(T)
-endif()
+file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
+FOREACH(T ${LEANPKGTESTS})
+  if(IS_DIRECTORY ${T})
+    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+    add_test(NAME "leanpkgtest_${T_NAME}"
+            WORKING_DIRECTORY "${T}"
+            COMMAND bash -c "${TEST_VARS} ./test.sh")
+  endif()
+ENDFOREACH(T)
 
 # LEAN SERVER TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean")