chore: upstream Array.reduceOption

feat: add Hashable instance for Char (#5747 )
I needed this in downstream code, and it seems to make the most sense to just contribute it here.
2026-03-18 02:44:12 +00:00 · 2024-10-18 11:21:17 +11:00 · 2024-10-17 14:46:10 +00:00 · 2024-10-17 12:23:34 +00:00 · 2024-10-17 12:09:54 +00:00 · 2024-10-17 09:55:11 +00:00
41 changed files with 1136 additions and 506 deletions
--- a/src/Init/Core.lean
+++ b/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
--- a/src/Init/Data/Array.lean
+++ b/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
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -817,9 +817,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 -/

 /--
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/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
@@ -45,16 +43,6 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
  rw [getElem?_eq]
  split <;> simp_all

-@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
-abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
-theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
-
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
    (a.push x)[i] = a[i] := by
@@ -77,7 +65,10 @@ namespace List

 open Array

-/-! ### Lemmas about `List.toArray`. -/
+/-! ### Lemmas about `List.toArray`.
+
+We prefer to pull `List.toArray` outwards.
+-/

@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
    (a.toArrayAux b).size = b.size + a.length := by
@@ -85,20 +76,11 @@ open Array

@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl

-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
    a.toArray[i] = a[i]'(by simpa using h) := rfl

@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl

-@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
-theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
  apply ext'
  simp
@@ -163,20 +145,12 @@ end List

 namespace Array

-attribute [simp] uset
-
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl

@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl

-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl

-@[deprecated length_toList (since := "2024-09-09")]
-abbrev data_length := @length_toList
-
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl

@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@@ -225,9 +199,6 @@ where
    induction l generalizing arr <;> simp [*]
  simp [H]

-@[deprecated toList_map (since := "2024-09-09")]
-abbrev map_data := @toList_map
-
@[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
  simp only [← length_toList]
  simp
@@ -248,21 +219,10 @@ theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
    (l.foldl F acc).toList = acc.toList ++ l.flatMap G := by
  induction l generalizing acc <;> simp [*, List.flatMap]

-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
-
 theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
    (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
  induction l generalizing acc <;> simp [*]

-@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
-abbrev foldl_data_eq_map := @foldl_toList_eq_map
-
-theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
-
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
  simp only [anyM, Nat.min_def]; split <;> rfl
@@ -277,6 +237,12 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
@[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
  simp [mem_def]

+/-! # uset -/
+
+attribute [simp] uset
+
+theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
+
 /-! # get -/

@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
@@ -396,6 +362,10 @@ termination_by n - i
    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun

+theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
+    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
+  simp [getElem?_def]
+
 /-- # mkArray -/

@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
@@ -403,19 +373,17 @@ termination_by n - i

@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl

-@[deprecated toList_mkArray (since := "2024-09-09")]
-abbrev mkArray_data := @toList_mkArray
-
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
    (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]

+theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+    (mkArray n v)[i]? = if i < n then some v else none := by
+  simp [getElem?_def]
+
 /-- # mem -/

 theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm

-@[deprecated mem_toList (since := "2024-09-09")]
-abbrev mem_data := @mem_toList
-
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun

 theorem getElem_of_mem {a : α} {as : Array α} :
@@ -425,6 +393,12 @@ theorem getElem_of_mem {a : α} {as : Array α} :
  exists i
  exists hbound

+theorem getElem?_of_mem {a : α} {as : Array α} :
+    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
+  intro ha
+  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
+  exists i
+
@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
    (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
  split <;> simp_all [mem_def]
@@ -447,14 +421,11 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
    idx < a.size :=
  hidx

-theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
+theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
  erw [Array.mem_def, getElem_eq_getElem_toList]
  apply List.get_mem

-theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
-
-@[deprecated getElem_fin_eq_toList_get (since := "2024-09-09")]
-abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
+theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl

@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
  a[i] = a[i.toNat] := rfl
@@ -465,26 +436,8 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none :
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
  simp only [getElem_eq_getElem_toList, List.getElem_mem]

-@[deprecated getElem_mem_toList (since := "2024-09-09")]
-abbrev getElem_mem_data := @getElem_mem_toList
-
-theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
-
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
-theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
-abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
-
-set_option linter.deprecated false in
-theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
-  getElem?_eq_toList_get? ..
-
-@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
-abbrev get?_eq_data_get? := @get?_eq_toList_get?
+theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i := by
+  simp [getElem?_eq_getElem?_toList]

 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
  simp [get!_eq_getD]
@@ -497,7 +450,7 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
  simp [back, back?]

@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_getElem?]
+  simp [back?, getElem?_eq_getElem?_toList]

 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp

@@ -528,9 +481,6 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el

@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl

-@[deprecated toList_set (since := "2024-09-09")]
-abbrev data_set := @toList_set
-
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
    (a.set i v)[i.1] = v := by
  simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
@@ -571,12 +521,9 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
@[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
    (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]

-@[deprecated toList_swap (since := "2024-09-09")]
-abbrev data_swap := @toList_swap
-
-theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
    if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
-  simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
+  simp [swap_def, get?_set, ← getElem_fin_eq_getElem_toList]

@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
    a.swapAt i v = (a[i.1], a.set i v) := rfl
@@ -594,9 +541,6 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :

@[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]

-@[deprecated toList_pop (since := "2024-09-09")]
-abbrev data_pop := @toList_pop
-
@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl

@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@@ -629,9 +573,6 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :

 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl

-@[deprecated size_eq_length_toList (since := "2024-09-09")]
-abbrev size_eq_length_data := @size_eq_length_toList
-
@[simp] theorem size_swap! (a : Array α) (i j) :
    (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]

@@ -656,14 +597,10 @@ abbrev size_eq_length_data := @size_eq_length_toList
@[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
  induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]

-@[deprecated toList_range (since := "2024-09-09")]
-abbrev data_range := @toList_range
-
@[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
  simp [getElem_eq_getElem_toList]

-set_option linter.deprecated false in
@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
  let rec go (as : Array α) (i j hj)
      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
@@ -676,9 +613,9 @@ set_option linter.deprecated false in
      · rwa [Nat.add_right_comm i]
      · simp [size_swap, h₂]
      · intro k
-        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        rw [← getElem?_eq_getElem?_toList, getElem?_swap]
        simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          getElem?_eq_toList_getElem?]
+          getElem?_eq_getElem?_toList]
        split <;> rename_i h₂
        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@@ -705,9 +642,6 @@ set_option linter.deprecated false in
        true_and, Nat.not_lt] at h
      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]

-@[deprecated toList_reverse (since := "2024-09-30")]
-abbrev reverse_toList := @toList_reverse
-
 /-! ### foldl / foldr -/

@[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -736,7 +670,7 @@ abbrev reverse_toList := @toList_reverse
    foldrM f init #[] start stop = return init := by
  simp [foldrM]

-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldlM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
@@ -752,7 +686,7 @@ theorem foldl_induction
    · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
  simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0

-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldrM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldr_induction
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
@@ -798,9 +732,6 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
    toList <$> arr.mapM f = arr.toList.mapM f := by
  simp [mapM_eq_mapM_toList]

-@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
-abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
-
 theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
  unfold mapM.map
@@ -872,56 +803,11 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
  · simp only [getElem_map, get_push, size_map]
    split <;> rfl

-/-! ### 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
+@[simp] theorem map_pop {f : α → β} {as : Array α} :
+    as.pop.map f = (as.map f).pop := by
+  ext
+  · simp
+  · simp only [getElem_map, getElem_pop, size_map]

 /-! ### modify -/

@@ -945,12 +831,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
    (as.modify i f)[j] = as[j]'(by simpa using hj) := by
  simp [getElem_modify hj, h]

-@[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
-  simp [getElem_modify h]
-
 /-! ### filter -/

@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -964,9 +844,6 @@ theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
  induction l with simp
  | cons => split <;> simp [*]

-@[deprecated toList_filter (since := "2024-09-09")]
-abbrev filter_data := @toList_filter
-
@[simp] theorem filter_filter (q) (l : Array α) :
    filter p (filter q l) = filter (fun a => p a && q a) l := by
  apply ext'
@@ -1000,9 +877,6 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
  · simp_all [Id.run, List.filterMap_cons]
    split <;> simp_all

-@[deprecated toList_filterMap (since := "2024-09-09")]
-abbrev filterMap_data := @toList_filterMap
-
@[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
  simp only [mem_def, toList_filterMap, List.mem_filterMap]
@@ -1020,9 +894,6 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl

 theorem toList_empty : (#[] : Array α).toList = [] := rfl

-@[deprecated toList_empty (since := "2024-09-09")]
-abbrev empty_data := @toList_empty
-
 /-! ### append -/

 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@@ -1045,9 +916,6 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
  apply List.get_of_eq; rw [toList_append]

-@[deprecated getElem_append_left (since := "2024-09-30")]
-abbrev get_append_left := @getElem_append_left
-
 theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
    (as ++ bs)[i] = bs[i - as.size] := by
@@ -1056,9 +924,6 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
  apply List.get_of_eq; rw [toList_append]

-@[deprecated getElem_append_right (since := "2024-09-30")]
-abbrev get_append_right := @getElem_append_right
-
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
  apply ext'; simp only [toList_append, toList_empty, List.append_nil]

@@ -1301,9 +1166,6 @@ theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any
  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
  exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩

-@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
-abbrev any_def := @any_toList
-
 /-! ### all -/

 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
@@ -1343,9 +1205,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
    rw [← getElem_eq_getElem_toList]
    exact w ⟨r, h⟩

-@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
-abbrev all_def := @all_toList
-
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
  simp only [← all_toList, List.all_eq_true, mem_def]

@@ -1415,33 +1274,8 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
    · split <;> simp_all
    · split <;> simp_all

-@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
-abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
-@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
-abbrev get_extract_loop_lt := @getElem_extract_loop_lt
-@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
-abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
-@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
-abbrev get_extract_loop_ge := @getElem_extract_loop_ge
-@[deprecated getElem_extract_aux (since := "2024-09-30")]
-abbrev get_extract_aux := @getElem_extract_aux
-@[deprecated getElem_extract (since := "2024-09-30")]
-abbrev get_extract := @getElem_extract
-
-@[deprecated getElem_swap_right (since := "2024-09-30")]
-abbrev get_swap_right := @getElem_swap_right
-@[deprecated getElem_swap_left (since := "2024-09-30")]
-abbrev get_swap_left := @getElem_swap_left
-@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
-abbrev get_swap_of_ne := @getElem_swap_of_ne
-@[deprecated getElem_swap (since := "2024-09-30")]
-abbrev get_swap := @getElem_swap
-@[deprecated getElem_swap' (since := "2024-09-30")]
-abbrev get_swap' := @getElem_swap'
-
 end Array

-
 open Array

 namespace List
@@ -1586,3 +1420,158 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
  simp

 end List
+
+/-! ### Deprecations -/
+
+namespace List
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
+theorem toArray_concat {as : List α} {x : α} :
+    (as ++ [x]).toArray = as.toArray.push x := by
+  apply ext'
+  simp
+
+end List
+
+namespace Array
+
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
+theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
+  simp
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
+
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
+abbrev foldl_data_eq_map := @foldl_toList_eq_map
+
+@[deprecated toList_mkArray (since := "2024-09-09")]
+abbrev mkArray_data := @toList_mkArray
+
+@[deprecated mem_toList (since := "2024-09-09")]
+abbrev mem_data := @mem_toList
+
+@[deprecated getElem_mem (since := "2024-10-17")]
+abbrev getElem?_mem := @getElem_mem
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-10-17")]
+abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-09-09")]
+abbrev getElem_fin_eq_data_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_mem_toList (since := "2024-09-09")]
+abbrev getElem_mem_data := @getElem_mem_toList
+
+@[deprecated getElem?_eq_getElem?_toList (since := "2024-10-17")]
+abbrev getElem?_eq_toList_getElem? := @getElem?_eq_getElem?_toList
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
+theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
+abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
+
+@[deprecated get?_eq_get?_toList (since := "2024-10-17")]
+abbrev get?_eq_toList_get? := @get?_eq_get?_toList
+
+@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
+abbrev get?_eq_data_get? := @get?_eq_get?_toList
+
+@[deprecated toList_set (since := "2024-09-09")]
+abbrev data_set := @toList_set
+
+@[deprecated toList_swap (since := "2024-09-09")]
+abbrev data_swap := @toList_swap
+
+@[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
+
+@[deprecated toList_pop (since := "2024-09-09")] abbrev data_pop := @toList_pop
+
+@[deprecated size_eq_length_toList (since := "2024-09-09")]
+abbrev size_eq_length_data := @size_eq_length_toList
+
+@[deprecated toList_range (since := "2024-09-09")]
+abbrev data_range := @toList_range
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
+
+@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
+abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
+
+@[deprecated getElem_modify (since := "2024-08-08")]
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+  simp [getElem_modify h]
+
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
+
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
+
+@[deprecated toList_empty (since := "2024-09-09")]
+abbrev empty_data := @toList_empty
+
+@[deprecated getElem_append_left (since := "2024-09-30")]
+abbrev get_append_left := @getElem_append_left
+
+@[deprecated getElem_append_right (since := "2024-09-30")]
+abbrev get_append_right := @getElem_append_right
+
+@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
+abbrev any_def := @any_toList
+
+@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
+abbrev all_def := @all_toList
+
+@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
+abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
+@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
+abbrev get_extract_loop_lt := @getElem_extract_loop_lt
+@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
+abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
+@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
+abbrev get_extract_loop_ge := @getElem_extract_loop_ge
+@[deprecated getElem_extract_aux (since := "2024-09-30")]
+abbrev get_extract_aux := @getElem_extract_aux
+@[deprecated getElem_extract (since := "2024-09-30")]
+abbrev get_extract := @getElem_extract
+
+@[deprecated getElem_swap_right (since := "2024-09-30")]
+abbrev get_swap_right := @getElem_swap_right
+@[deprecated getElem_swap_left (since := "2024-09-30")]
+abbrev get_swap_left := @getElem_swap_left
+@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
+abbrev get_swap_of_ne := @getElem_swap_of_ne
+@[deprecated getElem_swap (since := "2024-09-30")]
+abbrev get_swap := @getElem_swap
+@[deprecated getElem_swap' (since := "2024-09-30")]
+abbrev get_swap' := @getElem_swap'
+
+end Array
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -0,0 +1,64 @@
+/-
+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
+
+
+/-! ### 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
+
+end Array
--- a/src/Init/Data/Hashable.lean
+++ b/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)
--- a/src/Init/Data/List/BasicAux.lean
+++ b/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
--- a/src/Init/Data/List/MinMax.lean
+++ b/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 α} :
--- a/src/Init/Data/List/Monadic.lean
+++ b/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
--- a/src/Init/Data/Nat/Basic.lean
+++ b/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 :=
--- a/src/Init/Data/OfScientific.lean
+++ b/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) : α
--- a/src/Init/Data/Option/Attach.lean
+++ b/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}
--- a/src/Init/Data/String/Basic.lean
+++ b/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
--- a/src/Init/Data/Sum.lean
+++ b/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
--- a/src/Init/Data/Sum/Basic.lean
+++ b/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
--- a/src/Init/Data/Sum/Lemmas.lean
+++ b/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
--- a/src/Init/MetaTypes.lean
+++ b/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
--- a/src/Init/PropLemmas.lean
+++ b/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 :=
--- a/src/Init/Tactics.lean
+++ b/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
--- a/src/Lean.lean
+++ b/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
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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
--- a/src/Lean/Elab/LetRec.lean
+++ b/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

--- a/src/Lean/Elab/MutualDef.lean
+++ b/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
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/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
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/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

--- a/src/Lean/Language/Basic.lean
+++ b/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
--- a/src/Lean/LazyInitExtension.lean
+++ b/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
--- a/src/Lean/Linter/ConstructorAsVariable.lean
+++ b/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
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/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
--- a/src/Lean/Meta/Tactic/SplitIf.lean
+++ b/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.
--- a/src/Lean/Server/InfoUtils.lean
+++ b/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
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
  let li := derivedLits_arr[i]
  have li_in_derivedLits : li ∈ derivedLits := by
    rw [Array.mem_toList, ← derivedLits_arr_def]
-    simp only [li, Array.getElem?_mem]
+    simp [li, Array.getElem_mem]
  have i_in_bounds : i.1 < derivedLits.length := by
    have i_property := i.2
    simp only [derivedLits_arr_def, Array.size_mk] at i_property
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -570,7 +570,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
        rw [c_clause_rw] at pc1
        have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
          rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
          exact Exists.intro idx hidx
        rcases idx_exists with ⟨idx, hidx⟩
        specialize h1 idx idx.2
@@ -580,7 +580,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
        rw [c_clause_rw] at pc1
        have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
          rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
          exact Exists.intro idx hidx
        rcases idx_exists with ⟨idx, hidx⟩
        specialize h1 idx idx.2
@@ -595,7 +595,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
      rw [c_clause_rw] at pc1
      have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
        rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
        exact Exists.intro idx hidx
      rcases idx_exists with ⟨idx, hidx⟩
      apply Exists.intro idx ∘ And.intro idx.2
@@ -606,7 +606,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
      rw [c_clause_rw] at pc1
      have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
        rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
        exact Exists.intro idx hidx
      rcases idx_exists with ⟨idx, hidx⟩
      apply Exists.intro idx ∘ And.intro idx.2
--- a/src/lake/Lake/CLI/Init.lean
+++ b/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\"
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/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
--- a/tests/lean/1021.lean.expected.out
+++ b/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 } }
--- a/tests/lean/interactive/2881.lean
+++ b/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
--- a/tests/lean/interactive/2881.lean.expected.out
+++ b/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"]}
--- a/tests/lean/linterUnusedVariables.lean
+++ b/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]
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/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`
--- a/tests/lean/run/nofun1.lean
+++ b/tests/lean/run/nofun1.lean
@@ -1,10 +1,10 @@
-theorem Sum.inl_ne_inr : inl a ≠ inr b := nofun
+theorem Sum.inl_ne_inr' : inl a ≠ inr b := nofun

-theorem Sum.inr_ne_inl : inr b ≠ inl a := nofun
+theorem Sum.inr_ne_inl' : inr b ≠ inl a := nofun

-theorem Sum.inl_ne_inr' : inl a ≠ inr b := by nofun
+theorem Sum.inl_ne_inr'' : inl a ≠ inr b := by nofun

-theorem Sum.inr_ne_inl' : inr b ≠ inl a := by nofun
+theorem Sum.inr_ne_inl'' : inr b ≠ inl a := by nofun

 def f (a b : Bool) (_ : Sum.inr b ≠ Sum.inl a) : Nat := 0
Author	SHA1	Message	Date
Kim Morrison	10bdf8a9d8	chore: upstream Array.reduceOption	2024-10-18 11:21:17 +11:00
David Thrane Christiansen	d6a7eb3987	feat: add Hashable instance for Char (#5747 ) I needed this in downstream code, and it seems to make the most sense to just contribute it here.	2024-10-17 14:46:10 +00:00
Sebastian Ullrich	fc5e3cc66e	fix: do not force snapshot tree too early (#5752 ) This turns out to be the issue behind #5736, though really it is yet another indicator of a general thread pool weakness.	2024-10-17 12:23:34 +00:00
Marc Huisinga	372f344155	fix: some goal state issues (#5677 ) This PR resolves the following issues related to goal state display: 1. In a new line after a `case` tactic with a completed proof, the state of the proof in the `case` would be displayed, not the proof state after the `case` 1. In the range of `next =>` / `case' ... =>`, the state of the proof in the corresponding case would not be displayed, whereas this is true for `case` 1. In the `suffices ... by` tactic, the tactic state of the `by` block was not displayed after the `by` and before the first tactic The incorrect goal state after `case` was caused by `evalCase` adding a `TacticInfo` with the full block proof state for the full range of the `case` block that the goal state selection has no means of distinguishing from the `TacticInfo` with the same range that contains the state after the whole `case` block. Narrowing the range of this `TacticInfo` to `case ... =>` fixed this issue. The lack of a case proof state on `next =>` was caused by the `case` syntax that `next` expands to receiving noncanonical synthetic `SourceInfo`, which is usually ignored by the language server. Adding a token antiquotation for `next` fixed this issue. The lack of a case proof state on `case' ... =>` was caused by `evalCase'` not adding a `TacticInfo` with the full block state to the range of `case' ... =>`. Adding this `TacticInfo` fixed this issue. The tactic state of the block not being displayed after the `by` was caused by the macro expansion of `suffices` to `have` not transferring the trailing whitespace of the `by`. Ensuring that this trailing whitespace information is transferred fixed this issue. Fixes #2881.	2024-10-17 12:09:54 +00:00
Sebastian Ullrich	f2ac0d03c6	perf: do not lint unused variables defined in tactics by default (#5338 ) Should ensure we visit at most as many expr nodes as in the final expr instead of many possibly overlapping mvar assignments. This is likely the only way we can ensure acceptable performance in all cases. --------- Co-authored-by: Kim Morrison <kim@tqft.net>	2024-10-17 09:55:11 +00:00
Joachim Breitner	08d8a0873e	doc: remove docstring from implicitDefEqProofs (#5751 ) this option was added in `fb97275dcb` to prepare for #4595, due to boostrapping issues, but #4595 has not landed yet. This is be very confusing when people discover this option and try to use it (as I did). So let's clearly mark this as not yet implemented on `master`, and add the docstring only with #4595.	2024-10-17 09:38:52 +00:00
Sebastian Ullrich	68b0471de9	chore: remove `SplitIf.ext` cache (#5571 ) Incompatible as is with parallelism; let's first check if it has any impact at all	2024-10-17 09:36:00 +00:00
Kim Morrison	3a34a8e0d1	chore: move Array.mapIdx lemmas to new file (#5748 )	2024-10-17 05:54:25 +00:00
Kim Morrison	6fa75e346a	chore: upstream List.foldxM_map (#5697 )	2024-10-17 04:30:08 +00:00
Eric Wieser	2669fb525f	feat: change `lake new math` to use `autoImplicit false` (#5715 ) The reality is that almost every math project uses this setting already, even if it is not the default: * `36b7d4a6d0/lakefile.lean (L7)` * `9ea3a96243/lakefile.lean (L45)` * `97755eaae3/lakefile.toml (L6)` * `fb92dbf97f/lakefile.lean (L7)` * `c8569b3d39/lakefile.toml (L6)` * `c7fae107fd/lakefile.lean (L8)` * `1d891c770d/lakefile.lean (L27)` The fact that MIL uses it is particularly notable, as it means that newcomers have an unexpected surprise when they want to take on a brand new project. --- I don't know whether this is `chore`, `feat`, `fix`, `refactor`, or something else.	2024-10-17 04:29:48 +00:00
Eric Wieser	8632b79023	doc: point out that `OfScientific` is called with raw literals (#5725 )	2024-10-17 04:29:00 +00:00
Kim Morrison	e8970463d1	fix: change String.dropPrefix? signature (#5745 )	2024-10-17 03:51:45 +00:00
Kim Morrison	69e8cd3d8a	chore: cleanup in Array/Lemmas (#5744 )	2024-10-17 03:36:26 +00:00
Kim Morrison	565ac23b78	chore: move Antisymm to Std.Antisymm (#5740 )	2024-10-17 02:26:55 +00:00
Kim Morrison	c1750f4316	chore: upstream basic material on Sum (#5741 )	2024-10-17 01:27:41 +00:00
Kim Morrison	092c87a70f	chore: upstream ne_of_apply_ne (#5743 )	2024-10-17 01:24:01 +00:00
Kim Morrison	b8fc6c593a	chore: upstream ne_of_mem_of_not_mem (#5742 )	2024-10-17 01:18:23 +00:00