diff --git a/Std/CodeAction/Basic.lean b/Std/CodeAction/Basic.lean
index 17f8b2cac8..7302aaa9c5 100644
--- a/Std/CodeAction/Basic.lean
+++ b/Std/CodeAction/Basic.lean
@@ -147,7 +147,7 @@ partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
   (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
     Option (ContextInfo × InfoTree) :=
   match t with
-  | .context ctx t => findInfoTree? kind tgtRange ctx t f canonicalOnly
+  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
   | node@(.node i ts) => do
     if let some ctx := ctx? then
       if let some range := i.stx.getRange? canonicalOnly then
diff --git a/Std/Data/Array/Init/Basic.lean b/Std/Data/Array/Init/Basic.lean
index 444b5aec4e..5b44d9227d 100644
--- a/Std/Data/Array/Init/Basic.lean
+++ b/Std/Data/Array/Init/Basic.lean
@@ -29,7 +29,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by _ => n - i
+termination_by n - i
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
diff --git a/Std/Data/Array/Init/Lemmas.lean b/Std/Data/Array/Init/Lemmas.lean
index ba9ae7ec4e..39d92676b8 100644
--- a/Std/Data/Array/Init/Lemmas.lean
+++ b/Std/Data/Array/Init/Lemmas.lean
@@ -152,7 +152,7 @@ where
     · rw [← List.get_drop_eq_drop _ i ‹_›]
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
-termination_by aux => arr.size - i
+  termination_by arr.size - i
 
 theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
     (motive : Nat → Prop) (h0 : motive 0)
@@ -262,9 +262,9 @@ theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Arra
         | true, h => .pure h
         | false, h => go hj hstop h hp
     · next hj => exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0
+    termination_by stop - j
   simp only [Array.anyM_eq_anyM_loop]
   exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..
-termination_by go => stop - j
 
 theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
     (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)
diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean
index 4a85a12919..3692f0cceb 100644
--- a/Std/Data/Array/Lemmas.lean
+++ b/Std/Data/Array/Lemmas.lean
@@ -276,8 +276,8 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
       have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
+    termination_by j - i
   simp only [reverse]; split <;> simp [go]
-termination_by _ => j - i
 
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   unfold range
@@ -323,6 +323,7 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
         cases Nat.le_antisymm h₂.1 h₂.2
         exact (List.get?_reverse' _ _ h).symm
       · rfl
+    termination_by j - i
   simp only [reverse]; split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
@@ -330,7 +331,6 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
     split; {rfl}; rename_i h
     simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
     rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
-termination_by _ => j - i
 
 @[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
     (ofFn.go f i acc).size = acc.size + (n - i) := by
@@ -343,7 +343,7 @@ termination_by _ => j - i
     have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
     unfold ofFn.go
     simp [hin, this]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
 
@@ -363,7 +363,7 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     | inr hj => simp [get_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
@@ -427,8 +427,8 @@ theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Arr
         ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
         List.zipWith f (List.drop i as.data) (List.drop i bs.data)
       simp only [List.get_cons_drop]
+    termination_by as.size - i
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
-termination_by loop i _ _ _ => as.size - i
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
diff --git a/Std/Data/Array/Match.lean b/Std/Data/Array/Match.lean
index 36432a756b..f5ff981777 100644
--- a/Std/Data/Array/Match.lean
+++ b/Std/Data/Array/Match.lean
@@ -45,7 +45,7 @@ def PrefixTable.step [BEq α] (t : PrefixTable α) (x : α) : Fin (t.size+1) →
         ⟨k+1, Nat.succ_lt_succ hsz⟩
       else cont ()
     else cont ()
-termination_by _ k => k.val
+termination_by k => k.val
 
 /-- Extend a prefix table by one element
 
diff --git a/Std/Data/Array/Merge.lean b/Std/Data/Array/Merge.lean
index be301a9fb9..fc7727be02 100644
--- a/Std/Data/Array/Merge.lean
+++ b/Std/Data/Array/Merge.lean
@@ -40,7 +40,7 @@ where
         have : xs.size + ys.size - (i + j + 1) < xs.size + ys.size - (i + j) :=
           Nat.sub_succ_lt_self _ _ hij
         go (acc.push y) i (j + 1)
-termination_by go => xs.size + ys.size - (i + j)
+  termination_by xs.size + ys.size - (i + j)
 
 /--
 Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -83,7 +83,7 @@ where
           rw [show i + j + 2 = (i + 1) + (j + 1) by simp_arith]
           exact Nat.add_le_add hi hj
         go (acc.push (merge x y)) (i + 1) (j + 1)
-termination_by go => xs.size + ys.size - (i + j)
+    termination_by xs.size + ys.size - (i + j)
 
 /--
 Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -130,7 +130,7 @@ where
         go (acc.push hd) (i + 1) x
     else
       acc.push hd
-termination_by _ i _ => xs.size - i
+  termination_by xs.size - i
 
 /--
 Deduplicate a sorted array. The array must be sorted with to an order which
diff --git a/Std/Data/BinomialHeap/Basic.lean b/Std/Data/BinomialHeap/Basic.lean
index e21a79d9bc..8f2ed693bb 100644
--- a/Std/Data/BinomialHeap/Basic.lean
+++ b/Std/Data/BinomialHeap/Basic.lean
@@ -140,7 +140,7 @@ by rank and `merge` maintains this invariant.
       else if t₂.rankGT r
         then merge le t₁ (.cons r a n t₂)
         else .cons r a n (merge le t₁ t₂)
-termination_by _ s₁ s₂ => s₁.length + s₂.length
+termination_by s₁ s₂ => s₁.length + s₂.length
 
 /--
 `O(log n)`. Convert a `HeapNode` to a `Heap` by reversing the order of the nodes
@@ -219,7 +219,7 @@ theorem Heap.realSize_merge (le) (s₁ s₂ : Heap α) :
       rw [combine] at eq; split at eq <;> cases eq <;>
         simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
     split <;> split <;> simp [IH₁, IH₂, IH₃, this, Nat.add_assoc, Nat.add_left_comm]
-termination_by _ => s₁.length + s₂.length
+termination_by s₁.length + s₂.length
 
 private def FindMin.HasSize (res : FindMin α) (n : Nat) : Prop :=
   ∃ m,
@@ -280,7 +280,7 @@ by repeatedly pulling the minimum element out of the heap.
   | some (hd, tl) => do
     have : tl.realSize < s.realSize := by simp_arith [Heap.realSize_deleteMin eq]
     foldM le tl (← f init hd) f
-termination_by _ => s.realSize
+termination_by s.realSize
 
 /--
 `O(n log n)`. Fold over the elements of a heap in increasing order,
@@ -402,7 +402,7 @@ theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
     · let ⟨ih₁, ih₂⟩ := merge' ht₁ ht₂
       exact ⟨⟨Nat.le_succ_of_le hr₁, this, ih₁.of_rankGT (ih₂ (iff_of_false hl₁ hl₂))⟩,
         fun _ => Nat.lt_succ_of_le hr₁⟩
-termination_by _ => s₁.length + s₂.length
+termination_by s₁.length + s₂.length
 
 theorem Heap.WF.merge (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) : (merge le s₁ s₂).WF le n :=
   (merge' h₁ h₂).1
diff --git a/Std/Data/ByteArray.lean b/Std/Data/ByteArray.lean
index a874883aba..4652153d5c 100644
--- a/Std/Data/ByteArray.lean
+++ b/Std/Data/ByteArray.lean
@@ -133,7 +133,7 @@ def ofFn (f : Fin n → UInt8) : ByteArray where
 private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
   go (i : Nat) (acc : ByteArray) : ByteArray :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by _ => n - i
+termination_by n - i
 
 @[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by
   funext n f; ext; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty]
@@ -141,4 +141,4 @@ where
   ofFnAux_data {n} (f : Fin n → UInt8) (i) {acc} :
       (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by
     rw [ofFnAux.go, Array.ofFn.go]; split; rw [ofFnAux_data f (i+1), push_data]; rfl
-  termination_by _ => n - i
+  termination_by n - i
diff --git a/Std/Data/Fin/Basic.lean b/Std/Data/Fin/Basic.lean
index 7ba94ef582..52df57dd4e 100644
--- a/Std/Data/Fin/Basic.lean
+++ b/Std/Data/Fin/Basic.lean
@@ -60,7 +60,7 @@ def list (n) : List (Fin n) := (enum n).data
   /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
-termination_by loop i => n - i
+  termination_by n - i
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where
diff --git a/Std/Data/Fin/Iterate.lean b/Std/Data/Fin/Iterate.lean
index 6c6076bddd..c21fdffd89 100644
--- a/Std/Data/Fin/Iterate.lean
+++ b/Std/Data/Fin/Iterate.lean
@@ -21,7 +21,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
   else
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     cast (congrArg P p) a
-  termination_by hIterateFrom i _ _ => n - i
+  termination_by n - i
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a
diff --git a/Std/Data/Fin/Lemmas.lean b/Std/Data/Fin/Lemmas.lean
index d9c9869087..9e8d193a67 100644
--- a/Std/Data/Fin/Lemmas.lean
+++ b/Std/Data/Fin/Lemmas.lean
@@ -680,7 +680,7 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
   else
     let j : Fin n := ⟨i, Nat.lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩
     cast _ (reverseInduction last cast j.succ)
-termination_by _ => n + 1 - i
+termination_by n + 1 - i
 decreasing_by decreasing_with
   -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
@@ -802,24 +802,24 @@ theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list
 @[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
     Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HAdd.hAdd, Add.add, Fin.add]
+  simp [Fin.ofNat', Fin.add_def]
 
 @[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
     x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HAdd.hAdd, Add.add, Fin.add]
+  simp [Fin.ofNat', Fin.add_def]
 
 /-! ### sub -/
 
 @[simp] theorem ofNat'_sub (x : Nat) (lt : 0 < n) (y : Fin n) :
     Fin.ofNat' x lt - y = Fin.ofNat' (x + (n - y.val)) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HSub.hSub, Sub.sub, Fin.sub]
+  simp [Fin.ofNat', Fin.sub_def]
 
 @[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
     x - Fin.ofNat' y lt = Fin.ofNat' (x.val + (n - y % n)) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HSub.hSub, Sub.sub, Fin.sub]
+  simp [Fin.ofNat', Fin.sub_def]
 
 /-! ### mul -/
 
diff --git a/Std/Data/HashMap/Basic.lean b/Std/Data/HashMap/Basic.lean
index 168c47c299..9635d17ce3 100644
--- a/Std/Data/HashMap/Basic.lean
+++ b/Std/Data/HashMap/Basic.lean
@@ -151,7 +151,7 @@ where
       let target := es.foldl reinsertAux target
       go (i+1) source target
     else target
-termination_by _ i source _ => source.size - i
+  termination_by source.size - i
 
 /--
 Inserts key-value pair `a, b` into the map.
diff --git a/Std/Data/HashMap/WF.lean b/Std/Data/HashMap/WF.lean
index d5cc2a7058..82f1f9758e 100644
--- a/Std/Data/HashMap/WF.lean
+++ b/Std/Data/HashMap/WF.lean
@@ -108,7 +108,7 @@ where
       simp
       have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm
       rwa [List.getD_eq_get?, List.get?_eq_get, Option.getD_some] at this
-termination_by go i source _ _ => source.size - i
+  termination_by source.size - i
 
 theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α × β)} {i : Nat}
     (hl₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], l.Pairwise fun a b => ¬(a.1 == b.1))
@@ -170,7 +170,7 @@ where
           refine ⟨Nat.le_of_lt this, fun _ h h' => Nat.ne_of_lt this ?_⟩
           exact LawfulHashable.hash_eq h' ▸ hs₂ _ H _ h
     · exact ht.1
-termination_by go i source _ _ _ _ => source.size - i
+  termination_by source.size - i
 
 theorem insert_size [BEq α] [Hashable α] {m : Imp α β} {k v}
     (h : m.size = m.buckets.size) :
diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 84900593c9..9a861fdf18 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -128,7 +128,7 @@ where
       iter n next
     else
       guess
-termination_by iter guess => guess
+  termination_by guess
 
 /-!
 ### testBit
diff --git a/Std/Data/PairingHeap.lean b/Std/Data/PairingHeap.lean
index a4d192b44f..fbcdcdcb7f 100644
--- a/Std/Data/PairingHeap.lean
+++ b/Std/Data/PairingHeap.lean
@@ -173,7 +173,7 @@ by repeatedly pulling the minimum element out of the heap.
   | some (hd, tl) =>
     have : tl.size < s.size := by simp_arith [Heap.size_deleteMin_lt eq]
     do foldM le tl (← f init hd) f
-termination_by _ => s.size
+termination_by s.size
 
 /--
 `O(n log n)`. Fold over the elements of a heap in increasing order,
diff --git a/Std/Data/RBMap/Basic.lean b/Std/Data/RBMap/Basic.lean
index 2080cde801..bf69dc8b5a 100644
--- a/Std/Data/RBMap/Basic.lean
+++ b/Std/Data/RBMap/Basic.lean
@@ -360,7 +360,7 @@ def append : RBNode α → RBNode α → RBNode α
     | bc               => balLeft a x (node black bc y d)
   | a@(node black ..), node red b x c => node red (append a b) x c
   | node red a x b, c@(node black ..) => node red a x (append b c)
-termination_by _ x y => x.size + y.size
+termination_by x y => x.size + y.size
 
 /-! ## erase -/
 
diff --git a/Std/Data/RBMap/WF.lean b/Std/Data/RBMap/WF.lean
index 1d6a76c350..ce8fb81184 100644
--- a/Std/Data/RBMap/WF.lean
+++ b/Std/Data/RBMap/WF.lean
@@ -308,7 +308,7 @@ protected theorem All.append (hl : l.All p) (hr : r.All p) : (append l r).All p
     have := hb.append hc; split <;> simp_all [All.balLeft]
   · simp_all [hl.append hr.2.1]
   · simp_all [hl.2.2.append hr]
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-- The `append` function preserves the ordering invariants. -/
 protected theorem Ordered.append {l : RBNode α} {v : α} {r : RBNode α}
@@ -341,7 +341,7 @@ protected theorem Ordered.append {l : RBNode α} {v : α} {r : RBNode α}
     exact ⟨(vx.trans_r lv).append bx, yc, hl.append lv vb hb, hc⟩
   · have ⟨xv, _, bv⟩ := lv; have ⟨ax, xb, ha, hb⟩ := hl
     exact ⟨ax, xb.append (xv.trans_l vr), ha, hb.append bv vr hr⟩
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-- The balance properties of the `append` function. -/
 protected theorem Balanced.append {l r : RBNode α}
@@ -380,7 +380,7 @@ protected theorem Balanced.append {l r : RBNode α}
   · have .red ha hb := hl; have IH := hb.append hr
     have .black hc hd := hr; have ⟨c, IH⟩ := IH.of_false (· rfl rfl)
     exact .redred (fun.) ha IH
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-! ## erase -/
 
diff --git a/Std/Data/String/Basic.lean b/Std/Data/String/Basic.lean
index 014d2fc9b6..072fbe0222 100644
--- a/Std/Data/String/Basic.lean
+++ b/Std/Data/String/Basic.lean
@@ -91,7 +91,7 @@ where
         spos
     else
       spos
-termination_by loop => s.stopPos.byteIdx - spos.byteIdx
+  termination_by s.stopPos.byteIdx - spos.byteIdx
 
 /--
 Returns the longest common suffix of two substrings.
@@ -112,7 +112,7 @@ where
         spos
     else
       spos
-termination_by loop => spos.byteIdx
+  termination_by spos.byteIdx
 
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
diff --git a/Std/Lean/Delaborator.lean b/Std/Lean/Delaborator.lean
index 4c70f3ac31..98aa890e01 100644
--- a/Std/Lean/Delaborator.lean
+++ b/Std/Lean/Delaborator.lean
@@ -7,36 +7,6 @@ import Lean.PrettyPrinter
 
 open Lean PrettyPrinter Delaborator SubExpr
 
-/--
-This is similar to `withAppFnArgs` but it handles construction of an "over-application".
-For example, suppose we want to implement a delaborator for applications of `f : Foo A → A`
-like `f x` as `F[x]`, but because `A` is a type variable we might encounter a term of the form
-`@f (A → B) x y` which has an additional argument `y`.
-
-Most of the built in delaborators will deliberately fail on such an example, resulting in
-delaborated syntax `f x y`, but this combinator can be used if we want to display `F[x] y`
-instead.
-
-* `arity`: the expected number of arguments to `f`.
-  The combinator will fail if fewer than this number of arguments are passed
-* `x`: constructs data corresponding to the main application (`f x` in the example)
--/
-def Lean.PrettyPrinter.Delaborator.withOverApp (arity : Nat) (x : Delab) : Delab := do
-  let n := (← getExpr).getAppNumArgs
-  guard (n ≥ arity)
-  let kinds ← getParamKinds
-  let rec
-  /-- Inner loop of `withOverApp`. -/
-  loop : Nat → DelabM (Term × Array Term)
-  | 0 => return (← x, #[])
-  | n+1 => do
-    let mut (fnStx, args) ← withAppFn (loop n)
-    if kinds.get? (n + arity) |>.all (·.bInfo.isExplicit) then
-      args := args.push (← withAppArg delab)
-    pure (fnStx, args)
-  let (fnStx, argStxs) ← loop (n - arity)
-  return Syntax.mkApp fnStx argStxs
-
 /-- Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first
 argument is implicit, which is what the default `toMessageData` for `Expr` does.
diff --git a/Std/Lean/InfoTree.lean b/Std/Lean/InfoTree.lean
index f0977a19e9..d69450d575 100644
--- a/Std/Lean/InfoTree.lean
+++ b/Std/Lean/InfoTree.lean
@@ -14,7 +14,7 @@ partial def InfoTree.foldInfo' (init : α) (f : ContextInfo → InfoTree → α
 where
   /-- `foldInfo'.go` is like `foldInfo'` but with an additional outer context parameter `ctx?`. -/
   go ctx? a
-  | context ctx t => go ctx a t
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
   | t@(node i ts) =>
     let a := match ctx? with
       | none => a
diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
index b75dacbf57..b594d2099c 100644
--- a/Std/Lean/Meta/Basic.lean
+++ b/Std/Lean/Meta/Basic.lean
@@ -407,7 +407,7 @@ where
         match ← observing? (f g) with
         | some gs' => go n true gs' (gs::stk) acc
         | none => go n p gs stk (acc.push g)
-termination_by _ n p gs stk _ => (n, stk, gs)
+termination_by n p gs stk _ => (n, stk, gs)
 
 /--
 `repeat' f` runs `f` on all of the goals to produce a new list of goals,
diff --git a/Std/Lean/Meta/DiscrTree.lean b/Std/Lean/Meta/DiscrTree.lean
index 9250e07855..d6940b31bb 100644
--- a/Std/Lean/Meta/DiscrTree.lean
+++ b/Std/Lean/Meta/DiscrTree.lean
@@ -165,11 +165,11 @@ Inserts a new key into a discrimination tree,
 but only if it is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
 def insertIfSpecific [BEq α] (d : DiscrTree α)
-    (keys : Array DiscrTree.Key) (v : α) (config : WhnfCoreConfig) : DiscrTree α :=
+    (keys : Array DiscrTree.Key) (v : α) : DiscrTree α :=
   if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
-    d.insertCore keys v config
+    d.insertCore keys v
 
 variable {m : Type → Type} [Monad m]
 
diff --git a/Std/Lean/Meta/LazyDiscrTree.lean b/Std/Lean/Meta/LazyDiscrTree.lean
index ab45798e64..466231576d 100644
--- a/Std/Lean/Meta/LazyDiscrTree.lean
+++ b/Std/Lean/Meta/LazyDiscrTree.lean
@@ -558,8 +558,8 @@ private def MatchResult.push (r : MatchResult α) (score : Nat) (e : Array α) :
           loop (a.push #[])
         else
           { elts := a.push #[e] }
+    termination_by score - a.size
     loop r.elts
-  termination_by loop _ => score - a.size
 
 private partial def MatchResult.toArray (mr : MatchResult α) : Array α :=
     loop (Array.mkEmpty n) mr.elts
@@ -845,7 +845,7 @@ private def createImportedEnvironmentSeq (env : Environment)
               go d tree (start+1) stop
             else
               toFlat d tree
-  termination_by go _ idx stop => stop - idx
+    termination_by stop - start
 
 /-- Get the results of each task and merge using combining function -/
 private def combineGet [Append α] (z : α) (tasks : Array (Task α)) : α :=
@@ -873,9 +873,9 @@ def createImportedEnvironment (env : Environment)
           tasks.push <$> (createImportedEnvironmentSeq env act start n).asTask
         else
           pure tasks
+    termination_by env.header.moduleData.size - idx
   let tasks ← go #[] 0 0 0
   let r := combineGet default tasks
   if p : r.errors.size > 0 then
     throw r.errors[0].exception
   pure <| r.tree.toLazy
-  termination_by go _ idx => env.header.moduleData.size - idx
diff --git a/Std/Lean/Meta/Simp.lean b/Std/Lean/Meta/Simp.lean
index 7c9793b5f4..a00a5727d0 100644
--- a/Std/Lean/Meta/Simp.lean
+++ b/Std/Lean/Meta/Simp.lean
@@ -53,15 +53,18 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     simpOnlyBuiltins.foldlM (·.addConst ·) {}
   else
     pure simpTheorems
+  let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
     config       := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
-    let mut simpTheorems := r.ctx.simpTheorems
+    let ctx := r.ctx
+    let mut simpTheorems := ctx.simpTheorems
+    let simprocs := r.simprocs
     /-
     When using `zeta := false`, we do not expand let-declarations when using `[*]`.
     Users must explicitly include it in the list.
@@ -70,7 +73,9 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    return { ctx := { r.ctx with simpTheorems }, dischargeWrapper }
+    let ctx := { ctx with simpTheorems }
+    return { ctx, simprocs, dischargeWrapper }
+
 
 end Simp
 
diff --git a/Std/Tactic/Ext/Attr.lean b/Std/Tactic/Ext/Attr.lean
index 88877e16fc..e7b19480ef 100644
--- a/Std/Tactic/Ext/Attr.lean
+++ b/Std/Tactic/Ext/Attr.lean
@@ -39,7 +39,7 @@ initialize extExtension :
     SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
   registerSimpleScopedEnvExtension {
     addEntry := fun { tree, erased } thm =>
-      { tree := tree.insertCore thm.keys thm extExt.config, erased := erased.erase thm.declName }
+      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
     initial := {}
   }
 
diff --git a/Std/Tactic/LibrarySearch.lean b/Std/Tactic/LibrarySearch.lean
index 209a5416a8..e82898cdce 100644
--- a/Std/Tactic/LibrarySearch.lean
+++ b/Std/Tactic/LibrarySearch.lean
@@ -88,7 +88,7 @@ def cachePath : IO FilePath := do
 private def addPath [BEq α] (config : WhnfCoreConfig) (tree : DiscrTree α) (tp : Expr) (v : α) :
     MetaM (DiscrTree α) := do
   let k ← DiscrTree.mkPath tp config
-  pure <| tree.insertCore k v config
+  pure <| tree.insertCore k v
 
 /-- Adds a constant with given name to tree. -/
 private def updateTree (config : WhnfCoreConfig) (tree : DiscrTree (Name × DeclMod))
diff --git a/Std/Tactic/Lint/Misc.lean b/Std/Tactic/Lint/Misc.lean
index 1d328b63cc..77773eb5a7 100644
--- a/Std/Tactic/Lint/Misc.lean
+++ b/Std/Tactic/Lint/Misc.lean
@@ -226,11 +226,13 @@ Return a list of unused `let_fun` terms in an expression.
 def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do
   let res ← IO.mkRef #[]
   forEachExpr e fun e => do
-    let some (n, t, _v, b) := e.letFun? | return
-    if n.isInternal then return
-    if b.hasLooseBVars then return
-    let msg ← addMessageContextFull m!"unnecessary have {n.eraseMacroScopes} : {t}"
-    res.modify (·.push msg)
+    match e.letFun? with
+    | some (n, t, _, b) =>
+      if n.isInternal then return
+      if b.hasLooseBVars then return
+      let msg ← addMessageContextFull m!"unnecessary have {n.eraseMacroScopes} : {t}"
+      res.modify (·.push msg)
+    | _ => return
   res.get
 
 /-- A linter for checking that declarations don't have unused term mode have statements. We do not
diff --git a/Std/Tactic/Lint/Simp.lean b/Std/Tactic/Lint/Simp.lean
index 525107e803..b467032f0c 100644
--- a/Std/Tactic/Lint/Simp.lean
+++ b/Std/Tactic/Lint/Simp.lean
@@ -112,10 +112,10 @@ https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20for
     unless ← isSimpTheorem declName do return none
     let ctx := { ← Simp.Context.mkDefault with config.decide := false }
     checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
-      let (⟨lhs', prf1, _⟩, prf1Lems) ←
+      let ({ expr := lhs', proof? := prf1, .. }, prf1Lems) ←
         decorateError "simplify fails on left-hand side:" <| simp lhs ctx
       if prf1Lems.contains (.decl declName) then return none
-      let (⟨rhs', _, _⟩, used_lemmas) ←
+      let ({ expr := rhs', .. }, used_lemmas) ←
         decorateError "simplify fails on right-hand side:" <| simp rhs ctx (usedSimps := prf1Lems)
       let lhs'EqRhs' ← isSimpEq lhs' rhs' (whnfFirst := false)
       let lhsInNF ← isSimpEq lhs' lhs
diff --git a/Std/Tactic/NormCast.lean b/Std/Tactic/NormCast.lean
index e894460106..0dafd4770a 100644
--- a/Std/Tactic/NormCast.lean
+++ b/Std/Tactic/NormCast.lean
@@ -24,13 +24,13 @@ initialize registerTraceClass `Tactic.norm_cast
 /-- Prove `a = b` using the given simp set. -/
 def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) := do
   let go : SimpM (Option Simp.Result) := do
-    let methods := Simp.DefaultMethods.methods
-    let a' ← Simp.simp a methods
-    let b' ← Simp.simp b methods
+    let a' ← Simp.simp a
+    let b' ← Simp.simp b
     unless ← isDefEq a'.expr b'.expr do return none
-    mkEqTrans a' (← mkEqSymm b b')
+    a'.mkEqTrans (← mkEqSymm b b')
   withReducible do
-    (go { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
 
 /-- Prove `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -136,9 +136,10 @@ It tries to rewrite an expression using the elim and move lemmas.
 On failure, it calls the splitting procedure heuristic.
 -/
 partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-  let r ← Simp.rewrite? e up.post up.erased prove (tag := "squash") (rflOnly := false)
+  let r ← withDischarger prove do
+    Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
   let r := r.getD { expr := e }
-  let r ← mkEqTrans r <|← splittingProcedure r.expr
+  let r ← r.mkEqTrans (← splittingProcedure r.expr)
   if r.expr == e then return Simp.Step.done {expr := e}
   return Simp.Step.visit r
 
@@ -169,7 +170,7 @@ def derive (e : Expr) : MetaM Simp.Result := do
   }
   let congrTheorems ← Meta.getSimpCongrTheorems
 
-  let r := {expr := e}
+  let r : Simp.Result := { expr := e }
 
   let withTrace phase := withTraceNode `Tactic.norm_cast fun
     | .ok r => return m!"{r.expr} (after {phase})"
@@ -178,17 +179,17 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    Simp.mkEqTrans r (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    Simp.mkEqTrans r (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    mkEqTrans r (← simp r.expr { simpTheorems, config, congrTheorems }).1
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
 
   return r
 
@@ -204,7 +205,7 @@ elab "mod_cast " e:term : term <= expectedType => do
   let eTy' ← derive eTy
   unless ← isDefEq eTy'.expr expectedType'.expr do
     throwTypeMismatchError "mod_cast" expectedType'.expr eTy'.expr e
-  let eTy_eq_expectedType ← mkEqTrans eTy' (← mkEqSymm expectedType expectedType')
+  let eTy_eq_expectedType ← eTy'.mkEqTrans (← mkEqSymm expectedType expectedType')
   mkCast eTy_eq_expectedType e
 
 open Tactic Parser.Tactic Elab.Tactic
@@ -325,8 +326,8 @@ syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 @[inherit_doc pushCast, tactic pushCast] def evalPushCast : Tactic := fun stx => do
-  let { ctx, dischargeWrapper, .. } ← withMainContext do
+  let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext' (← pushCastExt.getTheorems) stx (eraseLocal := false)
   let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? =>
-    discard <| simpLocation ctx discharge? (expandOptLocation stx[5])
+    discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
diff --git a/Std/Tactic/Omega/OmegaM.lean b/Std/Tactic/Omega/OmegaM.lean
index 093e4c851c..16e7d0923e 100644
--- a/Std/Tactic/Omega/OmegaM.lean
+++ b/Std/Tactic/Omega/OmegaM.lean
@@ -153,7 +153,6 @@ Return its index, and, if it is new, a collection of interesting facts about the
 def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do
   let c ← getThe State
   for h : i in [:c.atoms.size] do
-    have : i < c.atoms.size := h.2
     if ← isDefEq e c.atoms[i] then
       return (i, none)
   trace[omega] "New atom: {e}"
diff --git a/Std/Tactic/RCases.lean b/Std/Tactic/RCases.lean
index 37157ad50c..68c8cf75cb 100644
--- a/Std/Tactic/RCases.lean
+++ b/Std/Tactic/RCases.lean
@@ -310,7 +310,7 @@ def processConstructor (ref : Syntax) (info : Array ParamInfo)
       | [p] => ([p.name?.getD `_], [p])
       | ps  => ([`_], [(bif explicit then .explicit ref else id) (.tuple ref ps)])
   else ([], [])
-termination_by _ => info.size - idx
+termination_by info.size - idx
 
 /--
 Takes a list of constructor names, and an (alternation) list of patterns, and matches each
@@ -487,10 +487,15 @@ The terminating continuation used in `rcasesCore` and `rcasesContinue`. We speci
 `α` to `Array MVarId` to collect the list of goals, and given the list of `clears`, it attempts to
 clear them from the goal and adds the goal to the list.
 -/
-def finish (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
+def finish (toTag : Array (Ident × FVarId) := #[])
+  (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
   (gs : Array MVarId) : TermElabM (Array MVarId) := do
   let cs : Array Expr := (clears.map fs.get).filter Expr.isFVar
-  gs.push <$> tryClearMany' g (cs.map Expr.fvarId!)
+  let g ← tryClearMany' g (cs.map Expr.fvarId!)
+  g.withContext do
+    for (stx, fvar) in toTag do
+      Term.addLocalVarInfo stx (fs.get fvar)
+  return gs.push g
 
 open Elab
 
@@ -511,7 +516,7 @@ partial def RCasesPatt.parse (stx : Syntax) : MetaM RCasesPatt :=
 -- extracted from elabCasesTargets
 /-- Generalize all the arguments as specified in `args` to fvars if they aren't already -/
 def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
-    MetaM (Array Expr × MVarId) := do
+    MetaM (Array Expr × Array FVarId × MVarId) := do
   let argsToGeneralize := args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
   let (fvarIdsNew, goal) ← goal.generalize argsToGeneralize
   let mut result := #[]
@@ -522,14 +527,14 @@ def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
     else
       result := result.push (mkFVar fvarIdsNew[j]!)
       j := j+1
-  pure (result, goal)
+  pure (result, fvarIdsNew[j:], goal)
 
 /--
 Given a list of targets of the form `e` or `h : e`, and a pattern, match all the targets
 against the pattern. Returns the list of produced subgoals.
 -/
-def rcases (tgts : Array (Option Name × Syntax))
-    (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
+def rcases (tgts : Array (Option Ident × Syntax))
+  (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
   let pats ← match tgts.size with
   | 0 => return [g]
   | 1 => pure [pat]
@@ -541,9 +546,11 @@ def rcases (tgts : Array (Option Name × Syntax))
       pure (.typed ref pat (← Term.exprToSyntax ty), some ty)
     | _ => pure (pat, none)
     let expr ← Term.ensureHasType ty (← Term.elabTerm tgt ty)
-    pure (pat, { expr, xName? := pat.name?, hName? : GeneralizeArg })
-  let (vs, g) ← generalizeExceptFVar g args
-  (·.toList) <$> rcasesContinue g {} #[] #[] (pats.zip vs).toList finish
+    pure (pat, { expr, xName? := pat.name?, hName? := hName?.map (·.getId) : GeneralizeArg })
+  let (vs, hs, g) ← generalizeExceptFVar g args
+  let toTag := tgts.filterMap (·.1) |>.zip hs
+  let gs ← rcasesContinue g {} #[] #[] (pats.zip vs).toList (finish (toTag := toTag))
+  pure gs.toList
 
 /--
 The `obtain` tactic in the no-target case. Given a type `T`, create a goal `|- T` and
@@ -688,7 +695,7 @@ elab (name := rcases) tk:"rcases" tgts:casesTarget,* pat:((" with " rcasesPatLo)
   | #[] => pure $ RCasesPatt.tuple tk []
   | _ => throwUnsupportedSyntax
   let tgts := tgts.getElems.map fun tgt =>
-    (if tgt.raw[0].isNone then none else some tgt.raw[0][0].getId, tgt.raw[1])
+    (if tgt.raw[0].isNone then none else some ⟨tgt.raw[0][0]⟩, tgt.raw[1])
   let g ← getMainGoal
   g.withContext do replaceMainGoal (← RCases.rcases tgts pat g)
 
diff --git a/Std/Tactic/Relation/Rfl.lean b/Std/Tactic/Relation/Rfl.lean
index 4675f3c6e0..fb14972946 100644
--- a/Std/Tactic/Relation/Rfl.lean
+++ b/Std/Tactic/Relation/Rfl.lean
@@ -24,7 +24,7 @@ def reflExt.config : WhnfCoreConfig := {}
 initialize reflExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) => dt.insertCore ks n reflExt.config
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
     initial := {}
   }
 
diff --git a/Std/Tactic/Relation/Symm.lean b/Std/Tactic/Relation/Symm.lean
index 6e09d318a3..2369a4efd6 100644
--- a/Std/Tactic/Relation/Symm.lean
+++ b/Std/Tactic/Relation/Symm.lean
@@ -27,7 +27,7 @@ def symmExt.config : WhnfCoreConfig := {}
 initialize symmExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    addEntry := fun dt (n, ks) => dt.insertCore ks n symmExt.config
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
     initial := {}
   }
 
diff --git a/Std/Tactic/SimpTrace.lean b/Std/Tactic/SimpTrace.lean
index 1496fdea11..59f9e85425 100644
--- a/Std/Tactic/SimpTrace.lean
+++ b/Std/Tactic/SimpTrace.lean
@@ -36,44 +36,10 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
 macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
 
 open TSyntax.Compat in
--- adapted from traceSimpCall
 /-- Constructs the syntax for a simp call, for use with `simp?`. -/
 def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tactic) := do
-  let mut stx := stx.unsetTrailing
-  if stx[3].isNone then
-    stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
-  let mut args := #[]
-  let mut localsOrStar := some #[]
-  let lctx ← getLCtx
-  let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
-    match thm with
-    | .decl declName inv => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← if inv then
-          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
-        else
-          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
-    | .fvar fvarId => -- local hypotheses in the context
-      if let some ldecl := lctx.find? fvarId then
-        localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
-              (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
-            some (locals.push ldecl.userName)
-          else
-            none
-      -- Note: the `if let` can fail for `simp (config := {contextual := true})` when
-      -- rewriting with a variable that was introduced in a scope. In that case we just ignore.
-    | .stx _ thmStx => -- simp theorems provided in the local invocation
-      args := args.push thmStx
-    | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`.
-      pure ()     -- We can't display them anyway.
-  if let some locals := localsOrStar then
-    args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
-  else
-    args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  pure <| stx.setArg 4 (mkNullNode argsStx)
+  let stx := stx.unsetTrailing
+  mkSimpOnly stx usedSimps
 
 elab_rules : tactic
   | `(tactic|
@@ -82,9 +48,11 @@ elab_rules : tactic
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+    let { ctx, simprocs, dischargeWrapper } ←
+      withMainContext <| mkSimpContext stx (eraseLocal := false)
     let usedSimps ← dischargeWrapper.with fun discharge? =>
-      simpLocation ctx discharge? <| (loc.map expandLocation).getD (.targets #[] true)
+      simpLocation ctx (simprocs := simprocs) discharge? <|
+        (loc.map expandLocation).getD (.targets #[] true)
     let stx ← mkSimpCallStx stx usedSimps
     TryThis.addSuggestion tk stx (origSpan? := ← getRef)
 
diff --git a/Std/Tactic/Simpa.lean b/Std/Tactic/Simpa.lean
index 0ae674f872..e2a6bb1fdd 100644
--- a/Std/Tactic/Simpa.lean
+++ b/Std/Tactic/Simpa.lean
@@ -53,59 +53,6 @@ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic
 
 open private useImplicitLambda from Lean.Elab.Term
 
--- FIXME: remove when lean4#1862 lands
-open TSyntax.Compat in
-/--
-If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
-`usedSimps` is the set of simp lemmas used by this invocation, then `mkSimpOnly`
-creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
-invocation.
--/
-private def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax.Tactic := do
-  let isSimpAll := stx[0].getAtomVal == "simp_all"
-  let mut stx := stx
-  if stx[3].isNone then
-    stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
-  let mut args := #[]
-  let mut localsOrStar := some #[]
-  let lctx ← getLCtx
-  let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
-    match thm with
-    | .decl declName inv => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← if inv then
-          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
-        else
-          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
-    | .fvar fvarId => -- local hypotheses in the context
-      if isSimpAll then
-        continue
-        -- `simp_all` uses all hypotheses anyway, so we do not need to include
-        -- them in the arguments. In fact, it would be harmful to do so:
-        -- `simp_all only [h]`, where `h` is a hypothesis, simplifies `h` to
-        -- `True` and subsequenly removes it from the context, whereas
-        -- `simp_all` does not. So to get behavior equivalent to `simp_all`, we
-        -- must omit `h`.
-      if let some ldecl := lctx.find? fvarId then
-        localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
-              (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
-            some (locals.push ldecl.userName)
-          else
-            none
-      -- Note: the `if let` can fail for `simp (config := {contextual := true})` when
-      -- rewriting with a variable that was introduced in a scope. In that case we just ignore.
-    | .stx _ thmStx => -- simp theorems provided in the local invocation
-      args := args.push thmStx
-    | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`.
-      pure ()     -- We can't display them anyway.
-  if let some locals := localsOrStar then
-    args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
-  else
-    args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  return stx.setArg 4 (mkNullNode argsStx)
 
 /-- Gets the value of the `linter.unnecessarySimpa` option. -/
 def getLinterUnnecessarySimpa (o : Options) : Bool :=
@@ -117,13 +64,14 @@ elab_rules : tactic
 | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
       $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
   let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
-  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper } ←
+    withMainContext <| mkSimpContext stx (eraseLocal := false)
   let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
   -- TODO: have `simpa` fail if it doesn't use `simp`.
   let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? => do
-    let (some (_, g), usedSimps) ←
-        simpGoal (← getMainGoal) ctx (simplifyTarget := true) (discharge? := discharge?)
+    let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
+        (simplifyTarget := true) (discharge? := discharge?)
       | if getLinterUnnecessarySimpa (← getOptions) then
           logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
     g.withContext do
@@ -135,7 +83,7 @@ elab_rules : tactic
         pure (h, g)
       else
         (← g.assert `h (← inferType e) e).intro1
-      let (result?, usedSimps) ← simpGoal g ctx (fvarIdsToSimp := #[h])
+      let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
         (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
       match result? with
       | some (xs, g) =>
@@ -151,8 +99,9 @@ elab_rules : tactic
               m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
       pure usedSimps
     else if let some ldecl := (← getLCtx).findFromUserName? `this then
-      if let (some (_, g), usedSimps) ← simpGoal g ctx (fvarIdsToSimp := #[ldecl.fvarId])
-          (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?) then
+      if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
+          (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
+          (discharge? := discharge?) then
         g.assumption; pure usedSimps
       else
         pure usedSimps
diff --git a/Std/Tactic/SqueezeScope.lean b/Std/Tactic/SqueezeScope.lean
index d967f5b719..520fa5b2e8 100644
--- a/Std/Tactic/SqueezeScope.lean
+++ b/Std/Tactic/SqueezeScope.lean
@@ -95,13 +95,14 @@ elab_rules : tactic
     let stx := tac.raw
     let usedSimps ← match stx.getKind with
     | ``Parser.Tactic.simp => do
-      let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+      let { ctx, simprocs, dischargeWrapper } ←
+        withMainContext <| mkSimpContext stx (eraseLocal := false)
       dischargeWrapper.with fun discharge? =>
-        simpLocation ctx discharge? (expandOptLocation stx[5])
+        simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
     | ``Parser.Tactic.simpAll => do
-      let { ctx, .. } ← mkSimpContext stx
+      let { ctx, simprocs, .. } ← mkSimpContext stx
         (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-      let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+      let (result?, usedSimps) ← simpAll (← getMainGoal) ctx simprocs
       match result? with
       | none => replaceMainGoal []
       | some mvarId => replaceMainGoal [mvarId]
diff --git a/Std/Util/Cache.lean b/Std/Util/Cache.lean
index 5ec7abc82f..1aa9979b1f 100644
--- a/Std/Util/Cache.lean
+++ b/Std/Util/Cache.lean
@@ -146,7 +146,7 @@ def DiscrTreeCache.mk [BEq α] (profilingName : String)
     IO (DiscrTreeCache α) :=
   let updateTree := fun name constInfo tree => do
     return (← processDecl name constInfo).foldl (init := tree) fun t (k, v) =>
-      t.insertCore k v config
+      t.insertCore k v
   let addDecl := fun name constInfo (tree₁, tree₂) =>
     return (← updateTree name constInfo tree₁, tree₂)
   let addLibraryDecl := fun name constInfo (tree₁, tree₂) =>
diff --git a/Std/WF.lean b/Std/WF.lean
index 010b9072e6..d672a79d00 100644
--- a/Std/WF.lean
+++ b/Std/WF.lean
@@ -51,7 +51,7 @@ instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
     {a : α} (t : Acc r a) : motive a t :=
   intro a (fun x h => t.inv h) (fun y hr => recC intro (t.inv hr))
-termination_by _ a h => Subtype.mk a h
+termination_by Subtype.mk a t
 
 private theorem recC_intro {motive : (a : α) → Acc r a → Sort v}
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
@@ -97,7 +97,7 @@ than the one inferred by default:
 ```
 def otherWF : WellFounded Nat := …
 def foo (n : Nat) := …
-termination_by foo n => otherWF.wrap n
+termination_by otherWF.wrap n
 ```
 -/
 def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x} :=
@@ -118,7 +118,7 @@ Workaround until Lean has native support for this. -/
 @[specialize] private def fixC {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
     (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   F x (fun y _ => fixC hwf F y)
-termination_by _ x => hwf.wrap x
+termination_by hwf.wrap x
 
 @[csimp] private theorem fix_eq_fixC : @fix = @fixC := rfl
 
diff --git a/lean-toolchain b/lean-toolchain
index bd59abf4ae..cfcdd3277d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0-rc1
diff --git a/test/rcases.lean b/test/rcases.lean
index 14e33afe30..f1c4039205 100644
--- a/test/rcases.lean
+++ b/test/rcases.lean
@@ -188,6 +188,11 @@ example (h : a ≤ 2 ∨ 2 < a) : True := by
   · guard_hyp ha1 : a ≤ 2; trivial
   · guard_hyp ha2 : 3 ≤ a; trivial
 
+example (a : Nat) : True := by
+  rcases h : a with _ | n
+  · guard_hyp h : a = 0; trivial
+  · guard_hyp h : a = n + 1; trivial
+
 inductive BaseType : Type where
   | one