original behavour as Array.mapFinIdx

Prints `Lean.versionString` and target/platform information. Example:
```
Lean 4.12.0, commit 8218940152
Target: arm64-apple-darwin23.5.0 macOS
```

.github/workflows/check-prelude.yml

@@ -11,7 +11,9 @@ jobs:
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: src/Lean
+          sparse-checkout: |
+            src/Lean
+            src/Std
       - name: Check Prelude
         run: |
           failed_files=""
@@ -19,8 +21,8 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean -name '*.lean' -print0)
+          done < <(find src/Lean src/Std -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1
-          fi
+          fi

CODEOWNERS

@@ -4,14 +4,14 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @semorrison
-/RELEASES.md @semorrison
+/.github/ @Kha @kim-em
+/RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
 /src/Lean/Data/Lsp/ @mhuisi
-/src/Lean/Elab/Deriving/ @semorrison
-/src/Lean/Elab/Tactic/ @semorrison
+/src/Lean/Elab/Deriving/ @kim-em
+/src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
@@ -19,7 +19,7 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/Init/Data/ @semorrison
+/src/Init/Data/ @kim-em
 /src/Init/Data/Array/Lemmas.lean @digama0
 /src/Init/Data/List/Lemmas.lean @digama0
 /src/Init/Data/List/BasicAux.lean @digama0
@@ -45,3 +45,4 @@
 /src/Std/ @TwoFX
 /src/Std/Tactic/BVDecide/ @hargoniX
 /src/Lean/Elab/Tactic/BVDecide/ @hargoniX
+/src/Std/Sat/ @hargoniX

src/Init/Core.lean

@@ -1937,15 +1937,6 @@ instance : Subsingleton (Squash α) where
     apply Quot.sound
     trivial
 
-/-! # Relations -/
-
-/--
-`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
--/
-class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
-  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
-
 namespace Lean
 /-! # Kernel reduction hints -/
 
@@ -2121,4 +2112,14 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
+/--
+`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
+-/
+class Antisymm (r : α → α → Prop) : Prop where
+  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
+  antisymm {a b : α} : r a b → r b a → a = b
+
+@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
+abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
+
 end Std

src/Init/Data/Array.lean

@@ -16,3 +16,4 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
+import Init.Data.Array.MapIdx

src/Init/Data/Array/Basic.lean

@@ -25,6 +25,8 @@ variable {α : Type u}
 
 namespace Array
 
+@[deprecated size (since := "2024-10-13")] abbrev data := @toList
+
 /-! ### Preliminary theorems -/
 
 @[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
@@ -396,20 +398,25 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
+/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
+    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
     | i+1, inv =>
-      have : j < as.size := by
+      have j_lt : j < as.size := by
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
-      let idx : Fin as.size := ⟨j, this⟩
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f idx (as.get idx)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
   map as.size 0 rfl (mkEmpty as.size)
 
+@[inline]
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+  as.mapFinIdxM fun i a => f i a
+
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
   for a in as do
@@ -515,8 +522,13 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f
 
+/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+  Id.run <| as.mapFinIdxM f
+
+@[inline]
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
@@ -817,9 +829,15 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
 
 /-! ## Auxiliary functions used in metaprogramming.
 
-We do not intend to provide verification theorems for these functions.
+We do not currently intend to provide verification theorems for these functions.
 -/
 
+/- ### reduceOption -/
+
+/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
+@[inline] def reduceOption (as : Array (Option α)) : Array α :=
+  as.filterMap id
+
 /-! ### eraseReps -/
 
 /--

src/Init/Data/Array/Lemmas.lean

@@ -12,9 +12,7 @@ import Init.Data.Array.Mem
 import Init.TacticsExtra
 
 /-!
-## Bootstrapping theorems about arrays
-
-This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
+## Theorems about `Array`.
 -/
 
 namespace Array
@@ -811,57 +809,6 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   · simp
   · simp only [getElem_map, getElem_pop, size_map]
 
-/-! ### mapIdx -/
-
--- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapIdxM.map]
-    | zero =>
-      have := (Nat.zero_add _).symm.trans h
-      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
-    | succ i ih =>
-      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
-      · intro i i_lt h'
-        rw [get_push]
-        split
-        · apply h₂
-        · simp only [size_push] at h'
-          obtain rfl : i = j := by omega
-          apply (hs ⟨i, by omega⟩ hm).1
-      · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
-
-theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
-  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
-
-@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
-  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapIdx _ _
-
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
-    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
-
-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
-    (a.mapIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
-  split <;> simp_all
-
 /-! ### modify -/
 
 @[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by

src/Init/Data/Array/MapIdx.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.List.MapIdx
+
+namespace Array
+
+/-! ### mapFinIdx -/
+
+-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
+theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+    let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    induction i generalizing j bs with simp [mapFinIdxM.map]
+    | zero =>
+      have := (Nat.zero_add _).symm.trans h
+      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
+    | succ i ih =>
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      · intro i i_lt h'
+        rw [get_push]
+        split
+        · apply h₂
+        · simp only [size_push] at h'
+          obtain rfl : i = j := by omega
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
+  simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
+
+theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapFinIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
+  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
+  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapFinIdx _ _
+
+@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapFinIdx a f).size) :
+    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapFinIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
+  split <;> simp_all
+
+/-! ### mapIdx -/
+
+theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
+
+theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapIdx (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)
+
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.map (f i) := by
+  simp [getElem?_def, size_mapIdx, getElem_mapIdx]
+
+end Array

src/Init/Data/Hashable.lean

@@ -51,6 +51,9 @@ instance : Hashable USize where
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 
+instance : Hashable Char where
+  hash c := c.val.toUInt64
+
 instance : Hashable Int where
   hash
     | Int.ofNat n => UInt64.ofNat (2 * n)

src/Init/Data/List/Basic.lean

@@ -1418,11 +1418,15 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
 /-- Sum of a list of natural numbers. -/
--- We intend to subsequently deprecate this in favor of `List.sum`.
+@[deprecated List.sum (since := "2024-10-17")]
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
-@[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
-@[simp] theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
+set_option linter.deprecated false in
+@[simp, deprecated sum_nil (since := "2024-10-17")]
+theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
+set_option linter.deprecated false in
+@[simp, deprecated sum_cons (since := "2024-10-17")]
+theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
     Nat.sum (a::l) = a + Nat.sum l := rfl
 
 /-! ### range -/

src/Init/Data/List/BasicAux.lean

@@ -232,7 +232,8 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   match as, bs with
   | [],    []    => rfl
   | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
@@ -248,7 +249,8 @@ theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as
         have : a = b := s.antisymm hab hba
         simp [this, ih]
 
-instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
+instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
+    Std.Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
 end List

src/Init/Data/List/MinMax.lean

@@ -75,7 +75,7 @@ theorem le_min?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
@@ -146,7 +146,7 @@ theorem max?_le_iff [Max α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

src/Init/Data/List/Monadic.lean

@@ -99,4 +99,14 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
+/-! ### foldlM and foldrM -/
+
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
+    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+  induction l generalizing g init <;> simp [*]
+
+theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
+    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+  induction l generalizing g init <;> simp [*]
+
 end List

src/Init/Data/Nat/Basic.lean

@@ -490,10 +490,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
             (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
 protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
-instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
+instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Antisymm (¬ . < . : Nat → Nat → Prop) where
+instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=

src/Init/Data/OfScientific.lean

@@ -10,8 +10,10 @@ import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
    Examples:
-   - `OfScientific.ofScientific 123 true 2`    represents `1.23`
-   - `OfScientific.ofScientific 121 false 100` represents `121e100`
+   - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
+   - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
+
+   Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
 -/
 class OfScientific (α : Type u) where
   ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

src/Init/Data/Option/Attach.lean

@@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
   simp
 
 theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
-    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
+    o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
   subst w
   simp
 
@@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
   cases o <;> simp
 
 theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
-    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
 theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
-    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
 theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}

src/Init/Data/String/Basic.lean

@@ -1148,23 +1148,23 @@ namespace String
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
 -/
-def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
-  s.toSubstring.dropPrefix? pre
+def dropPrefix? (s : String) (pre : String) : Option Substring :=
+  s.toSubstring.dropPrefix? pre.toSubstring
 
 /--
 If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
 -/
-def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
-  s.toSubstring.dropSuffix? suff
+def dropSuffix? (s : String) (suff : String) : Option Substring :=
+  s.toSubstring.dropSuffix? suff.toSubstring
 
 /-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : Substring) : String :=
+def stripPrefix (s : String) (pre : String) : String :=
   s.dropPrefix? pre |>.map Substring.toString |>.getD s
 
 /-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : Substring) : String :=
+def stripSuffix (s : String) (suff : String) : String :=
   s.dropSuffix? suff |>.map Substring.toString |>.getD s
 
 end String

src/Init/Data/Sum.lean

@@ -4,21 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 prelude
-import Init.Core
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-def getLeft? : α ⊕ β → Option α
-  | inl a => some a
-  | inr _ => none
-
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-def getRight? : α ⊕ β → Option β
-  | inr b => some b
-  | inl _ => none
-
-end Sum
+import Init.Data.Sum.Basic
+import Init.Data.Sum.Lemmas

src/Init/Data/Sum/Basic.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Yury G. Kudryashov
+-/
+prelude
+import Init.PropLemmas
+
+/-!
+# Disjoint union of types
+
+This file defines basic operations on the the sum type `α ⊕ β`.
+
+`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
+
+## Main declarations
+
+* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
+* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
+* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
+* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
+* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
+  if it's coming from the right.
+* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
+  if it's coming from the left.
+* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
+* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
+* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
+* `Sum.LiftRel`: The disjoint union of two relations.
+* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
+
+## Further material
+
+See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
+
+## Notes
+
+The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
+To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
+universe signature in consequence. The `Prop` version is `Or`.
+-/
+
+namespace Sum
+
+deriving instance DecidableEq for Sum
+deriving instance BEq for Sum
+
+section get
+
+/-- Check if a sum is `inl`. -/
+def isLeft : α ⊕ β → Bool
+  | inl _ => true
+  | inr _ => false
+
+/-- Check if a sum is `inr`. -/
+def isRight : α ⊕ β → Bool
+  | inl _ => false
+  | inr _ => true
+
+/-- Retrieve the contents from a sum known to be `inl`.-/
+def getLeft : (ab : α ⊕ β) → ab.isLeft → α
+  | inl a, _ => a
+
+/-- Retrieve the contents from a sum known to be `inr`.-/
+def getRight : (ab : α ⊕ β) → ab.isRight → β
+  | inr b, _ => b
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+def getLeft? : α ⊕ β → Option α
+  | inl a => some a
+  | inr _ => none
+
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+def getRight? : α ⊕ β → Option β
+  | inr b => some b
+  | inl _ => none
+
+@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
+@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
+@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
+@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
+
+@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
+@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
+
+@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
+@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
+@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
+@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
+
+end get
+
+/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
+protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
+  fun x => Sum.casesOn x f g
+
+@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
+    Sum.elim f g (inl x) = f x := rfl
+
+@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
+    Sum.elim f g (inr x) = g x := rfl
+
+/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
+protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
+  Sum.elim (inl ∘ f) (inr ∘ g)
+
+@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
+
+@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
+
+/-- Swap the factors of a sum type -/
+def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
+
+@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
+
+@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
+
+section LiftRel
+
+/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
+`α ⊕ β` and `γ ⊕ δ`. -/
+inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
+  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
+  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
+  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
+  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
+
+@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
+  ⟨fun h => by cases h; assumption, LiftRel.inl⟩
+
+@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
+
+@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
+
+@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
+  ⟨fun h => by cases h; assumption, LiftRel.inr⟩
+
+instance {r : α → γ → Prop} {s : β → δ → Prop}
+    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
+    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
+  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
+  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
+  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
+  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
+
+end LiftRel
+
+section Lex
+
+/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
+respective order on `α` or `β`. -/
+inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
+  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
+  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
+  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
+  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
+  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
+  | sep (a b) : Lex r s (inl a) (inr b)
+
+attribute [simp] Lex.sep
+
+@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
+  ⟨fun h => by cases h; assumption, Lex.inl⟩
+
+@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
+  ⟨fun h => by cases h; assumption, Lex.inr⟩
+
+@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
+
+instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
+  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
+  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
+  | inr _, inl _ => Decidable.isFalse lex_inr_inl
+  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr
+
+end Lex
+
+end Sum

src/Init/Data/Sum/Lemmas.lean

@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Yury G. Kudryashov
+-/
+prelude
+import Init.Data.Sum.Basic
+import Init.Ext
+
+/-!
+# Disjoint union of types
+
+Theorems about the definitions introduced in `Init.Data.Sum.Basic`.
+-/
+
+open Function
+
+namespace Sum
+
+@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
+    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
+  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
+
+@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
+    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
+  ⟨ fun
+    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
+    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
+    fun
+    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
+    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
+
+theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
+    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
+  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
+  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
+    apply funext
+    rintro (_ | _) <;> rfl
+  rw [h1]; exact h _ _
+
+section get
+
+@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
+  | inl _, _ => rfl
+@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
+  | inr _, _ => rfl
+
+@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
+  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
+
+@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
+  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
+
+theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
+  | inl _, _ => rfl
+
+@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
+  cases x <;> simp at h ⊢
+
+theorem eq_right_getRight_of_isRight : ∀ {x : α ⊕ β} (h : x.isRight), x = inr (x.getRight h)
+  | inr _, _ => rfl
+
+@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
+  cases x <;> simp at h ⊢
+
+@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
+  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
+
+@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
+  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
+
+@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
+
+@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
+
+theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight := by simp
+
+@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
+
+@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
+
+theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft := by simp
+
+theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
+
+theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
+
+end get
+
+theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
+
+theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
+
+theorem inl_ne_inr : inl a ≠ inr b := nofun
+
+theorem inr_ne_inl : inr b ≠ inl a := nofun
+
+/-! ### `Sum.elim` -/
+
+@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f :=
+  rfl
+
+@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g :=
+  rfl
+
+@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
+  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
+
+theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
+    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
+  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
+
+@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
+    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
+  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
+
+theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
+    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
+  simp [funext_iff]
+
+/-! ### `Sum.map` -/
+
+@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
+    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
+  | inl _ => rfl
+  | inr _ => rfl
+
+@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
+    Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
+  funext <| map_map f' g' f g
+
+@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
+  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
+
+theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
+    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
+  cases x <;> rfl
+
+theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
+    Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
+  funext fun _ => elim_map
+
+@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
+    isLeft (x.map f g) = isLeft x := by
+  cases x <;> rfl
+
+@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
+    isRight (x.map f g) = isRight x := by
+  cases x <;> rfl
+
+@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
+    (x.map f g).getLeft? = x.getLeft?.map f := by
+  cases x <;> rfl
+
+@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
+    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
+
+/-! ### `Sum.swap` -/
+
+@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
+
+@[simp] theorem swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
+
+@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
+
+@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
+
+@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
+
+@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
+
+section LiftRel
+
+theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
+  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
+  cases h
+  · exact LiftRel.inl (hr _ _ ‹_›)
+  · exact LiftRel.inr (hs _ _ ‹_›)
+
+theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
+    LiftRel r₂ s x y :=
+  (h.mono hr) fun _ _ => id
+
+theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
+    LiftRel r s₂ x y :=
+  h.mono (fun _ _ => id) hs
+
+protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
+  cases h
+  · exact LiftRel.inr ‹_›
+  · exact LiftRel.inl ‹_›
+
+@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
+  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
+
+end LiftRel
+
+section Lex
+
+protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
+  cases h
+  · exact Lex.inl ‹_›
+  · exact Lex.inr ‹_›
+
+theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
+
+theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
+    Lex r₂ s₂ x y := by
+  cases h
+  · exact Lex.inl (hr _ _ ‹_›)
+  · exact Lex.inr (hs _ _ ‹_›)
+  · exact Lex.sep _ _
+
+theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
+  (h.mono hr) fun _ _ => id
+
+theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
+  h.mono (fun _ _ => id) hs
+
+theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
+  induction aca with
+  | intro _ _ IH =>
+    constructor
+    intro y h
+    cases h with
+    | inl h' => exact IH _ h'
+
+theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
+    Acc (Lex r s) (inr b) := by
+  induction acb with
+  | intro _ _ IH =>
+    constructor
+    intro y h
+    cases h with
+    | inr h' => exact IH _ h'
+    | sep => exact aca _
+
+theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
+  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
+  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
+
+end Lex
+
+theorem elim_const_const (c : γ) :
+    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
+  apply funext
+  rintro (_ | _) <;> rfl
+
+@[simp] theorem elim_lam_const_lam_const (c : γ) :
+    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
+  Sum.elim_const_const c

src/Init/MetaTypes.lean

@@ -224,11 +224,7 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
-  with an `rfl`-theorem.
-  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
-  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
-  will **not** create a proof term which is an application of the annotated theorem.
+  This option does not have any effect (yet).
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

src/Init/NotationExtra.lean

@@ -168,9 +168,9 @@ end Lean
   | _                => throw ()
 
 @[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) _)   => `(sorry)
-  | `($(_) _ _) => `(sorry)
-  | _           => throw ()
+  | `($(_) $_)    => `(sorry)
+  | `($(_) $_ $_) => `(sorry)
+  | _             => throw ()
 
 @[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)

src/Init/PropLemmas.lean

@@ -135,6 +135,10 @@ Both reduce to `b = false ∧ c = false` via `not_or`.
 
 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
 
+/-! ## not equal -/
+
+theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
+  mt <| congrArg _
 
 /-! ## Ite -/
 
@@ -384,6 +388,17 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 
 end quantifiers
 
+/-! ## membership -/
+
+section Mem
+variable [Membership α β] {s t : β} {a b : α}
+
+theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ h
+
+theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ h
+
+end Mem
+
 /-! ## Nonempty -/
 
 @[simp] theorem nonempty_prop {p : Prop} : Nonempty p ↔ p :=

src/Init/Tactics.lean

@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
   -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
+  withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic

src/Lean.lean

@@ -29,7 +29,6 @@ import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
-import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
 import Lean.Log

src/Lean/Elab/BuiltinCommand.lean

@@ -12,16 +12,18 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
+import Init.System.Platform
 
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
-   match stx[1] with
-   | Syntax.atom _ val =>
-     let doc := val.extract 0 (val.endPos - ⟨2⟩)
-     let range ← Elab.getDeclarationRange stx
-     modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+  match stx[1] with
+  | Syntax.atom _ val =>
+    let doc := val.extract 0 (val.endPos - ⟨2⟩)
+    let some range ← Elab.getDeclarationRange? stx
+      | return  -- must be from partial syntax, ignore
+    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
 private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
@@ -403,6 +405,16 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
   | _ => throwUnsupportedSyntax
 
+@[builtin_command_elab version] def elabVersion : CommandElab := fun _ => do
+  let mut target := System.Platform.target
+  if target.isEmpty then target := "unknown"
+  -- Only one should be set, but good to know if multiple are set in error.
+  let platforms :=
+    (if System.Platform.isWindows then [" Windows"] else [])
+    ++ (if System.Platform.isOSX then [" macOS"] else [])
+    ++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
+  logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
+
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
   -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
   -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
   -- such as "failed to infer definition type" can surface.
-  let defView := mkDefViewOfDef { isUnsafe := true }
+  let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
   Term.elabMutualDef #[] { header := "" } #[defView]

src/Lean/Elab/BuiltinNotation.lean

@@ -135,13 +135,21 @@ open Meta
   | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
-  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
-  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
-  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
-  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
-  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
-  | _                                                                 => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)   => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)   => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type $b:byTactic'; $body) =>
+    -- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
+    -- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk $x : $type := $body; $b:byTactic)
+  | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk _%$x : $type := $body; $b:byTactic)
+  | `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
+  | _ => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/DeclModifiers.lean

@@ -57,6 +57,7 @@ inductive RecKind where
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
+  stx             : TSyntax ``Parser.Command.declModifiers
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false
@@ -121,16 +122,16 @@ section Methods
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
-def elabModifiers (stx : Syntax) : m Modifiers := do
-  let docCommentStx := stx[0]
-  let attrsStx      := stx[1]
-  let visibilityStx := stx[2]
-  let noncompStx    := stx[3]
-  let unsafeStx     := stx[4]
+def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
+  let docCommentStx := stx.raw[0]
+  let attrsStx      := stx.raw[1]
+  let visibilityStx := stx.raw[2]
+  let noncompStx    := stx.raw[3]
+  let unsafeStx     := stx.raw[4]
   let recKind       :=
-    if stx[5].isNone then
+    if stx.raw[5].isNone then
       RecKind.default
-    else if stx[5][0].getKind == ``Parser.Command.partial then
+    else if stx.raw[5][0].getKind == ``Parser.Command.partial then
       RecKind.partial
     else
       RecKind.nonrec
@@ -148,7 +149,7 @@ def elabModifiers (stx : Syntax) : m Modifiers := do
     | none       => pure #[]
     | some attrs => elabDeclAttrs attrs
   return {
-    docString?, visibility, recKind, attrs,
+    stx, docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
     isNoncomputable := !noncompStx.isNone
   }

src/Lean/Elab/Declaration.lean

@@ -104,7 +104,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let (binders, typeStx) := expandDeclSig stx[2]
   let scopeLevelNames ← getLevelNames
   let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName stx
+  addDeclarationRanges declName modifiers.stx stx
   runTermElabM fun vars =>
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
@@ -144,10 +144,10 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName decl
+  addDeclarationRanges declName modifiers.stx decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ctor[2]
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
@@ -214,17 +214,18 @@ def elabDeclaration : CommandElab := fun stx => do
     -- only case implementing incrementality currently
     elabMutualDef #[stx]
   else withoutCommandIncrementality true do
+    let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩
     if declKind == ``Lean.Parser.Command.«axiom» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabAxiom modifiers decl
     else if declKind == ``Lean.Parser.Command.«inductive» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabClassInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«structure» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabStructure modifiers decl
     else
       throwError "unexpected declaration"
@@ -238,7 +239,7 @@ private def isMutualInductive (stx : Syntax) : Bool :=
 
 private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
   let views ← elems.mapM fun stx => do
-     let modifiers ← elabModifiers stx[0]
+     let modifiers ← elabModifiers ⟨stx[0]⟩
      inductiveSyntaxToView modifiers stx[1]
   elabInductiveViews views
 
@@ -399,7 +400,7 @@ def elabMutual : CommandElab := fun stx => do
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
-      addDeclarationRanges fullId defStx
+      addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
       elabCommand (← `(
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))

src/Lean/Elab/DeclarationRange.lean

@@ -11,12 +11,14 @@ import Lean.Data.Lsp.Utf16
 
 namespace Lean.Elab
 
-def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
+def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do
+  let some range := stx.getRange?
+    | return none
   let fileMap ← getFileMap
-  let pos    := stx.getPos?.getD 0
-  let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition
-  let pos    := pos |> fileMap.toPosition
-  return {
+  --let range := fileMap.utf8RangeToLspRange
+  let pos    := fileMap.toPosition range.start
+  let endPos := fileMap.toPosition range.stop
+  return some {
     pos          := pos
     charUtf16    := fileMap.leanPosToLspPos pos |>.character
     endPos       := endPos
@@ -49,23 +51,27 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
 
 
 /--
-  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
-  This method is for the builtin declarations only.
-  User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
-def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
-  if stx.getKind == ``Parser.Command.«example» then
+Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
+`cmdStx` the remaining part of the syntax tree for `declName`.
+
+This method is for the builtin declarations only. User-defined commands should use
+`Lean.addDeclarationRanges` to store this information for their commands.
+-/
+def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
+    (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
+  if declStx.getKind == ``Parser.Command.«example» then
     return ()
-  else
-    Lean.addDeclarationRanges declName {
-      range          := (← getDeclarationRange stx)
-      selectionRange := (← getDeclarationRange (getDeclarationSelectionRef stx))
-    }
+  let stx := mkNullNode #[modsStx, declStx]
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
 
 /-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
 def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
-  Lean.addDeclarationRanges declName {
-    range          := (← getDeclarationRange stx)
-    selectionRange := (← getDeclarationRange header)
-  }
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? header | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
 
 end Lean.Elab

src/Lean/Elab/Frontend.lean

@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data.stx
+    let commands := commands.push snap.data
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -111,13 +111,15 @@ where
       let messages := toSnapshotTree initialSnap
         |>.getAll.map (·.diagnostics.msgLog)
         |>.foldl (· ++ ·) {}
-      let trees := toSnapshotTree initialSnap
-        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
+      -- In contrast to messages, we should collect info trees only from the top-level command
+      -- snapshots as they subsume any info trees reported incrementally by their children.
+      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
       return {
         commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.data.parserState
         cmdPos := snap.data.parserState.pos
-        inputCtx, initialSnap, commands
+        commands := commands.map (·.stx)
+        inputCtx, initialSnap
       }
 
 def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)

src/Lean/Elab/LetRec.lean

@@ -90,6 +90,7 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
+        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
          let value ← elabTermEnsuringType view.valStx type
          mkLambdaFVars xs value
 

src/Lean/Elab/MutualDef.lean

@@ -410,11 +410,15 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-          -- synthesize mvars here to force the top-level tactic block (if any) to run
-          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-        -- leads to more section variables being included than necessary
-        let val ← instantiateMVarsProfiling val
+          -- Store instantiated body in info tree for the benefit of the unused variables linter
+          -- and other metaprograms that may want to inspect it without paying for the instantiation
+          -- again
+          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
+            -- synthesize mvars here to force the top-level tactic block (if any) to run
+            let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+            -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+            -- leads to more section variables being included than necessary
+            instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do
@@ -883,6 +887,7 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
   else DefKind.«def»
 
 def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
+  stx             := ⟨mkNullNode #[]⟩  -- ignore when computing declaration range
   isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable
   recKind         := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
   isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
@@ -993,7 +998,7 @@ where
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
         -- that depends only on a part of the ref
-        addDeclarationRanges header.declName view.ref
+        addDeclarationRanges header.declName view.modifiers.stx view.ref
 
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -1017,7 +1022,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
-      let modifiers ← elabModifiers d[0]
+      let modifiers ← elabModifiers ⟨d[0]⟩
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]

src/Lean/Elab/PreDefinition/Basic.lean

@@ -221,7 +221,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
               else
                 none
             | _ => none
-          modifiers := {} }
+          modifiers := default }
 
 private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool :=
   (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome

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

@@ -212,21 +212,21 @@ def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
 /--
 Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context,
-The `type` is the expected type of the argument.
+The `FType` is the expected type of the argument.
 The `recArgInfos` is used to transform the body of the function to replace recursive calls with
 uses of the `below` induction hypothesis.
 -/
 def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
     (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
   lambdaTelescope value fun xs value => do
-    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
-    let FType ← instantiateForall FType indexMajorArgs
+    let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indicesMajorArgs
     forallBoundedTelescope FType (some 1) fun below _ => do
       -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
       -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
       let below := below[0]!
-      let valueNew   ← replaceRecApps recArgInfos positions below value
-      mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let valueNew ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
 
 /--
 Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
@@ -264,7 +264,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     (brecOnConst : Nat → Expr) : MetaM (Array Expr) := do
   let numTypeFormers := positions.size
   let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
-  let brecOn := brecOnConst 0
+  let brecOn := brecOnConst recArgInfo.indIdx
   check brecOn
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument

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

@@ -77,7 +77,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       if !indIndices.all Expr.isFVar then
         throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
       else if !indIndices.allDiff then
-        throwError " its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+        throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
         let indexMinPos := getIndexMinPos xs indIndices
         let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed

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

@@ -107,9 +107,9 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
     check valueNew
     return #[{ preDef with value := valueNew }]
 
-  -- Sort the (indices of the) definitions by their position in indInfo.all
+  -- Groups the (indices of the) definitions by their position in indInfo.all
   let positions : Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
-  trace[Elab.definition.structural] "positions: {positions}"
+  trace[Elab.definition.structural] "assignments of type formers of {indInfo.name} to functions: {positions}"
 
   -- Construct the common `.brecOn` arguments
   let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
@@ -117,7 +117,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   let brecOnConst ← mkBRecOnConst recArgInfos positions motives
   let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
   trace[Elab.definition.structural] "FTypes: {FTypes}"
-  let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
+  let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
     mkBRecOnF recArgInfos positions r v t
   trace[Elab.definition.structural] "FArgs: {FArgs}"
   -- Assemble the individual `.brecOn` applications

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

@@ -15,7 +15,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) :
   return { preDef with
     declName  := mkSmartUnfoldingNameFor preDef.declName
     value     := (← visit preDef.value)
-    modifiers := {}
+    modifiers := default
   }
 where
   /--

src/Lean/Elab/Structure.lean

@@ -95,7 +95,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
     addAuxDeclarationRanges declName ref ref
-    pure { ref, modifiers := {}, name := defaultCtorName, declName }
+    pure { ref, modifiers := default, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
   else
@@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
       let scopeLevelNames ← Term.getLevelNames
       let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
       Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
-        addDeclarationRanges declName stx
+        addDeclarationRanges declName modifiers.stx stx
         Term.withDeclName declName do
           let ctor ← expandCtor stx modifiers declName
           let fields ← expandFields stx modifiers declName

src/Lean/Elab/Syntax.lean

@@ -146,7 +146,7 @@ where
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else
-      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) do process arg
+      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i == 0 }) do process arg
       mkParserSeq args
 
   ensureNoPrec (stx : Syntax) :=

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -520,7 +520,7 @@ where
 
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
-  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     -- disable incrementality if body is run multiple times
     Term.withoutTacticIncrementality (tag.size > 1) do
       for tag in tag, hs in hs do
@@ -528,20 +528,20 @@ def evalCase : Tactic
         let g ← renameInaccessibles g hs
         setGoals [g]
         g.setTag Name.anonymous
-        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
+        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <|
           Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
         setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic «case'»] def evalCase' : Tactic
-  | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case'%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
     let mut acc := #[]
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       let mvarTag ← g.getTag
       setGoals [g]
-      withCaseRef arr tac (evalTactic tac)
+      withCaseRef arr tac <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <| evalTactic tac
       let gs' ← getUnsolvedGoals
       if let [g'] := gs' then
         g'.setTag mvarTag

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

@@ -119,7 +119,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         let ids ← ids.mapIdxM fun i id =>
           match id.getNat with
           | 0 => throwErrorAt id "positive integer expected"
-          | n+1 => pure (n, i.1)
+          | n+1 => pure (n, i)
         let ids := ids.qsort (·.1 < ·.1)
         unless @Array.allDiff _ ⟨(·.1 == ·.1)⟩ ids do
           throwError "occurrence list is not distinct"

src/Lean/Elab/Tactic/Ext.lean

@@ -123,9 +123,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
           levelParams := info.levelParams
         }
         modifyEnv fun env => addProtected env extName
-        Lean.addDeclarationRanges extName {
-          range := ← getDeclarationRange (← getRef)
-          selectionRange := ← getDeclarationRange (← getRef) }
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
@@ -163,9 +161,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         -- Only declarations in a namespace can be protected:
         unless extIffName.isAtomic do
           modifyEnv fun env => addProtected env extIffName
-        Lean.addDeclarationRanges extIffName {
-          range := ← getDeclarationRange (← getRef)
-          selectionRange := ← getDeclarationRange (← getRef) }
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\

src/Lean/Elab/Tactic/Induction.lean

@@ -27,8 +27,10 @@ open Meta
   syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
   ```
 -/
+private def getAltLhses (alt : Syntax) : Syntax :=
+  alt[0]
 private def getFirstAltLhs (alt : Syntax) : Syntax :=
-  alt[0][0]
+  (getAltLhses alt)[0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
 private def getAltName (alt : Syntax) : Name :=
   let lhs := getFirstAltLhs alt
@@ -70,7 +72,9 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
       let goals ← getGoals
       try
         setGoals [mvarId]
-        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
+        closeUsingOrAdmit <|
+          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
+            (addInfo *> evalTactic rhs)
       finally
         setGoals goals
 

src/Lean/Elab/Term.lean

@@ -914,7 +914,9 @@ private def applyAttributesCore
   Remark: if the declaration has syntax errors, `declName` may be `.anonymous` see issue #4309
   In this case, we skip attribute application.
   -/
-  unless declName == .anonymous do
+  if declName == .anonymous then
+    return
+  withDeclName declName do
     for attr in attrs do
       withRef attr.stx do withLogging do
       let env ← getEnv

src/Lean/Language/Basic.lean

@@ -243,11 +243,16 @@ instance : ToSnapshotTree SnapshotLeaf where
 structure DynamicSnapshot where
   /-- Concrete snapshot value as `Dynamic`. -/
   val  : Dynamic
-  /-- Snapshot tree retrieved from `val` before erasure. -/
-  tree : SnapshotTree
+  /--
+  Snapshot tree retrieved from `val` before erasure. We do thunk even the first level as accessing
+  it too early can create some unnecessary tasks from `toSnapshotTree` that are otherwise avoided by
+  `(sync := true)` when accessing only after elaboration has finished. Early access can even lead to
+  deadlocks when later forcing these unnecessary tasks on a starved thread pool.
+  -/
+  tree : Thunk SnapshotTree
 
 instance : ToSnapshotTree DynamicSnapshot where
-  toSnapshotTree s := s.tree
+  toSnapshotTree s := s.tree.get
 
 /-- Creates a `DynamicSnapshot` from a typed snapshot value. -/
 def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where

src/Lean/LazyInitExtension.lean

@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.MonadEnv
-
-namespace Lean
-
-structure LazyInitExtension (m : Type → Type) (α : Type) where
-  ext : EnvExtension (Option α)
-  fn  : m α
-
-instance [Monad m] [Inhabited α] : Inhabited (LazyInitExtension m α) where
-  default := {
-    ext := default
-    fn  := pure default
-  }
-
-/--
-  Register an environment extension for storing the result of `fn`.
-  We initialize the extension with `none`, and `fn` is executed the
-  first time `LazyInit.get` is executed.
-
-  This kind of extension is useful for avoiding work duplication in
-  scenarios where a thunk cannot be used because the computation depends
-  on state from the `m` monad. For example, we may want to "cache" a collection
-  of theorems as a `SimpLemmas` object.  -/
-def registerLazyInitExtension (fn : m α) : IO (LazyInitExtension m α) := do
-  let ext ← registerEnvExtension (pure none)
-  return { ext, fn }
-
-def LazyInitExtension.get [MonadEnv m] [Monad m] (init : LazyInitExtension m α) : m α := do
-  match init.ext.getState (← getEnv) with
-  | some a => return a
-  | none   =>
-    let a ← init.fn
-    modifyEnv fun env => init.ext.setState env (some a)
-    return a
-
-end Lean

src/Lean/Linter/ConstructorAsVariable.lean

@@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
     let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
-      tree.visitM' (preNode := fun ci info _ => do
+      tree.visitM' (postNode := fun ci info _ => do
         match info with
         | .ofTermInfo ti =>
           match ti.expr with

src/Lean/Linter/UnusedVariables.lean

@@ -10,41 +10,55 @@ set_option linter.missingDocs true -- keep it documented
 
 /-! # Unused variable Linter
 
-This file implements the unused variable linter, which runs automatically on all commands
-and reports any local variables that are never referred to, using information from the info tree.
+This file implements the unused variable linter, which runs automatically on all
+commands and reports any local variables that are never referred to, using
+information from the info tree.
 
-It is not immediately obvious but this is a surprisingly expensive check without some optimizations.
-The main complication is that it can be difficult to determine what constitutes a "use".
-For example, we would like this to be considered a use of `x`:
+It is not immediately obvious but this is a surprisingly expensive check without
+some optimizations.  The main complication is that it can be difficult to
+determine what constitutes a "use" apart from direct references to a variable
+that we can easily find in the info tree.  For example, we would like this to be
+considered a use of `x`: 
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
 
-The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
-the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
-further into the tactic state we can see the `fvar` show up in the instantiation to the original
-goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
-instantiations to determine what happened after the fact, because tactics might skip the goal
-metavariable and instantiate some other metavariable created prior to it instead.
+The final proof term is `fun x => x` so clearly `x` was used, but we can't make
+use of this because the final proof term is after we have abstracted over the
+original `fvar` for `x`. Instead, we make sure to store the proof term before
+abstraction but after instantiation of mvars in the info tree and retrieve it in
+the linter. Using the instantiated term is very important as redoing that step
+in the linter can be prohibitively expensive. The downside of special-casing the
+definition body in this way is that while it works for parameters, it does not
+work for local variables in the body, so we ignore them by default if any tactic
+infos are present (`linter.unusedVariables.analyzeTactics`).
 
-Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
-metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
-linear in the size of the info tree, even though there are many metavariable contexts in all the
-intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
-so there is a lot of subterm sharing we can take advantage of.
+If we do turn on this option and look further into the tactic state, we can see
+the `fvar` show up in the instantiation to the original goal metavariable
+`?m : Nat := x`, but it is not always the case that we can follow metavariable
+instantiations to determine what happened after the fact, because tactics might
+skip the goal metavariable and instantiate some other metavariable created prior
+to it instead.  Instead, we use a (much more expensive) overapproximation, which
+is just to look through the entire metavariable context looking for occurrences
+of `x`. We use caching to ensure that this is still linear in the size of the
+info tree, even though there are many metavariable contexts in all the
+intermediate stages of elaboration; these are highly similar and make use of
+`PersistentHashMap` so there is a lot of subterm sharing we can take advantage
+of.
 
 ## The `@[unused_variables_ignore_fn]` attribute
 
-Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
-variables in these positions. For example:
+Some occurrences of variables are deliberately unused, or at least we don't want
+to lint on unused variables in these positions. For example:
 
 ```
 def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
                   -- ^ don't lint this unused variable because it is public API
 ```
 
-They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
-external syntax can also opt in to lint suppression, like so:
+They are generally a syntactic criterion, so we allow adding custom
+`IgnoreFunction`s so that external syntax can also opt in to lint suppression,
+like so:
 
 ```
 macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
@@ -77,6 +91,17 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
+/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
+register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
+  defValue := false
+  descr := "enable analysis of local variables in presence of tactic proofs\
+          \n\
+          \nBy default, the linter will limit itself to linting a declaration's parameters \
+            whenever tactic proofs are present as these can be expensive to analyze. Enabling this \
+            option extends linting to local variables both inside and outside tactic proofs, \
+            though it can also lead to some false negatives as intermediate tactic states may \
+            reference some variables without the declaration ultimately depending on them."
+}
 
 /-- Gets the status of `linter.unusedVariables` -/
 def getLinterUnusedVariables (o : Options) : Bool :=
@@ -356,55 +381,82 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
-    StateRefT References IO Unit := do
-  for tree in infoTrees do
-    tree.visitM' (preNode := fun ci info _ => do
-      match info with
-      | .ofTermInfo ti =>
-        match ti.expr with
-        | .const .. =>
-          if ti.isBinder then
-            let some range := info.range? | return
-            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-            modify fun s => { s with constDecls := s.constDecls.insert range }
-        | .fvar id .. =>
-          let some range := info.range? | return
-          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-          if ti.isBinder then
-            -- This is a local variable declaration.
-            let some ldecl := ti.lctx.find? id | return
-            -- Skip declarations which are outside the command syntax range, like `variable`s
-            -- (it would be confusing to lint these), or those which are macro-generated
-            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
-            let opts := ci.options
-            -- we have to check for the option again here because it can be set locally
-            if !getLinterUnusedVariables opts then return
-            let stx := skipDeclIdIfPresent info.stx
-            if let .str _ s := stx.getId then
-              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-              -- This is the suggested way to silence the warning
-              if s.startsWith "_" then return
-            -- Record this either as a new `fvarDefs`, or an alias of an existing one
-            modify fun s =>
-              if let some ref := s.fvarDefs[range]? then
-                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
-              else
-                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
-          else
-            -- Found a direct use, keep track of it
-            modify fun s => { s with fvarUses := s.fvarUses.insert id }
-        | _ => pure ()
-      | .ofTacticInfo ti =>
-        -- Keep track of the `MetavarContext` after a tactic for later
-        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
-      | .ofFVarAliasInfo i =>
-        -- record any aliases we find
-        modify fun s =>
-          let id := followAliases s.fvarAliases i.baseId
-          { s with fvarAliases := s.fvarAliases.insert i.id id }
-      | _ => pure ())
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
 where
+  go infoTrees ctx? := do
+    for tree in infoTrees do
+      tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
+        -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
+        let ignored ← read
+        match info with
+        | .ofTermInfo ti =>
+          -- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
+          -- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
+          -- parameters
+          if ti.elaborator == `MutualDef.body &&
+              !linter.unusedVariables.analyzeTactics.get ci.options then
+            -- the body is the only `Expr` we will analyze in this case
+            -- NOTE: we include it even if no tactics are present as at least for parameters we want
+            -- to lint only truly unused binders
+            let (e, _) := instantiateMVarsCore ci.mctx ti.expr
+            modify fun s => { s with
+              assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+            let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+            withReader (· || tacticsPresent) do
+              go children.toArray ci
+            return false
+          if ignored then return true
+          match ti.expr with
+          | .const .. =>
+            if ti.isBinder then
+              let some range := info.range? | return true
+              let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+              modify fun s => { s with constDecls := s.constDecls.insert range }
+          | .fvar id .. =>
+            let some range := info.range? | return true
+            let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+            if ti.isBinder then
+              -- This is a local variable declaration.
+              if ignored then return true
+              let some ldecl := ti.lctx.find? id | return true
+              -- Skip declarations which are outside the command syntax range, like `variable`s
+              -- (it would be confusing to lint these), or those which are macro-generated
+              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
+              let opts := ci.options
+              -- we have to check for the option again here because it can be set locally
+              if !getLinterUnusedVariables opts then return true
+              let stx := skipDeclIdIfPresent info.stx
+              if let .str _ s := stx.getId then
+                -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+                -- This is the suggested way to silence the warning
+                if s.startsWith "_" then return true
+              -- Record this either as a new `fvarDefs`, or an alias of an existing one
+              modify fun s =>
+                if let some ref := s.fvarDefs[range]? then
+                  { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+                else
+                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+            else
+              -- Found a direct use, keep track of it
+              modify fun s => { s with fvarUses := s.fvarUses.insert id }
+          | _ => pure ()
+          return true
+        | .ofTacticInfo ti =>
+          -- When ignoring new binders, no need to look at intermediate tactic states either as
+          -- references to binders outside the body will be covered by the body `Expr`
+          if ignored then return true
+          -- Keep track of the `MetavarContext` after a tactic for later
+          modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+          return true
+        | .ofFVarAliasInfo i =>
+          if ignored then return true
+          -- record any aliases we find
+          modify fun s =>
+            let id := followAliases s.fvarAliases i.baseId
+            { s with fvarAliases := s.fvarAliases.insert i.id id }
+          return true
+        | _ => return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
@@ -493,7 +545,7 @@ def unusedVariables : Linter where
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
         -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
+        fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now

src/Lean/Meta/IndPredBelow.lean

@@ -54,7 +54,7 @@ def mkContext (declName : Name) : MetaM Context := do
   let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
   let motiveTypes ← typeInfos.mapM motiveType
   let motives ← motiveTypes.mapIdxM fun j motive =>
-    return (← motiveName motiveTypes j.val, motive)
+    return (← motiveName motiveTypes j, motive)
   let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
   return {
     motives := motives
@@ -214,7 +214,7 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
 
 def mkInductiveType
     (ctx : Context)
-    (i : Fin ctx.typeInfos.size)
+    (i : Nat)
     (indVal : InductiveVal) : MetaM InductiveType := do
   return {
     name := ctx.belowNames[i]!
@@ -340,11 +340,11 @@ where
   mkIH
       (params : Array Expr)
       (motives : Array Expr)
-      (idx : Fin ctx.motives.size)
+      (idx : Nat)
       (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
     let name :=
       if ctx.motives.size > 1
-      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx + 1}"
       else mkFreshUserName <| .mkSimple "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
@@ -353,7 +353,7 @@ where
         let args := params ++ motives ++ ys
         let premise :=
           mkAppN
-            (mkConst ctx.belowNames[idx.val]! levels) args
+            (mkConst ctx.belowNames[idx]! levels) args
         let conclusion :=
           mkAppN motives[idx]! ys
         mkForallFVars ys (←mkArrow premise conclusion)

src/Lean/Meta/InferType.lean

@@ -441,6 +441,8 @@ This can be used to infer the expected type of the alternatives when constructin
 -/
 def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
   forallBoundedTelescope type n fun xs _ => do
+    unless xs.size = n do
+      throwError "type {type} does not have {n} parameters"
     let types ← xs.mapM (inferType ·)
     for t in types do
       if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -70,7 +70,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId
       let hEqSz  := (subst.get hEq).fvarId!
-      if h : i.val < sizes.size then
+      if h : i < sizes.size then
          let n := sizes.get ⟨i, h⟩
          let mvarId ← mvarId.clear subgoal.newHs[0]!
          let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!

src/Lean/Meta/Match/Match.lean

@@ -545,7 +545,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
   let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
-    if h : i.val < values.size then
+    if h : i < values.size then
       let value := values.get ⟨i, h⟩
       -- (x = value) branch
       let subst := subgoal.subst
@@ -599,7 +599,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
   let sizes := collectArraySizes p
   let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
   subgoals.mapIdxM fun i subgoal => do
-    if i.val < sizes.size then
+    if i < sizes.size then
       let size     := sizes.get! i
       let subst    := subgoal.subst
       let elems    := subgoal.elems.toList

src/Lean/Meta/Tactic/FunInd.lean

@@ -643,7 +643,7 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
       pure mvar
   trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
   let decls := mvars.mapIdx fun i mvar =>
-    (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType))
+    (.mkSimple s!"case{i+1}", (fun _ => mvar.getType))
   Meta.withLocalDeclsD decls fun xs => do
       for mvar in mvars, x in xs do
         mvar.assign x
@@ -971,7 +971,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
             mkForallFVars ys (.sort levelZero)
         let motiveArities ← infos.mapM fun info => do
           lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
-        let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do
+        let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do
           let n := if infos.size = 1 then .mkSimple "motive"
                                      else .mkSimple s!"motive_{i+1}"
           pure (n, fun _ => pure motiveType)

src/Lean/Meta/Tactic/SplitIf.lean

@@ -4,31 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.LazyInitExtension
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 namespace SplitIf
 
-builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
-  registerLazyInitExtension do
-    let mut s : SimpTheorems := {}
-    s ← s.addConst ``if_pos
-    s ← s.addConst ``if_neg
-    s ← s.addConst ``dif_pos
-    s ← s.addConst ``dif_neg
-    return {
-      simpTheorems  := #[s]
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := { Simp.neutralConfig with dsimp := false }
-    }
-
 /--
   Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
   just the rewriting rules for reducing `if` expressions. -/
-def getSimpContext : MetaM Simp.Context :=
-  ext.get
+def getSimpContext : MetaM Simp.Context := do
+  let mut s : SimpTheorems := {}
+  s ← s.addConst ``if_pos
+  s ← s.addConst ``if_neg
+  s ← s.addConst ``dif_pos
+  s ← s.addConst ``dif_neg
+  return {
+    simpTheorems  := #[s]
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := { Simp.neutralConfig with dsimp := false }
+  }
 
 /--
   Default `discharge?` function for `simpIf` methods.

src/Lean/Parser/Command.lean

@@ -505,6 +505,9 @@ Displays all available tactic tags, with documentation.
 -/
 @[builtin_command_parser] def printTacTags   := leading_parser
   "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
+/-- Shows the current Lean version. Prints `Lean.versionString`. -/
+@[builtin_command_parser] def version        := leading_parser
+  "#version"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit

src/Lean/Parser/Extra.lean

@@ -189,7 +189,7 @@ open PrettyPrinter Syntax.MonadTraverser Formatter in
 @[combinator_formatter sepByIndent]
 def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : Formatter := do
   let stx ← getCur
-  let hasNewlineSep := stx.getArgs.mapIdx (fun ⟨i, _⟩ n =>
+  let hasNewlineSep := stx.getArgs.mapIdx (fun i n =>
     i % 2 == 1 && n.matchesNull 0 && i != stx.getArgs.size - 1) |>.any id
   visitArgs do
     for i in (List.range stx.getArgs.size).reverse do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1215,32 +1215,11 @@ def delabDo : Delab := whenPPOption getPPNotation do
   let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))
   `(do $items:doSeqItem*)
 
-def reifyName : Expr → DelabM Name
-  | .const ``Lean.Name.anonymous _ => return Name.anonymous
-  | mkApp2 (.const ``Lean.Name.str _) n (.lit (.strVal s)) => return (← reifyName n).mkStr s
-  | mkApp2 (.const ``Lean.Name.num _) n (.lit (.natVal i)) => return (← reifyName n).mkNum i
-  | mkApp (.const ``Lean.Name.mkStr1 _) (.lit (.strVal a)) => return Lean.Name.mkStr1 a
-  | mkApp2 (.const ``Lean.Name.mkStr2 _) (.lit (.strVal a1)) (.lit (.strVal a2)) =>
-    return Lean.Name.mkStr2 a1 a2
-  | mkApp3 (.const ``Lean.Name.mkStr3 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) =>
-    return Lean.Name.mkStr3 a1 a2 a3
-  | mkApp4 (.const ``Lean.Name.mkStr4 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) =>
-    return Lean.Name.mkStr4 a1 a2 a3 a4
-  | mkApp5 (.const ``Lean.Name.mkStr5 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) =>
-    return Lean.Name.mkStr5 a1 a2 a3 a4 a5
-  | mkApp6 (.const ``Lean.Name.mkStr6 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) =>
-    return Lean.Name.mkStr6 a1 a2 a3 a4 a5 a6
-  | mkApp7 (.const ``Lean.Name.mkStr7 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) =>
-    return Lean.Name.mkStr7 a1 a2 a3 a4 a5 a6 a7
-  | mkApp8 (.const ``Lean.Name.mkStr8 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) (.lit (.strVal a8)) =>
-    return Lean.Name.mkStr8 a1 a2 a3 a4 a5 a6 a7 a8
-  | _ => failure
-
 @[builtin_delab app.Lean.Name.str,
   builtin_delab app.Lean.Name.mkStr1, builtin_delab app.Lean.Name.mkStr2, builtin_delab app.Lean.Name.mkStr3, builtin_delab app.Lean.Name.mkStr4,
   builtin_delab app.Lean.Name.mkStr5, builtin_delab app.Lean.Name.mkStr6, builtin_delab app.Lean.Name.mkStr7, builtin_delab app.Lean.Name.mkStr8]
 def delabNameMkStr : Delab := whenPPOption getPPNotation do
-  let n ← reifyName (← getExpr)
+  let some n := (← getExpr).name? | failure
   -- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
   return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
 

src/Lean/Server/Completion.lean

@@ -1004,7 +1004,7 @@ private def assignSortTexts (completions : CompletionList) : CompletionList := I
   if completions.items.isEmpty then
     return completions
   let items := completions.items.mapIdx fun i item =>
-    { item with sortText? := toString i.val }
+    { item with sortText? := toString i }
   let maxDigits := items[items.size - 1]!.sortText?.get!.length
   let items := items.map fun item =>
     let sortText := item.sortText?.get!

src/Lean/Server/InfoUtils.lean

@@ -40,27 +40,34 @@ structure InfoWithCtx where
   info : Elab.Info
   children : PersistentArray InfoTree
 
-/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
-and accumulating results on the way back up. -/
+/--
+Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
+accumulating results on the way back up. If `preNode` returns `false`, the children of the current
+node are skipped and `postNode` is invoked with an empty list of results.
+-/
 partial def InfoTree.visitM [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
-    : InfoTree → m (Option α) :=
-  go none
+    (ctx? : Option ContextInfo := none) : InfoTree → m (Option α) :=
+  go ctx?
 where go
   | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
   | some ctx, node i cs => do
-    preNode ctx i cs
-    let as ← cs.toList.mapM (go <| i.updateContext? ctx)
-    postNode ctx i cs as
+    let visitChildren ← preNode ctx i cs
+    if !visitChildren then
+      postNode ctx i cs []
+    else
+      let as ← cs.toList.mapM (go <| i.updateContext? ctx)
+      postNode ctx i cs as
   | none, node .. => panic! "unexpected context-free info tree node"
   | _, hole .. => pure none
 
 /-- `InfoTree.visitM` specialized to `Unit` return type -/
 def InfoTree.visitM' [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
-    (t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard
+    (ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
+  t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
 
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
@@ -410,6 +417,9 @@ where go ci?
     match ci?, i with
     | some ci, .ofTermInfo ti
     | some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
+      -- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
+      -- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
+      -- of making the `instantiateMVars` here a no-op and avoids further recursing into the body
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
       return expr.hasSorry
       -- we assume that `cs` are subterms of `ti.expr` and

src/Lean/Util/Recognizers.lean

@@ -106,4 +106,29 @@ def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
 def prod? (e : Expr) : Option (Expr × Expr) :=
   e.app2? ``Prod
 
+/--
+Checks if an expression is a `Name` literal, and if so returns the name.
+-/
+def name? : Expr → Option Name
+  | .const ``Lean.Name.anonymous _ => Name.anonymous
+  | mkApp2 (.const ``Lean.Name.str _) n (.lit (.strVal s)) => (name? n).map (·.str s)
+  | mkApp2 (.const ``Lean.Name.num _) n i =>
+    (i.rawNatLit? <|> i.nat?).bind fun i => (name? n).map (Name.num · i)
+  | mkApp (.const ``Lean.Name.mkStr1 _) (.lit (.strVal a)) => Lean.Name.mkStr1 a
+  | mkApp2 (.const ``Lean.Name.mkStr2 _) (.lit (.strVal a1)) (.lit (.strVal a2)) =>
+    Lean.Name.mkStr2 a1 a2
+  | mkApp3 (.const ``Lean.Name.mkStr3 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) =>
+    Lean.Name.mkStr3 a1 a2 a3
+  | mkApp4 (.const ``Lean.Name.mkStr4 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) =>
+    Lean.Name.mkStr4 a1 a2 a3 a4
+  | mkApp5 (.const ``Lean.Name.mkStr5 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) =>
+    Lean.Name.mkStr5 a1 a2 a3 a4 a5
+  | mkApp6 (.const ``Lean.Name.mkStr6 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) =>
+    Lean.Name.mkStr6 a1 a2 a3 a4 a5 a6
+  | mkApp7 (.const ``Lean.Name.mkStr7 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) =>
+    Lean.Name.mkStr7 a1 a2 a3 a4 a5 a6 a7
+  | mkApp8 (.const ``Lean.Name.mkStr8 _) (.lit (.strVal a1)) (.lit (.strVal a2)) (.lit (.strVal a3)) (.lit (.strVal a4)) (.lit (.strVal a5)) (.lit (.strVal a6)) (.lit (.strVal a7)) (.lit (.strVal a8)) =>
+    Lean.Name.mkStr8 a1 a2 a3 a4 a5 a6 a7 a8
+  | _ => none
+
 end Lean.Expr

src/Std/Sat/AIG.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.Lemmas

src/Std/Sat/AIG/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Data.HashMap
 import Std.Data.HashSet
 

src/Std/Sat/AIG/CNF.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.CNF
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas

src/Std/Sat/AIG/Cached.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 

src/Std/Sat/AIG/CachedGates.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Cached
 import Std.Sat.AIG.CachedLemmas
 

src/Std/Sat/AIG/CachedGatesLemmas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.CachedGates
 import Std.Sat.AIG.LawfulOperator
 

src/Std/Sat/AIG/CachedLemmas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Cached
 
 /-!

src/Std/Sat/AIG/If.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.CachedGatesLemmas
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/LawfulOperator.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 
 /-!

src/Std/Sat/AIG/LawfulVecOperator.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.RefVec
 

src/Std/Sat/AIG/Lemmas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 

src/Std/Sat/AIG/RefVec.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.CachedGatesLemmas
 

src/Std/Sat/AIG/RefVecOperator.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVecOperator.Map
 import Std.Sat.AIG.RefVecOperator.Zip
 import Std.Sat.AIG.RefVecOperator.Fold

src/Std/Sat/AIG/RefVecOperator/Fold.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/RefVecOperator/Map.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/RefVecOperator/Zip.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 

src/Std/Sat/AIG/Relabel.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 

src/Std/Sat/AIG/RelabelNat.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Relabel
 
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+import Init.Data.AC
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not

src/lake/Lake/CLI/Init.lean

@@ -126,7 +126,8 @@ package {repr pkgName} where
   version := v!\"0.1.0\"
   keywords := #[\"math\"]
   leanOptions := #[
-    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`autoImplicit, false⟩
   ]
 
 require \"leanprover-community\" / \"mathlib\"
@@ -144,6 +145,7 @@ defaultTargets = [{repr libRoot}]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+autoImplicit = false
 
 [[require]]
 name = \"mathlib\"

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -31,49 +31,52 @@ a : α
       • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
       • match α, β, x, a with
         | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
-        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-          • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-        • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.636 -> _uniq.312
-        • FVarAlias α: _uniq.635 -> _uniq.310
-        • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-          • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.667 -> _uniq.312
-        • FVarAlias n: _uniq.666 -> _uniq.310
-        • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-          • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
+        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ MutualDef.body
+        • match α, β, x, a with
+          | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
+          | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+            • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+          • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • FVarAlias a: _uniq.636 -> _uniq.312
+          • FVarAlias α: _uniq.635 -> _uniq.310
+          • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+          • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
+          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+            • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+          • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+          • FVarAlias a: _uniq.667 -> _uniq.312
+          • FVarAlias n: _uniq.666 -> _uniq.310
+          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
+            • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
       • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
 [Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 194, column := 42 }, charUtf16 := 42, endPos := { line := 200, column := 31 },
+      { pos := { line := 202, column := 42 }, charUtf16 := 42, endPos := { line := 208, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 },
+      { pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },
         endCharUtf16 := 58 } }

tests/lean/1074b.lean.expected.out

@@ -2,4 +2,4 @@
 1074b.lean:11:43-11:53: error: tactic 'assumption' failed
 a n z✝ : Term
 a✝ : Brx z✝
-⊢ Brx (sorryAx Term true)
+⊢ Brx sorry

tests/lean/1301.lean.expected.out

@@ -6,4 +6,4 @@ a' : True ∧ True
 1301.lean:9:25-9:29: error: elaboration function for 'termTerm' has not been implemented
   term
 def b : Nat → Nat :=
-sorryAx (Nat → Nat) true
+sorry

tests/lean/255.lean.expected.out

@@ -1,6 +1,6 @@
 A : α
 id x✝ : α
 255.lean:16:7-16:8: error: unknown constant 'x✝'
-id (sorryAx ?m true) : ?m
+id sorry : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (sorryAx ?m true) : ?m
+id sorry : ?m

tests/lean/StxQuot.lean.expected.out

@@ -45,7 +45,7 @@ StxQuot.lean:83:7-83:19: error: unknown identifier 'sufficesDecl'
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
 StxQuot.lean:97:39-97:44: error: unexpected antiquotation splice
-fun x => sorryAx (?m x) true : (x : ?m) → ?m x
+fun x => sorry : (x : ?m) → ?m x
 "#[(some 1), (some 2)]"
 StxQuot.lean:104:13-104:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -10,11 +10,11 @@ has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+Prop → sorry : Sort (imax 1 u_1)
 binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
   p
 has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+Prop → sorry : Sort (imax 1 u_1)

tests/lean/defInst.lean.expected.out

@@ -2,7 +2,7 @@
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
-fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
+fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
 [("hello", "hello")]

tests/lean/docStr.lean.expected.out

@@ -19,7 +19,7 @@ doc string for 'g' is not available
 "Auxiliary declaration used to implement named patterns like `x@h:p`. "
 "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n"
 Foo :=
-  { range := { pos := { line := 4, column := 0 },
+  { range := { pos := { line := 3, column := 0 },
                charUtf16 := 0,
                endPos := { line := 6, column := 58 },
                endCharUtf16 := 58 },
@@ -46,7 +46,7 @@ Foo.val :=
                         endPos := { line := 6, column := 47 },
                         endCharUtf16 := 47 } }
 myAxiom :=
-  { range := { pos := { line := 9, column := 0 },
+  { range := { pos := { line := 8, column := 0 },
                charUtf16 := 0,
                endPos := { line := 9, column := 19 },
                endCharUtf16 := 19 },
@@ -91,7 +91,7 @@ Boo.y :=
                         endPos := { line := 15, column := 5 },
                         endCharUtf16 := 5 } }
 Tree :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -100,7 +100,7 @@ Tree :=
                         endPos := { line := 18, column := 14 },
                         endCharUtf16 := 14 } }
 Tree.rec :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -109,7 +109,7 @@ Tree.rec :=
                         endPos := { line := 18, column := 14 },
                         endCharUtf16 := 14 } }
 Tree.casesOn :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -136,7 +136,7 @@ Tree.leaf :=
                         endPos := { line := 20, column := 43 },
                         endCharUtf16 := 43 } }
 Bla.test :=
-  { range := { pos := { line := 25, column := 0 },
+  { range := { pos := { line := 24, column := 0 },
                charUtf16 := 0,
                endPos := { line := 31, column := 16 },
                endCharUtf16 := 16 },

tests/lean/interactive/2881.lean

@@ -0,0 +1,49 @@
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry
+    -- General goal
+--^ $/lean/plainGoal
+
+example : True := by
+  suffices True by
+      -- Goal assuming `True`
+  --^ $/lean/plainGoal
+    sorry

tests/lean/interactive/2881.lean.expected.out

@@ -0,0 +1,31 @@
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 2, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 8, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 13, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 19, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 24, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 30, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 35, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 41, "character": 2}}
+{"rendered": "```lean\nn : Nat\n⊢ True\n```", "goals": ["n : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 46, "character": 4}}
+{"rendered": "```lean\nthis : True\n⊢ True\n```",
+ "goals": ["this : True\n⊢ True"]}

tests/lean/interactive/goTo.lean.expected.out

@@ -92,8 +92,7 @@
   {"start": {"line": 38, "character": 26},
    "end": {"line": 38, "character": 38}},
   "targetRange":
-  {"start": {"line": 38, "character": 22},
-   "end": {"line": 40, "character": 78}},
+  {"start": {"line": 38, "character": 0}, "end": {"line": 40, "character": 78}},
   "originSelectionRange":
   {"start": {"line": 43, "character": 7},
    "end": {"line": 43, "character": 11}}}]

tests/lean/linterUnusedVariables.lean

@@ -129,6 +129,7 @@ def nolintPatternVars (x : Option (Option Nat)) : Nat :=
   | some (some y) => (fun z => 1) 2
   | _ => 0
 
+set_option linter.unusedVariables.analyzeTactics true in
 set_option linter.unusedVariables.patternVars false in
 theorem nolintPatternVarsInduction (n : Nat) : True := by
   induction n with
@@ -188,9 +189,12 @@ opaque foo (x : Nat) : Nat
 opaque foo' (x : Nat) : Nat :=
   let y := 5
   3
+
+section
 variable (bar)
 variable (bar' : (x : Nat) → Nat)
 variable {α β} [inst : ToString α]
+end
 
 @[specialize]
 def specializeDef (x : Nat) : Nat := 3
@@ -210,6 +214,8 @@ opaque externConst (x : Nat) : Nat :=
   let y := 3
   5
 
+section
+variable {α : Type}
 
 macro "useArg " name:declId arg:ident : command => `(def $name ($arg : α) : α := $arg)
 useArg usedMacroVariable a
@@ -222,6 +228,7 @@ doNotUseArg unusedMacroVariable b
 def ignoreDoNotUse : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``doNotUse]
 
 doNotUseArg unusedMacroVariable2 b
+end
 
 macro "ignoreArg " id:declId sig:declSig : command => `(opaque $id $sig)
 ignoreArg ignoredMacroVariable (x : UInt32) : UInt32
@@ -246,6 +253,7 @@ def Nat.discriminate (n : Nat) (H1 : n = 0 → α) (H2 : ∀ m, n = succ m →
   | 0 => H1 rfl
   | succ m => H2 m rfl
 
+/-! These are *not* linted against anymore as they are parameters used in the eventual body term. -/
 example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
@@ -267,3 +275,16 @@ inaccessible annotation.
 -/
 example : (x = y) → y = x
   | .refl _ => .refl _
+
+/-! We do lint parameters by default (`analyzeTactics false`) even when they have lexical uses -/
+
+theorem lexicalTacticUse (p : α → Prop) (ha : p a) (hb : p b) : p b := by
+  simp [ha, hb]
+
+/-!
+... however, `analyzeTactics true` consistently takes lexical uses for all variables into account
+-/
+
+set_option linter.unusedVariables.analyzeTactics true in
+theorem lexicalTacticUse' (p : α → Prop) (ha : p a) (hb : p b) : p b := by
+  simp [ha, hb]

tests/lean/linterUnusedVariables.lean.expected.out

@@ -30,51 +30,37 @@ linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h`
+linterUnusedVariables.lean:138:9-138:10: warning: unused variable `h`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y`
+linterUnusedVariables.lean:152:8-152:9: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β`
+linterUnusedVariables.lean:155:20-155:21: warning: unused variable `β`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x`
+linterUnusedVariables.lean:156:7-156:8: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s`
+linterUnusedVariables.lean:166:6-166:7: warning: unused variable `s`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y`
+linterUnusedVariables.lean:190:6-190:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x`
+linterUnusedVariables.lean:200:19-200:20: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
+linterUnusedVariables.lean:204:6-204:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
+linterUnusedVariables.lean:209:6-209:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
+linterUnusedVariables.lean:214:6-214:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b`
+linterUnusedVariables.lean:225:32-225:33: warning: unused variable `b`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:236:27-236:28: error: don't know how to synthesize placeholder
+linterUnusedVariables.lean:243:27-243:28: error: don't know how to synthesize placeholder
 context:
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:237:0-237:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:238:0-238:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:239:29-241:7: error: unexpected token 'theorem'; expected '{' or tactic
-linterUnusedVariables.lean:239:27-239:29: error: unsolved goals
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
+linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:246:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
+linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h`
+linterUnusedVariables.lean:281:41-281:43: warning: unused variable `ha`
 note: this linter can be disabled with `set_option linter.unusedVariables false`

tests/lean/macroSwizzle.lean.expected.out

@@ -9,4 +9,4 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-(sorryAx Nat true).succ : Nat
+sorry.succ : Nat

tests/lean/nameArgErrorIssue.lean.expected.out

@@ -7,7 +7,7 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-bla (sorryAx Nat true) 5 : Nat
+bla sorry 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: application type mismatch
   bla "hi"
 argument

tests/lean/namedHoles.lean.expected.out

@@ -6,13 +6,13 @@ has type
   Nat : Type
 but is expected to have type
   Bool : Type
-f ?x (sorryAx Bool true) : Nat
+f ?x sorry : Nat
 g ?x ?x : Nat
 20
 foo (fun x => ?hole) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun x => ?hole) fun y => sorryAx Nat true : Nat
+boo (fun x => ?hole) fun y => sorry : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context

tests/lean/noTabs.lean.expected.out

@@ -1,3 +1,3 @@
 noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
 let a := 1;
-sorryAx ?m true : ?m
+sorry : ?m

tests/lean/run/1163.lean

@@ -1,7 +1,7 @@
 import Lean
 open Lean Elab Tactic
 
-macro "obviously1" : tactic => `(tactic| exact sorryAx _)
+macro "obviously1" : tactic => `(tactic| exact sorryAx _ false)
 
 theorem result1 : False := by obviously1