diff --git a/doc/examples/interp.lean.out.expected b/doc/examples/interp.lean.out.expected
index cccbb7bd52..46321acbb3 100644
--- a/doc/examples/interp.lean.out.expected
+++ b/doc/examples/interp.lean.out.expected
@@ -1,3 +1,4 @@
 30
 interp.lean:146:4: warning: declaration uses `sorry`
+interp.lean:146:0: warning: declaration uses `sorry`
 3628800
diff --git a/src/Init/Control/Lawful/MonadAttach/Instances.lean b/src/Init/Control/Lawful/MonadAttach/Instances.lean
index 0bdc9a298a..9440e89822 100644
--- a/src/Init/Control/Lawful/MonadAttach/Instances.lean
+++ b/src/Init/Control/Lawful/MonadAttach/Instances.lean
@@ -72,11 +72,11 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT _ _))
+  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadAttach (ReaderT _ _))
+  inferInstanceAs (LawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 section
 
diff --git a/src/Init/Data/List/MinMaxIdx.lean b/src/Init/Data/List/MinMaxIdx.lean
index 32b83034dd..2e45f7e644 100644
--- a/src/Init/Data/List/MinMaxIdx.lean
+++ b/src/Init/Data/List/MinMaxIdx.lean
@@ -481,13 +481,13 @@ protected theorem maxIdxOn_nil_eq_iff_false [LE β] [DecidableLE β] {f : α →
 @[simp]
 protected theorem maxIdxOn_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
     [x].maxIdxOn f (of_decide_eq_false rfl) = 0 :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_singleton
 
 @[simp]
 protected theorem maxIdxOn_lt_length [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxIdxOn f h < xs.length :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_lt_length h
 
 protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -495,7 +495,7 @@ protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [Decidable
     {k : Nat} (hi : k < xs.length) (hle : f (xs.maxOn f h) ≤ f xs[k]) :
     xs.maxIdxOn f h ≤ k := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn] at hle ⊢
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minIdxOn_le_of_apply_getElem_le_apply_minOn h hi (by simpa [LE.le_opposite_iff] using hle)
 
 protected theorem apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β]
@@ -513,7 +513,7 @@ protected theorem getElem_maxIdxOn [LE β] [DecidableLE β] [IsLinearPreorder β
     {f : α → β} {xs : List α} (h : xs ≠ []) :
     xs[xs.maxIdxOn f h] = xs.maxOn f h := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.getElem_minIdxOn h
 
 protected theorem le_maxIdxOn_of_apply_getElem_lt_apply_getElem [LE β] [DecidableLE β] [LT β]
@@ -562,14 +562,14 @@ protected theorem maxIdxOn_cons
       else if f (xs.maxOn f h) ≤ f x then 0
       else (xs.maxIdxOn f h) + 1 := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_cons (f := f)
 
 protected theorem maxIdxOn_eq_zero_iff [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h = 0 ↔ ∀ x ∈ xs, f x ≤ f (xs.head h) := by
   simp only [List.maxIdxOn_eq_minIdxOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_eq_zero_iff h (f := f)
 
 protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -580,26 +580,26 @@ protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
       else
         xs.length + ys.maxIdxOn f hys := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_append hxs hys (f := f)
 
 protected theorem left_le_maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h ≤ (xs ++ ys).maxIdxOn f (by simp [h]) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.left_le_minIdxOn_append h
 
 protected theorem maxIdxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     (xs.take i).maxIdxOn f h ≤ xs.maxIdxOn f (List.ne_nil_of_take_ne_nil h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_take_le h
 
 @[simp]
 protected theorem maxIdxOn_replicate [LE β] [DecidableLE β] [Refl (α := β) (· ≤ ·)]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxIdxOn f h = 0 :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minIdxOn_replicate h
 
 @[simp]
diff --git a/src/Init/Data/List/MinMaxOn.lean b/src/Init/Data/List/MinMaxOn.lean
index 6182461542..25b6e091c2 100644
--- a/src/Init/Data/List/MinMaxOn.lean
+++ b/src/Init/Data/List/MinMaxOn.lean
@@ -297,13 +297,13 @@ protected theorem maxOn_cons
     (x :: xs).maxOn f (by exact of_decide_eq_false rfl) =
       if h : xs = [] then x else maxOn f x (xs.maxOn f h) := by
   simp only [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn_cons (f := f)
 
 protected theorem maxOn_cons_cons [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} :
     (a :: b :: l).maxOn f (by simp) = (maxOn f a b :: l).maxOn f (by simp) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn_cons_cons
 
 @[simp]
@@ -334,51 +334,51 @@ protected theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLea
     {xs : List α} (h : xs ≠ []) :
     xs.maxOn id h = xs.max h := by
   simp only [List.maxOn_eq_minOn]
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simpa only [List.max_eq_min] using List.minOn_id h
 
 @[simp]
 protected theorem maxOn_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} {h : xs ≠ []} : xs.maxOn f h ∈ xs :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_mem (f := f)
 
 protected theorem le_apply_maxOn_of_mem [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
     f y ≤ f (xs.maxOn f (List.ne_nil_of_mem hx)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_of_mem (f := f) hx
 
 protected theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) ≤ b ↔ ∀ x ∈ xs, f x ≤ b := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_iff (f := f) h
 
 protected theorem le_apply_maxOn_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     b ≤ f (xs.maxOn f h) ↔ ∃ x ∈ xs, b ≤ f x := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_iff (f := f) h
 
 protected theorem apply_maxOn_lt_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) < b ↔ ∀ x ∈ xs, f x < b := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   simpa [LT.lt_opposite_iff] using List.lt_apply_minOn_iff (f := f) h
 
 protected theorem lt_apply_maxOn_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     b < f (xs.maxOn f h) ↔ ∃ x ∈ xs, b < f x := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   simpa [LT.lt_opposite_iff] using List.apply_minOn_lt_iff (f := f) h
 
 protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
@@ -386,14 +386,14 @@ protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
     haveI : xs ≠ [] := by intro h; rw [h] at hxs; simp_all [subset_nil]
     f (ys.maxOn f hys) ≤ f (xs.maxOn f this) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_apply_minOn_of_subset (f := f) hxs hys
 
 protected theorem apply_maxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     f ((xs.take i).maxOn f h) ≤ f (xs.maxOn f (List.ne_nil_of_take_ne_nil h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_take (f := f) h
 
 protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -401,7 +401,7 @@ protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearP
     f (xs.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_left_ne_nil h ys)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_left (f := f) h
 
 protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -409,7 +409,7 @@ protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinear
     f (ys.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_right_ne_nil xs h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_right (f := f) h
 
 @[simp]
@@ -417,21 +417,21 @@ protected theorem maxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β] {x
     {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
     (xs ++ ys).maxOn f (by simp [hxs]) = maxOn f (xs.maxOn f hxs) (ys.maxOn f hys) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minOn_append (f := f) hxs hys
 
 protected theorem maxOn_eq_head [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) (h' : ∀ x ∈ xs, f x ≤ f (xs.head h)) :
     xs.maxOn f h = xs.head h := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.minOn_eq_head (f := f) h (by simpa [LE.le_opposite_iff] using h')
 
 protected theorem max_map
     [LE β] [DecidableLE β] [Max β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMax β] {xs : List α}
     {f : α → β} (h : xs ≠ []) : (xs.map f).max (by simpa) = f (xs.maxOn f h) := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : Max β).oppositeMin
   simpa [List.max_eq_min] using List.min_map (f := f) h
 
 protected theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
@@ -458,7 +458,7 @@ protected theorem max_map_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderL
 protected theorem maxOn_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxOn f h = a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_replicate (f := f) h
 
 /-! # minOn? -/
@@ -579,7 +579,7 @@ protected theorem maxOn?_nil [LE β] [DecidableLE β] {f : α → β} :
 protected theorem maxOn?_cons_eq_some_maxOn
     [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).maxOn? f = some ((x :: xs).maxOn f (fun h => nomatch h)) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_cons_eq_some_minOn
 
 protected theorem maxOn?_cons
@@ -588,7 +588,7 @@ protected theorem maxOn?_cons
   have : maxOn f x = (letI : LE β := LE.opposite inferInstance; minOn f x) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn?_cons
 
 @[simp]
@@ -599,8 +599,8 @@ protected theorem maxOn?_singleton [LE β] [DecidableLE β] {x : α} {f : α →
 @[simp]
 protected theorem maxOn?_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
     {xs : List α} : xs.maxOn? id = xs.max? := by
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simpa only [List.maxOn?_eq_minOn?, List.max?_eq_min?] using List.minOn?_id (α := α)
 
 protected theorem maxOn?_eq_if
@@ -610,7 +610,7 @@ protected theorem maxOn?_eq_if
       some (xs.maxOn f h)
     else
       none :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_eq_if
 
 @[simp]
@@ -620,55 +620,55 @@ protected theorem isSome_maxOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs
 
 protected theorem maxOn_eq_get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn f h = (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_eq_get_minOn? (f := f) h
 
 protected theorem maxOn?_eq_some_maxOn [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn? f = some (xs.maxOn f h) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_eq_some_minOn (f := f) h
 
 @[simp]
 protected theorem get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) = xs.maxOn f h :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.get_minOn? (f := f) h
 
 protected theorem maxOn_eq_of_maxOn?_eq_some
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : xs.maxOn? f = some x) :
     xs.maxOn f (List.isSome_maxOn?_iff.mp (Option.isSome_of_eq_some h)) = x :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn_eq_of_minOn?_eq_some (f := f) h
 
 protected theorem isSome_maxOn?_of_mem
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     (xs.maxOn? f).isSome :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.isSome_minOn?_of_mem (f := f) h
 
 protected theorem le_apply_get_maxOn?_of_mem
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     f x ≤ f ((xs.maxOn? f).get (List.isSome_maxOn?_of_mem h)) := by
   simp only [List.maxOn?_eq_minOn?]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa [LE.le_opposite_iff] using List.apply_get_minOn?_le_of_mem (f := f) h
 
 protected theorem maxOn?_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} (h : xs.maxOn? f = some a) : a ∈ xs :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_mem (f := f) h
 
 protected theorem maxOn?_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} :
     (replicate n a).maxOn? f = if n = 0 then none else some a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_replicate
 
 @[simp]
 protected theorem maxOn?_replicate_of_pos [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : 0 < n) :
     (replicate n a).maxOn? f = some a :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   List.minOn?_replicate_of_pos (f := f) h
 
 @[simp]
@@ -678,7 +678,7 @@ protected theorem maxOn?_append [LE β] [DecidableLE β] [IsLinearPreorder β]
   have : maxOn f = (letI : LE β := LE.opposite inferInstance; minOn f) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn?_append xs ys f
 
 end List
diff --git a/src/Init/Data/Order/MinMaxOn.lean b/src/Init/Data/Order/MinMaxOn.lean
index dacbfd937b..86f49a55fe 100644
--- a/src/Init/Data/Order/MinMaxOn.lean
+++ b/src/Init/Data/Order/MinMaxOn.lean
@@ -39,8 +39,8 @@ public theorem minOn_id [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeanin
 
 public theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] {x y : α} :
     maxOn id x y = max x y := by
-  letI : LE α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : Max α).oppositeMin
   simp [maxOn, minOn_id, Max.min_oppositeMin, this]
 
 public theorem minOn_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
@@ -168,32 +168,32 @@ public theorem maxOn_eq_right_of_lt
     [LE β] [DecidableLE β] [LT β] [Total (α := β) (· ≤ ·)] [LawfulOrderLT β]
     {f : α → β} {x y : α} (h : f x < f y) :
     maxOn f x y = y :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : LT β).opposite
   minOn_eq_right_of_lt (h := by simpa [LT.lt_opposite_iff] using h) ..
 
 public theorem left_le_apply_maxOn [le : LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f x ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_left (f := f) ..
 
 public theorem right_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f y ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_right (f := f)
 
 public theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} {b : β} :
     f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   simpa only [LE.le_opposite_iff] using le_apply_minOn_iff (f := f)
 
 public theorem maxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y z : α} : maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z) :=
-  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   minOn_assoc (f := f)
 
 public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
@@ -203,8 +203,8 @@ public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
 
 public theorem max_apply [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
     {f : α → β} {x y : α} : max (f x) (f y) = f (maxOn f x y) := by
-  letI : LE β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : Max β).oppositeMin
   simpa [Max.min_oppositeMin] using min_apply (f := f)
 
 public theorem apply_maxOn [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
diff --git a/src/Init/Data/Order/Opposite.lean b/src/Init/Data/Order/Opposite.lean
index 3cfc17b51b..bb985df789 100644
--- a/src/Init/Data/Order/Opposite.lean
+++ b/src/Init/Data/Order/Opposite.lean
@@ -44,7 +44,7 @@ def min' [LE α] [DecidableLE α] (a b : α) : α :=
 
 open scoped Std.OppositeOrderInstances in
 def max' [LE α] [DecidableLE α] (a b : α) : α :=
-  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : LE α := (inferInstance : LE α).opposite
   -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
   min' a b
 ```
diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index f47a189a50..10e5888e1e 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -954,7 +954,7 @@ theorem monotone_readerTRun [PartialOrder γ]
 instance [inst : PartialOrder (m α)] : PartialOrder (StateRefT' ω σ m α) := instOrderPi
 instance [inst : CCPO (m α)] : CCPO (StateRefT' ω σ m α) := instCCPOPi
 instance [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] : MonoBind (StateRefT' ω σ m) :=
-  inferInstanceAs (MonoBind (ReaderT _ _))
+  inferInstanceAs (MonoBind (ReaderT (ST.Ref ω σ) m))
 
 @[partial_fixpoint_monotone]
 theorem monotone_stateRefT'Run [PartialOrder γ]
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index df1cd7e77f..87e65df98c 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -185,18 +185,17 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
-inference. This is just like `inferInstance` except that `α` is given
-explicitly instead of being inferred from the target type. It is especially
-useful when the target type is some `α'` which is definitionally equal to `α`,
-but the instance we are looking for is only registered for `α` (because
-typeclass search does not unfold most definitions, but definitional equality
-does.) Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
+"instance normal form": the result is a constructor application whose sub-instance fields
+are canonical instances and whose types match `α` exactly. This is useful when `α` is
+definitionally equal to some `α'` for which instances are registered, as it prevents
+leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
+for details. Example:
 ```
 #check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
 ```
 -/
-abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
+abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 
 
 
diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index 3cb60f944a..9eab38ac6d 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/src/Lean/Compiler/LCNF/CompilerM.lean
@@ -49,7 +49,7 @@ structure CompilerM.Context where
 abbrev CompilerM := ReaderT CompilerM.Context $ StateRefT CompilerM.State CoreM
 
 @[always_inline]
-instance : Monad CompilerM := let i := inferInstanceAs (Monad CompilerM); { pure := i.pure, bind := i.bind }
+instance : Monad CompilerM := let i : Monad CompilerM := inferInstance; { pure := i.pure, bind := i.bind }
 
 @[inline] def withPhase (phase : Phase) (x : CompilerM α) : CompilerM α :=
   withReader (fun ctx => { ctx with phase }) x
diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
index 1c15fa72cb..1f38cd10e8 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
@@ -78,7 +78,7 @@ structure State where
 abbrev SimpM := ReaderT Context $ StateRefT State DiscrM
 
 @[always_inline]
-instance : Monad SimpM := let i := inferInstanceAs (Monad SimpM); { pure := i.pure, bind := i.bind }
+instance : Monad SimpM := let i : Monad SimpM := inferInstance; { pure := i.pure, bind := i.bind }
 
 instance : MonadFVarSubst SimpM .pure false where
   getSubst := return (← get).subst
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index a41489f7a6..3a6a68b50f 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -256,7 +256,7 @@ abbrev CoreM := ReaderT Context <| StateRefT State (EIO Exception)
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
 @[always_inline]
-instance : Monad CoreM := let i := inferInstanceAs (Monad CoreM); { pure := i.pure, bind := i.bind }
+instance : Monad CoreM := let i : Monad CoreM := inferInstance; { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (CoreM α) where
   default := fun _ _ => throw default
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index e43d199f7d..c7cef17018 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -313,6 +314,26 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     return val
   | _ => panic! "resolveId? returned an unexpected expression"
 
+@[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
+  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
+  -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
+  let typeStx := stx[stx.getNumArgs - 1]!
+  let type ← withSynthesize (postpone := .yes) <| elabType typeStx
+  -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
+  discard <| isDefEq type expectedType
+  let type ← instantiateMVars type
+  -- Rebuild type with fresh synthetic mvars for instance-implicit args, so that
+  -- synthesis is not influenced by the expected type's instance choices.
+  let type ← abstractInstImplicitArgs type
+  let inst ← synthInstance type
+  let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
+    -- Normalize to instance normal form.
+    let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
+  else
+    pure inst
+  ensureHasType expectedType? inst
+
 @[builtin_term_elab clear] def elabClear : TermElab := fun stx expectedType? => do
   let some (.fvar fvarId) ← isLocalIdent? stx[1]
     | throwErrorAt stx[1] "not in scope"
@@ -383,14 +404,13 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
       let name ← mkAuxDeclName `_private
       withoutExporting do
         let e ← elabTermAndSynthesize e expectedType?
-        let compile := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
         let e ← mkAuxDefinitionFor (compile := false) name e
-        if compile then
-          -- Inline as changing visibility should not affect run time.
-          setInlineAttribute name
-          if (← read).declName?.any (isMarkedMeta (← getEnv)) then
-            modifyEnv (markMeta · name)
-          compileDecls #[name]
+        -- Inline as changing visibility should not affect run time.
+        setInlineAttribute name
+        if (← read).declName?.any (isMarkedMeta (← getEnv)) then
+          modifyEnv (markMeta · name)
+        let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
+        compileDecls (logErrors := logCompileErrors) #[name]
         return e
     else
       elabTerm e expectedType?
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index cb5128ee98..327741d088 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -71,7 +71,7 @@ whole monad stack at every use site. May eventually be covered by `deriving`.
 Remark: see comment at TermElabM
 -/
 @[always_inline]
-instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
+instance : Monad CommandElabM := let i : Monad CommandElabM := inferInstance; { pure := i.pure, bind := i.bind }
 
 /--
 Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 1f6ff45169..9e339d7302 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
+import Lean.Meta.InstanceNormalForm
 
 public section
 
@@ -187,7 +188,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
   let ConstantInfo.defnInfo info ← getConstInfo declName
     | throwError "Failed to delta derive instance, `{.ofConstName declName}` is not a definition."
   let value := info.value.beta decl.getAppArgs
-  let result : Closure.MkValueTypeClosureResult ←
+  let (result, preNormValue, instName) : Closure.MkValueTypeClosureResult × Expr × Name ←
     -- Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code
     -- the function is written as a lambda expression.
     -- Furthermore, we don't use `forallTelescope` because users want to derive instances for monads.
@@ -210,22 +211,32 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
           -- We don't reduce because of abbreviations such as `DecidableEq`
           forallTelescope classExpr fun _ classExpr => do
             let result ← mkInst classExpr declName decl value
-            Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
+            -- Save the pre-normalization value for the noncomputable check below,
+            -- since `normalizeInstance` may inline noncomputable constants.
+            let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
+            -- Compute instance name early so `normalizeInstance` can use it for aux def naming.
+            let env ← getEnv
+            let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" preNormClosure.type)
+            instName ← liftMacroM <| mkUnusedBaseName instName
+            if isPrivateName declName then
+              instName := mkPrivateName env instName
+            let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
+              withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
+                normalizeInstance result.instVal result.instType
+                  (logCompileErrors := false)  -- covered by noncomputable check below
+            else
+              pure result.instVal
+            let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)
+            return (closure, preNormClosure.value, instName)
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" result.type)
-  -- We don't have a facility to let users override derived names, so make an unused name if needed.
-  instName ← liftMacroM <| mkUnusedBaseName instName
-  -- Make the instance private if the declaration is private.
-  if isPrivateName declName then
-    instName := mkPrivateName env instName
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
   let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
   -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
   -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
   unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := result.value.foldConsts none fun n acc =>
+    let noncompRef? := preNormValue.foldConsts none fun n acc =>
       acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
     if let some noncompRef := noncompRef? then
       if let some cmdRef := cmdRef? then
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 35ddc5e7c9..3247a4a473 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -10,6 +10,7 @@ public import Lean.Compiler.NoncomputableAttr
 public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Elab.DefView
 public section
 
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 7f6afd4721..8c3f1c62b5 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -63,7 +63,7 @@ See comment at `Monad TermElabM`
 -/
 @[always_inline]
 instance : Monad TacticM :=
-  let i := inferInstanceAs (Monad TacticM);
+  let i : Monad TacticM := inferInstance;
   { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (TacticM α) where
diff --git a/src/Lean/Elab/Tactic/Decide.lean b/src/Lean/Elab/Tactic/Decide.lean
index 2ae08e3e7f..602f1409c2 100644
--- a/src/Lean/Elab/Tactic/Decide.lean
+++ b/src/Lean/Elab/Tactic/Decide.lean
@@ -155,7 +155,7 @@ where
         .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
           which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
           To avoid tactics, make use of functions such as \
-          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
+          `{.ofConstName `inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
           to alter a proposition."
       else if reason.isAppOf ``Classical.choice then
         .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
index fd507d4b7d..2a32d76f48 100644
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -74,7 +74,7 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : GrindTacticM Un
 
 @[always_inline]
 instance : Monad GrindTacticM :=
-  let i := inferInstanceAs (Monad GrindTacticM)
+  let i : Monad GrindTacticM := inferInstance
   { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (GrindTacticM α) where
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 748a57b86d..7fde3bc80a 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -371,7 +371,7 @@ whole monad stack at every use site. May eventually be covered by `deriving`.
 -/
 @[always_inline]
 instance : Monad TermElabM :=
-  let i := inferInstanceAs (Monad TermElabM)
+  let i : Monad TermElabM := inferInstance
   { pure := i.pure, bind := i.bind }
 
 open Meta
diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index 2f491cda05..6e71d999f9 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -27,6 +27,7 @@ public import Lean.Meta.Match
 public import Lean.Meta.ReduceEval
 public import Lean.Meta.Closure
 public import Lean.Meta.AbstractNestedProofs
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Meta.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index 9ad124f04d..3b27b6f36b 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -87,8 +87,13 @@ partial def visit (e : Expr) : M Expr := do
         lctx := lctx.modifyLocalDecl xFVarId fun _ => localDecl
       withLCtx lctx localInstances k
     checkCache { val := e : ExprStructEq } fun _ => do
-      if (← isNonTrivialProof e) then
-        /- Ensure proofs nested in type are also abstracted -/
+      if (← isNonTrivialProof e) && !e.hasSorry then
+        /- Ensure proofs nested in type are also abstracted.
+           We skip abstraction for proofs containing `sorry` to avoid generating extra
+           "declaration uses sorry" warnings for auxiliary theorems: one per abstracted proof
+           instead of a single warning for the main declaration. Additionally, the `zetaDelta`
+           expansion in `mkAuxTheorem` can inline let-bound sorry values, causing warnings
+           even for proofs that only transitively reference sorry-containing definitions. -/
         abstractProof e (← read).cache visit
       else match e with
         | .lam ..
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index f7def11880..79b5ac6704 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -565,7 +565,7 @@ abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
 @[always_inline]
-instance : Monad MetaM := let i := inferInstanceAs (Monad MetaM); { pure := i.pure, bind := i.bind }
+instance : Monad MetaM := let i : Monad MetaM := inferInstance; { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (MetaM α) where
   default := fun _ _ => default
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 3f630e634e..d5c6d4bf86 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -431,7 +431,8 @@ end Closure
   A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
-def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
+def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false)
+    (compile : Bool := true) (logCompileErrors : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
@@ -439,14 +440,16 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool
     result.type result.value  hints)
   addDecl decl
   if compile then
-    compileDecl decl
+    compileDecl decl (logErrors := logCompileErrors)
   return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
-def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false) (compile := true) : MetaM Expr := do
+def mkAuxDefinitionFor (name : Name) (value : Expr) (zetaDelta : Bool := false)
+    (compile := true) (logCompileErrors : Bool := true) : MetaM Expr := do
   let type ← inferType value
   let type := type.headBeta
   mkAuxDefinition name type value (zetaDelta := zetaDelta) (compile := compile)
+    (logCompileErrors := logCompileErrors)
 
 /--
   Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.
diff --git a/src/Lean/Meta/InstanceNormalForm.lean b/src/Lean/Meta/InstanceNormalForm.lean
new file mode 100644
index 0000000000..20fefdd6d9
--- /dev/null
+++ b/src/Lean/Meta/InstanceNormalForm.lean
@@ -0,0 +1,190 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Authors: Eric Wieser, Kyle Miller, Jovan Gerbscheid, Kim Morrison, Sebastian Ullrich
+-/
+module
+
+prelude
+public import Lean.Meta.Closure
+public import Lean.Meta.SynthInstance
+public import Lean.Meta.CtorRecognizer
+
+public section
+
+/-!
+# Instance Normal Form
+
+Both `inferInstanceAs` and the default `deriving` handler normalize instance bodies to
+"instance normal form". This ensures that when deriving or inferring an instance for a
+semireducible type definition, the definition's RHS is not leaked when reduced at lower
+than semireducible transparency.
+
+## Algorithm
+
+Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
+`normalizeInstance` constructs a result instance as follows, executing all steps at
+`instances` transparency:
+
+1. If `I'` is not a class, return `i` unchanged.
+2. If `I'` is a proposition, wrap `i` in an auxiliary theorem of type `I'` and return it
+   (controlled by `backward.inferInstanceAs.wrap.instances`).
+3. Reduce `i` to whnf.
+4. If `i` is not a constructor application: if the type of `i` is already defeq to `I'`,
+   return `i`; otherwise wrap it in an auxiliary definition of type `I'` and return it
+   (controlled by `backward.inferInstanceAs.wrap.instances`).
+5. Otherwise, for `i = ctor a₁ ... aₙ` with `ctor : C ?p₁ ... ?pₙ`:
+   - Unify `C ?p₁ ... ?pₙ` with `I'`.
+   - Return a new application `ctor a₁' ... aₙ' : I'` where each `aᵢ'` is constructed as:
+     - If the field type is a proposition: assign directly if types are defeq, otherwise
+       wrap in an auxiliary theorem.
+     - If the field type is a class: first try to reuse an existing synthesized instance
+       for the target type (controlled by `backward.inferInstanceAs.wrap.reuseSubInstances`);
+       if that fails, recurse with source instance `aᵢ` and expected type `?pᵢ`.
+     - Otherwise (data field): assign directly if types are defeq, otherwise wrap in an
+       auxiliary definition to fix the type (controlled by `backward.inferInstanceAs.wrap.data`).
+
+## Options
+
+- `backward.inferInstanceAs.wrap`: master switch for normalization in both `inferInstanceAs`
+  and the default `deriving` handler
+- `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for sub-instance
+  fields to avoid non-defeq instance diamonds
+- `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary
+  definitions
+- `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions
+-/
+
+namespace Lean.Meta
+
+register_builtin_option backward.inferInstanceAs.wrap : Bool := {
+  defValue := true
+  descr := "normalize instance bodies to constructor-based normal form in `inferInstanceAs` and the default `deriving` handler"
+}
+
+register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
+  defValue := true
+  descr := "when recursing into sub-instances, reuse existing instances for the target type instead of re-wrapping them, which can be important to avoid non-defeq instance diamonds"
+}
+
+register_builtin_option backward.inferInstanceAs.wrap.instances : Bool := {
+  defValue := true
+  descr := "wrap non-reducible instances in auxiliary definitions to fix their types"
+}
+
+register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
+  defValue := true
+  descr := "wrap data fields in auxiliary definitions to fix their types"
+}
+
+builtin_initialize registerTraceClass `Meta.instanceNormalForm
+
+/--
+Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
+Non-instance-implicit arguments are assigned from the original application's arguments.
+If the function is over-applied, extra arguments are preserved.
+-/
+def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
+  let fn := type.getAppFn
+  let args := type.getAppArgs
+  let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
+  for i in [:mvars.size] do
+    unless bis[i]!.isInstImplicit do
+      mvars[i]!.mvarId!.assign args[i]!
+  let args := mvars ++ args.drop mvars.size
+  instantiateMVars (mkAppN fn args)
+
+/--
+Normalize an instance value to "instance normal form".
+See the module docstring for the full algorithm specification.
+-/
+partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
+    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
+  withTraceNode `Meta.instanceNormalForm
+      (fun _ => return m!"type: {expectedType}") do
+  let some className ← isClass? expectedType
+    | return inst
+  trace[Meta.instanceNormalForm] "class is {className}"
+
+  if ← isProp expectedType then
+    if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
+      return (← mkAuxTheorem expectedType inst (zetaDelta := true))
+    else
+      return inst
+
+  -- Try to reduce it to a constructor.
+  let inst ← whnf inst
+  inst.withApp fun f args => do
+    let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
+      | do
+        trace[Meta.instanceNormalForm] "did not reduce to constructor application, returning/wrapping as is: {inst}"
+        if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
+          let instType ← inferType inst
+          if ← isDefEq expectedType instType then
+            return inst
+          else
+            let name ← mkAuxDeclName
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
+              (logCompileErrors := logCompileErrors)
+            setReducibilityStatus name .implicitReducible
+            enableRealizationsForConst name
+            return wrapped
+        else
+          return inst
+    let (mvars, _, cls) ← forallMetaTelescope (← inferType f)
+    if h₁ : args.size ≠ mvars.size then
+      throwError "instance normal form: incorrect number of arguments for \
+        constructor application `{f}`: {args}"
+    else
+      unless ← isDefEq expectedType cls do
+        throwError "instance normal form: `{expectedType}` does not unify with the conclusion of \
+          `{.ofConstName ci.name}`"
+      for h₂ : i in ci.numParams...args.size do
+        have : i < mvars.size := by
+          simp only [ne_eq, Decidable.not_not] at h₁
+          rw [← h₁]
+          get_elem_tactic
+        let mvarId := mvars[i].mvarId!
+        let mvarDecl ← mvarId.getDecl
+        let argExpectedType ← instantiateMVars mvarDecl.type
+        let arg := args[i]
+        if ← isProp argExpectedType then
+          let argType ← inferType arg
+          if ← isDefEq argExpectedType argType then
+            mvarId.assign arg
+          else
+            trace[Meta.instanceNormalForm] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
+            mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
+        -- Recurse into instance arguments of the constructor
+        else if (← isClass? argExpectedType).isSome then
+          if backward.inferInstanceAs.wrap.reuseSubInstances.get (← getOptions) then
+            -- Reuse existing instance for the target type if any. This is especially important when recursing
+            -- as it guarantees subinstances of overlapping instances are defeq under more than just
+            -- semireducible transparency.
+            try
+              if let .some new ← trySynthInstance argExpectedType then
+                trace[Meta.instanceNormalForm] "using existing instance {new}"
+                mvarId.assign new
+                continue
+            catch _ => pure ()
+
+          mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
+            (logCompileErrors := logCompileErrors))
+        else
+          -- For data fields, assign directly or wrap in aux def to fix types.
+          if backward.inferInstanceAs.wrap.data.get (← getOptions) then
+            let argType ← inferType arg
+            if ← isDefEq argExpectedType argType then
+              mvarId.assign arg
+            else
+              let name ← mkAuxDeclName
+              mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
+              setInlineAttribute name
+              if compile then
+                compileDecls (logErrors := logCompileErrors) #[name]
+              enableRealizationsForConst name
+          else
+            mvarId.assign arg
+      return mkAppN f (← mvars.mapM instantiateMVars)
+
+end Lean.Meta
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 68e908c836..69a3a3f95e 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -774,6 +774,14 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 @[builtin_term_parser] def noImplicitLambda := leading_parser
   "no_implicit_lambda% " >> termParser maxPrec
 /--
+`inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
+"instance normal form": the result is a constructor application whose sub-instance
+fields are canonical instances and whose types match `α` exactly. See
+`Lean.Meta.InstanceNormalForm` for details.
+-/
+@[builtin_term_parser] def «inferInstanceAs» := leading_parser
+  "inferInstanceAs" >> (((" $ " <|> " <| ") >> termParser minPrec) <|> (ppSpace >> termParser argPrec))
+/--
 `value_of% x` elaborates to the value of `x`, which can be a local or global definition.
 -/
 @[builtin_term_parser] def valueOf := leading_parser
diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean
index 4e087b356b..3ad571d5fb 100644
--- a/src/Std/Time/Time/Unit/Second.lean
+++ b/src/Std/Time/Time/Unit/Second.lean
@@ -36,7 +36,7 @@ instance : ToString (Ordinal leap) where
   toString r := toString r.val
 
 instance : OfNat (Ordinal leap) n := by
-  have inst := inferInstanceAs (OfNat (Bounded.LE 0 (0 + (59 : Nat))) n)
+  have inst : OfNat (Bounded.LE 0 (0 + (59 : Nat))) n := inferInstance
   cases leap
   · exact inst
   · exact ⟨inst.ofNat.expandTop (by decide)⟩
diff --git a/src/lake/Lake/Build/Target/Fetch.lean b/src/lake/Lake/Build/Target/Fetch.lean
index 129a33d1c3..e4dc91dda5 100644
--- a/src/lake/Lake/Build/Target/Fetch.lean
+++ b/src/lake/Lake/Build/Target/Fetch.lean
@@ -139,7 +139,7 @@ public protected def Target.fetchIn
   [DataKind α] (defaultPkg : Package) (self : Target α) : FetchM (Job α)
 := do
   let ⟨_, job⟩ ← self.key.fetchInCore defaultPkg
-  have ⟨kind, ⟨h_anon, h_kind⟩⟩ := inferInstanceAs (DataKind α)
+  have ⟨kind, ⟨h_anon, h_kind⟩⟩ := (inferInstance : DataKind α)
   if h : job.kind.name = kind then
     have h := by
       have h_job := h ▸ job.kind.wf
diff --git a/tests/elab/1017.lean.out.expected b/tests/elab/1017.lean.out.expected
index 626046a697..f0ba351be8 100644
--- a/tests/elab/1017.lean.out.expected
+++ b/tests/elab/1017.lean.out.expected
@@ -1,6 +1,3 @@
 1017.lean:46:4-46:7: warning: declaration uses `sorry`
 1017.lean:46:4-46:7: warning: declaration uses `sorry`
-1017.lean:46:4-46:7: warning: declaration uses `sorry`
-1017.lean:46:4-46:7: warning: declaration uses `sorry`
-1017.lean:46:4-46:7: warning: declaration uses `sorry`
 1017.lean:46:0-53:23: warning: declaration uses `sorry`
diff --git a/tests/elab/10234.lean b/tests/elab/10234.lean
index 7b730a4a38..0a18db015e 100644
--- a/tests/elab/10234.lean
+++ b/tests/elab/10234.lean
@@ -8,6 +8,8 @@ def infSeq1 (r : α → α → Prop) : α → Prop := infSeq_functor1 r (infSeq1
 info: infSeq1.coinduct.{u_1} (pred : {α : Type u_1} → (α → α → Prop) → α → Prop)
   (hyp : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), pred r a → infSeq_functor1 r (fun {α} => pred) a) {α : Type u_1}
   (r : α → α → Prop) (a✝ : α) : pred r a✝ → infSeq1 r a✝
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check infSeq1.coinduct
@@ -23,6 +25,8 @@ def infSeq2 (r : α → α → Prop) : α → Prop := infSeq_functor2 r infSeq2
 info: infSeq2.coinduct.{u_1} (pred : {α : Sort u_1} → (α → α → Prop) → α → Prop)
   (hyp : ∀ {α : Sort u_1} (r : α → α → Prop) (a : α), pred r a → ∃ b, r a b ∧ (fun {α} => pred) r b) {α : Sort u_1}
   (r : α → α → Prop) (a✝ : α) : pred r a✝ → infSeq2 r a✝
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check infSeq2.coinduct
diff --git a/tests/elab/10234.lean.out.expected b/tests/elab/10234.lean.out.expected
index 1cf14eef9c..f4fd232f5f 100644
--- a/tests/elab/10234.lean.out.expected
+++ b/tests/elab/10234.lean.out.expected
@@ -1,2 +1,2 @@
 10234.lean:4:4-4:11: warning: declaration uses `sorry`
-10234.lean:19:4-19:11: warning: declaration uses `sorry`
+10234.lean:21:4-21:11: warning: declaration uses `sorry`
diff --git a/tests/elab/1024.lean.out.expected b/tests/elab/1024.lean.out.expected
index 9017a3019e..14f1155390 100644
--- a/tests/elab/1024.lean.out.expected
+++ b/tests/elab/1024.lean.out.expected
@@ -1,3 +1,9 @@
 1024.lean:6:6-6:9: warning: declaration uses `sorry`
 1024.lean:6:6-6:9: warning: declaration uses `sorry`
 1024.lean:6:6-6:9: warning: declaration uses `sorry`
+1024.lean:19:17-19:20: warning: declaration uses `sorry`
+1024.lean:19:17-19:20: warning: declaration uses `sorry`
+1024.lean:14:10-14:21: warning: declaration uses `sorry`
+1024.lean:27:17-27:20: warning: declaration uses `sorry`
+1024.lean:27:17-27:20: warning: declaration uses `sorry`
+1024.lean:22:10-22:27: warning: declaration uses `sorry`
diff --git a/tests/elab/1026.lean b/tests/elab/1026.lean
index 945b4a4e7b..aa8673eacb 100644
--- a/tests/elab/1026.lean
+++ b/tests/elab/1026.lean
@@ -16,7 +16,7 @@ info: foo.eq_def (n : Nat) :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_3;
+      have this := foo._proof_2;
       foo x
 -/
 #guard_msgs in
@@ -28,7 +28,7 @@ info: foo.eq_unfold :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_3;
+      have this := foo._proof_2;
       foo x
 -/
 #guard_msgs in
diff --git a/tests/elab/1026.lean.out.expected b/tests/elab/1026.lean.out.expected
index b8641fcc9f..5086a69dcf 100644
--- a/tests/elab/1026.lean.out.expected
+++ b/tests/elab/1026.lean.out.expected
@@ -1,2 +1,3 @@
 1026.lean:1:4-1:7: warning: declaration uses `sorry`
+1026.lean:1:0-7:19: warning: declaration uses `sorry`
 1026.lean:9:8-9:10: warning: declaration uses `sorry`
diff --git a/tests/elab/11719.lean b/tests/elab/11719.lean
index 04d7539d5d..536d2d5a40 100644
--- a/tests/elab/11719.lean
+++ b/tests/elab/11719.lean
@@ -11,8 +11,6 @@ def subspace := { x : space α // True }
 
 /--
 warning: declaration uses `sorry`
----
-warning: declaration uses `sorry`
 -/
 #guard_msgs in
 def foo : subspace α → subspace α :=
@@ -29,8 +27,6 @@ def subspace := { x : space // True }
 
 /--
 warning: declaration uses `sorry`
----
-warning: declaration uses `sorry`
 -/
 #guard_msgs in
 def foo : subspace → subspace :=
diff --git a/tests/elab/1237.lean.out.expected b/tests/elab/1237.lean.out.expected
index 6fa59b2184..63100c9435 100644
--- a/tests/elab/1237.lean.out.expected
+++ b/tests/elab/1237.lean.out.expected
@@ -1,5 +1,3 @@
 1237.lean:9:4-9:15: warning: declaration uses `sorry`
 1237.lean:9:4-9:15: warning: declaration uses `sorry`
 1237.lean:9:4-9:15: warning: declaration uses `sorry`
-1237.lean:9:4-9:15: warning: declaration uses `sorry`
-1237.lean:9:4-9:15: warning: declaration uses `sorry`
diff --git a/tests/elab/1361b.lean.out.expected b/tests/elab/1361b.lean.out.expected
index 52f8a2cc37..3335d00330 100644
--- a/tests/elab/1361b.lean.out.expected
+++ b/tests/elab/1361b.lean.out.expected
@@ -3,4 +3,3 @@
 1361b.lean:3:4-3:10: warning: declaration uses `sorry`
 1361b.lean:5:0-5:38: warning: declaration uses `sorry`
 1361b.lean:4:4-4:17: warning: declaration uses `sorry`
-1361b.lean:4:4-4:17: warning: declaration uses `sorry`
diff --git a/tests/elab/1986.lean b/tests/elab/1986.lean
index 0a4e1bf962..f3b1ad4128 100644
--- a/tests/elab/1986.lean
+++ b/tests/elab/1986.lean
@@ -160,10 +160,10 @@ instance lattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) :=
 { Pi.semilatticeSup, Pi.semilatticeInf with }
 
 instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) :=
-  { inferInstanceAs (Top (∀ i, α' i)) with le_top := sorry }
+  { (inferInstance : Top (∀ i, α' i)) with le_top := sorry }
 
 instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) :=
-  { inferInstanceAs (Bot (∀ i, α' i)) with bot_le := sorry }
+  { (inferInstance : Bot (∀ i, α' i)) with bot_le := sorry }
 
 instance boundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i) :=
 { Pi.orderTop, Pi.orderBot with }
diff --git a/tests/elab/1986.lean.out.expected b/tests/elab/1986.lean.out.expected
index c4bcc93343..1e2bdd5d53 100644
--- a/tests/elab/1986.lean.out.expected
+++ b/tests/elab/1986.lean.out.expected
@@ -1,13 +1,8 @@
 1986.lean:66:19-66:29: warning: @HasSup.sup does not have a doc string
 1986.lean:69:19-69:29: warning: @HasInf.inf does not have a doc string
 1986.lean:136:9-136:17: warning: declaration uses `sorry`
-1986.lean:136:9-136:17: warning: declaration uses `sorry`
-1986.lean:136:9-136:17: warning: declaration uses `sorry`
 1986.lean:142:9-142:21: warning: declaration uses `sorry`
 1986.lean:162:9-162:17: warning: declaration uses `sorry`
 1986.lean:165:9-165:17: warning: declaration uses `sorry`
 1986.lean:177:9-177:24: warning: declaration uses `sorry`
-1986.lean:177:9-177:24: warning: declaration uses `sorry`
-1986.lean:177:9-177:24: warning: declaration uses `sorry`
-1986.lean:177:9-177:24: warning: declaration uses `sorry`
 1986.lean:189:9-189:16: warning: declaration uses `sorry`
diff --git a/tests/elab/2736.lean.out.expected b/tests/elab/2736.lean.out.expected
index 88318f8fe5..933ce7a79e 100644
--- a/tests/elab/2736.lean.out.expected
+++ b/tests/elab/2736.lean.out.expected
@@ -1,5 +1,4 @@
 2736.lean:37:0-37:8: warning: declaration uses `sorry`
-2736.lean:37:0-37:8: warning: declaration uses `sorry`
 instSemiringNat.toMulOneClass
 Distrib.rightDistribClass Nat
 2736.lean:49:8-49:11: warning: declaration uses `sorry`
diff --git a/tests/elab/2899.lean.out.expected b/tests/elab/2899.lean.out.expected
index 04a0ab77ec..9b10dbfa6a 100644
--- a/tests/elab/2899.lean.out.expected
+++ b/tests/elab/2899.lean.out.expected
@@ -1,6 +1,5 @@
 2899.lean:1:4-1:15: warning: declaration uses `sorry`
 2899.lean:5:4-5:9: warning: declaration uses `sorry`
 2899.lean:5:4-5:9: warning: declaration uses `sorry`
-2899.lean:5:4-5:9: warning: declaration uses `sorry`
-2899.lean:5:4-5:9: warning: declaration uses `sorry`
+2899.lean:4:0-12:27: warning: declaration uses `sorry`
 2899.lean:4:0-12:27: warning: declaration uses `sorry`
diff --git a/tests/elab/3705.lean.out.expected b/tests/elab/3705.lean.out.expected
index 9088fe3923..c918fa425e 100644
--- a/tests/elab/3705.lean.out.expected
+++ b/tests/elab/3705.lean.out.expected
@@ -1,4 +1,3 @@
 3705.lean:17:9-17:29: warning: declaration uses `sorry`
-3705.lean:17:9-17:29: warning: declaration uses `sorry`
 3705.lean:23:0-23:7: warning: declaration uses `sorry`
 3705.lean:30:8-30:11: warning: declaration uses `sorry`
diff --git a/tests/elab/3807.lean b/tests/elab/3807.lean
index 7d02202058..edc86ed30f 100644
--- a/tests/elab/3807.lean
+++ b/tests/elab/3807.lean
@@ -1,4 +1,5 @@
 import Lean.Elab.Binders
+set_option warn.sorry false
 /-!
 
 This is a test case extracted from Mathlib exhibiting a slow-down in `IsDefEq` after
@@ -344,7 +345,7 @@ instance Pi.hasLe {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] :
     LE (∀ i, α i) where le x y := ∀ i, x i ≤ y i
 
 instance Pi.preorder {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] : Preorder (∀ i, α i) where
-  __ := inferInstanceAs (LE (∀ i, α i))
+  __ := (inferInstance : LE (∀ i, α i))
   le_refl := sorry
   le_trans := sorry
 
@@ -429,8 +430,8 @@ instance instSemilatticeInf [∀ i, SemilatticeInf (α' i)] : SemilatticeInf (
   le_inf _ _ _ ac bc i := sorry
 
 instance instLattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) where
-  __ := inferInstanceAs (SemilatticeSup (∀ i, α' i))
-  __ := inferInstanceAs (SemilatticeInf (∀ i, α' i))
+  __ := (inferInstance : SemilatticeSup (∀ i, α' i))
+  __ := (inferInstance : SemilatticeInf (∀ i, α' i))
 
 instance instDistribLattice [∀ i, DistribLattice (α' i)] : DistribLattice (∀ i, α' i) where
   le_sup_inf _ _ _ _ := sorry
diff --git a/tests/elab/3965.lean.out.expected b/tests/elab/3965.lean.out.expected
index 72ff7d8c45..3dbfce7cdf 100644
--- a/tests/elab/3965.lean.out.expected
+++ b/tests/elab/3965.lean.out.expected
@@ -12,6 +12,7 @@
 3965.lean:90:0-90:8: warning: declaration uses `sorry`
 3965.lean:112:4-112:10: warning: declaration uses `sorry`
 3965.lean:112:4-112:10: warning: declaration uses `sorry`
+3965.lean:112:4-112:10: warning: declaration uses `sorry`
 3965.lean:116:8-116:17: warning: declaration uses `sorry`
 3965.lean:151:8-151:14: warning: declaration uses `sorry`
 3965.lean:170:8-170:28: warning: declaration uses `sorry`
diff --git a/tests/elab/3965_2.lean.out.expected b/tests/elab/3965_2.lean.out.expected
index d4010da443..dd1533b5c0 100644
--- a/tests/elab/3965_2.lean.out.expected
+++ b/tests/elab/3965_2.lean.out.expected
@@ -1,14 +1,9 @@
 3965_2.lean:11:8-11:19: warning: declaration uses `sorry`
 3965_2.lean:32:12-32:18: warning: declaration uses `sorry`
 3965_2.lean:34:28-34:33: warning: declaration uses `sorry`
-3965_2.lean:34:28-34:33: warning: declaration uses `sorry`
 3965_2.lean:41:18-41:27: warning: declaration uses `sorry`
 3965_2.lean:43:18-43:27: warning: declaration uses `sorry`
 3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
 3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
 3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
-3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
-3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
-3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
-3965_2.lean:83:4-83:8: warning: declaration uses `sorry`
 3965_2.lean:91:8-91:25: warning: declaration uses `sorry`
diff --git a/tests/elab/3965_3.lean.out.expected b/tests/elab/3965_3.lean.out.expected
index 381bedb779..16a0274405 100644
--- a/tests/elab/3965_3.lean.out.expected
+++ b/tests/elab/3965_3.lean.out.expected
@@ -6,25 +6,10 @@
 3965_3.lean:140:8-140:19: warning: declaration uses `sorry`
 3965_3.lean:142:8-142:18: warning: declaration uses `sorry`
 3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:150:14-150:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
-3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
 3965_3.lean:158:14-158:28: warning: declaration uses `sorry`
 3965_3.lean:219:8-219:15: warning: declaration uses `sorry`
 3965_3.lean:229:8-229:15: warning: declaration uses `sorry`
 3965_3.lean:262:9-262:17: warning: declaration uses `sorry`
 3965_3.lean:264:9-264:17: warning: declaration uses `sorry`
 3965_3.lean:280:4-280:23: warning: declaration uses `sorry`
-3965_3.lean:280:4-280:23: warning: declaration uses `sorry`
-3965_3.lean:280:4-280:23: warning: declaration uses `sorry`
-3965_3.lean:280:4-280:23: warning: declaration uses `sorry`
 3965_3.lean:289:0-289:7: warning: declaration uses `sorry`
diff --git a/tests/elab/4171.lean.out.expected b/tests/elab/4171.lean.out.expected
index 97e7900d01..67da2f8c1e 100644
--- a/tests/elab/4171.lean.out.expected
+++ b/tests/elab/4171.lean.out.expected
@@ -1,7 +1,4 @@
 4171.lean:203:9-203:25: warning: declaration uses `sorry`
-4171.lean:203:9-203:25: warning: declaration uses `sorry`
-4171.lean:203:9-203:25: warning: declaration uses `sorry`
-4171.lean:297:9-297:26: warning: declaration uses `sorry`
 4171.lean:297:9-297:26: warning: declaration uses `sorry`
 4171.lean:350:8-350:20: warning: declaration uses `sorry`
 4171.lean:354:8-354:20: warning: declaration uses `sorry`
@@ -10,19 +7,15 @@
 4171.lean:424:4-424:19: warning: declaration uses `sorry`
 4171.lean:462:4-462:12: warning: declaration uses `sorry`
 4171.lean:487:4-487:11: warning: declaration uses `sorry`
-4171.lean:487:4-487:11: warning: declaration uses `sorry`
 4171.lean:486:2-486:6: warning: declaration uses `sorry`
 4171.lean:507:0-507:8: warning: declaration uses `sorry`
-4171.lean:507:0-507:8: warning: declaration uses `sorry`
 4171.lean:515:8-515:11: warning: declaration uses `sorry`
 4171.lean:518:8-518:15: warning: declaration uses `sorry`
 4171.lean:521:8-521:17: warning: declaration uses `sorry`
 4171.lean:536:9-536:26: warning: declaration uses `sorry`
-4171.lean:536:9-536:26: warning: declaration uses `sorry`
 4171.lean:535:2-535:6: warning: declaration uses `sorry`
 4171.lean:565:9-565:20: warning: declaration uses `sorry`
 4171.lean:601:0-601:8: warning: declaration uses `sorry`
-4171.lean:601:0-601:8: warning: declaration uses `sorry`
 4171.lean:608:15-608:18: warning: declaration uses `sorry`
 4171.lean:620:4-620:27: warning: declaration uses `sorry`
 4171.lean:661:4-661:12: warning: declaration uses `sorry`
diff --git a/tests/elab/4390.lean.out.expected b/tests/elab/4390.lean.out.expected
index 6d75627f08..4b3e1374ed 100644
--- a/tests/elab/4390.lean.out.expected
+++ b/tests/elab/4390.lean.out.expected
@@ -1 +1,2 @@
 4390.lean:6:4-6:13: warning: declaration uses `sorry`
+4390.lean:6:0-11:19: warning: declaration uses `sorry`
diff --git a/tests/elab/4595_slowdown.lean.out.expected b/tests/elab/4595_slowdown.lean.out.expected
index d6a15ba365..b52c7fef95 100644
--- a/tests/elab/4595_slowdown.lean.out.expected
+++ b/tests/elab/4595_slowdown.lean.out.expected
@@ -1,18 +1,9 @@
 4595_slowdown.lean:104:14-104:25: warning: declaration uses `sorry`
 4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry`
-4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry`
-4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry`
 4595_slowdown.lean:154:8-154:16: warning: declaration uses `sorry`
 4595_slowdown.lean:181:8-181:14: warning: declaration uses `sorry`
 4595_slowdown.lean:183:8-183:14: warning: declaration uses `sorry`
 4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
 4595_slowdown.lean:194:8-194:19: warning: declaration uses `sorry`
 4595_slowdown.lean:197:8-197:15: warning: declaration uses `sorry`
 4595_slowdown.lean:207:4-207:13: warning: declaration uses `sorry`
diff --git a/tests/elab/6123_cat_adjunction.lean.out.expected b/tests/elab/6123_cat_adjunction.lean.out.expected
index e07e74f8a4..30ab647e31 100644
--- a/tests/elab/6123_cat_adjunction.lean.out.expected
+++ b/tests/elab/6123_cat_adjunction.lean.out.expected
@@ -9,7 +9,4 @@
 6123_cat_adjunction.lean:443:4-443:41: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:448:4-448:35: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
-6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
-6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
-6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
diff --git a/tests/elab/6123_mod_cast.lean.out.expected b/tests/elab/6123_mod_cast.lean.out.expected
index 766ddefb12..6fe2a7323a 100644
--- a/tests/elab/6123_mod_cast.lean.out.expected
+++ b/tests/elab/6123_mod_cast.lean.out.expected
@@ -1,4 +1,2 @@
 6123_mod_cast.lean:64:8-64:32: warning: declaration uses `sorry`
 6123_mod_cast.lean:166:9-166:17: warning: declaration uses `sorry`
-6123_mod_cast.lean:166:9-166:17: warning: declaration uses `sorry`
-6123_mod_cast.lean:166:9-166:17: warning: declaration uses `sorry`
diff --git a/tests/elab/988.lean.out.expected b/tests/elab/988.lean.out.expected
index b851b05fd9..82f0d73fa7 100644
--- a/tests/elab/988.lean.out.expected
+++ b/tests/elab/988.lean.out.expected
@@ -1 +1,2 @@
 988.lean:1:0-1:8: warning: declaration uses `sorry`
+988.lean:6:8-6:20: warning: declaration uses `sorry`
diff --git a/tests/elab/Reformat.lean.input b/tests/elab/Reformat.lean.input
index 624ba69d4d..b2438f2bd4 100644
--- a/tests/elab/Reformat.lean.input
+++ b/tests/elab/Reformat.lean.input
@@ -35,7 +35,7 @@ abbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
   fun x => a
 
 @[reducible] def inferInstance {α : Type u} [i : α] : α := i
-@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i
+@[reducible] def «inferInstanceAs» (α : Type u) [i : α] : α := i
 
 set_option bootstrap.inductiveCheckResultingUniverse false in
 inductive PUnit : Sort u
diff --git a/tests/elab/Reformat.lean.out.expected b/tests/elab/Reformat.lean.out.expected
index 2f5a1d8483..19f460d409 100644
--- a/tests/elab/Reformat.lean.out.expected
+++ b/tests/elab/Reformat.lean.out.expected
@@ -45,7 +45,7 @@ def inferInstance {α : Type u} [i : α] : α :=
   i
 
 @[reducible]
-def inferInstanceAs (α : Type u) [i : α] : α :=
+def «inferInstanceAs» (α : Type u) [i : α] : α :=
   i
 
 set_option bootstrap.inductiveCheckResultingUniverse false in
diff --git a/tests/elab/Reparen.lean.out.expected b/tests/elab/Reparen.lean.out.expected
index d844206b02..c2a7c1934d 100644
--- a/tests/elab/Reparen.lean.out.expected
+++ b/tests/elab/Reparen.lean.out.expected
@@ -185,18 +185,17 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
-inference. This is just like `inferInstance` except that `α` is given
-explicitly instead of being inferred from the target type. It is especially
-useful when the target type is some `α'` which is definitionally equal to `α`,
-but the instance we are looking for is only registered for `α` (because
-typeclass search does not unfold most definitions, but definitional equality
-does.) Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
+"instance normal form": the result is a constructor application whose sub-instance fields
+are canonical instances and whose types match `α` exactly. This is useful when `α` is
+definitionally equal to some `α'` for which instances are registered, as it prevents
+leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
+for details. Example:
 ```
 #check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
 ```
 -/
-abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
+abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 
 
 
diff --git a/tests/elab/bhaviksSampler.lean.out.expected b/tests/elab/bhaviksSampler.lean.out.expected
index b79e2ff959..5e78511dcc 100644
--- a/tests/elab/bhaviksSampler.lean.out.expected
+++ b/tests/elab/bhaviksSampler.lean.out.expected
@@ -1,7 +1,6 @@
 bhaviksSampler.lean:98:4-98:11: warning: declaration uses `sorry`
-bhaviksSampler.lean:98:4-98:11: warning: declaration uses `sorry`
-bhaviksSampler.lean:117:4-117:8: warning: declaration uses `sorry`
 bhaviksSampler.lean:117:4-117:8: warning: declaration uses `sorry`
 bhaviksSampler.lean:126:8-126:18: warning: declaration uses `sorry`
 bhaviksSampler.lean:129:8-129:25: warning: declaration uses `sorry`
+bhaviksSampler.lean:156:17-156:24: warning: declaration uses `sorry`
 bhaviksSampler.lean:152:8-152:23: warning: declaration uses `sorry`
diff --git a/tests/elab/binop_binrel_perf_issue.lean.out.expected b/tests/elab/binop_binrel_perf_issue.lean.out.expected
index a062ea13dc..7f7cefc9ed 100644
--- a/tests/elab/binop_binrel_perf_issue.lean.out.expected
+++ b/tests/elab/binop_binrel_perf_issue.lean.out.expected
@@ -1,13 +1,10 @@
 binop_binrel_perf_issue.lean:316:14-316:26: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:316:14-316:26: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:322:14-322:26: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:339:14-339:26: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:345:14-345:26: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:345:14-345:26: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:366:14-366:22: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:385:9-385:25: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:388:9-388:25: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:388:9-388:25: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:404:9-404:21: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:420:27-420:30: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:429:27-429:30: warning: declaration uses `sorry`
@@ -15,14 +12,12 @@ binop_binrel_perf_issue.lean:483:9-483:12: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:486:9-486:13: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:493:9-493:14: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:501:26-501:39: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:501:26-501:39: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:568:9-568:15: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:579:4-579:8: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:589:9-589:37: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:593:9-593:21: warning: declaration uses `sorry`
+binop_binrel_perf_issue.lean:593:9-593:21: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry`
@@ -31,7 +26,6 @@ binop_binrel_perf_issue.lean:610:9-610:15: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:613:9-613:37: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry`
-binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:668:4-668:12: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:839:9-839:17: warning: declaration uses `sorry`
 binop_binrel_perf_issue.lean:853:0-853:8: warning: declaration uses `sorry`
diff --git a/tests/elab/bintreeGoal.lean.out.expected b/tests/elab/bintreeGoal.lean.out.expected
index 4eb58c9980..b2a46023b5 100644
--- a/tests/elab/bintreeGoal.lean.out.expected
+++ b/tests/elab/bintreeGoal.lean.out.expected
@@ -1,2 +1,3 @@
 bintreeGoal.lean:53:4-53:18: warning: declaration uses `sorry`
+bintreeGoal.lean:56:17-56:21: warning: declaration uses `sorry`
 bintreeGoal.lean:60:8-60:27: warning: declaration uses `sorry`
diff --git a/tests/elab/congrSimpMathlibIssue.lean b/tests/elab/congrSimpMathlibIssue.lean
index 62524870bf..a96a4162d3 100644
--- a/tests/elab/congrSimpMathlibIssue.lean
+++ b/tests/elab/congrSimpMathlibIssue.lean
@@ -736,7 +736,7 @@ induced by `equivalence_not_adj`. -/
 def setoid : Setoid V := ⟨_, h.equivalence_not_adj⟩
 
 instance : DecidableRel h.setoid.r :=
-  inferInstanceAs <| DecidableRel (¬G.Adj · ·)
+  inferInstanceAs (DecidableRel (¬G.Adj · ·))
 
 /-- The finpartition derived from `h.setoid`. -/
 def finpartition [DecidableEq V] : Finpartition (univ : Finset V) := Finpartition.ofSetoid h.setoid
diff --git a/tests/elab/decideTactic.lean b/tests/elab/decideTactic.lean
index 3f526c93a1..c74fd8f180 100644
--- a/tests/elab/decideTactic.lean
+++ b/tests/elab/decideTactic.lean
@@ -69,7 +69,7 @@ did not reduce to `isTrue` or `isFalse`.
 After unfolding the instances `baz` and `instDecidableNice`, reduction got stuck at the `Decidable` instance
   ⋯ ▸ inferInstance
 
-Hint: Reduction got stuck on `▸` (Eq.rec), which suggests that one of the `Decidable` instances is defined using tactics such as `rw` or `simp`. To avoid tactics, make use of functions such as `inferInstanceAs` or `decidable_of_decidable_of_iff` to alter a proposition.
+Hint: Reduction got stuck on `▸` (Eq.rec), which suggests that one of the `Decidable` instances is defined using tactics such as `rw` or `simp`. To avoid tactics, make use of functions such as `«inferInstanceAs»` or `decidable_of_decidable_of_iff` to alter a proposition.
 -/
 #guard_msgs in
 example : Nice 102 := by decide
@@ -89,7 +89,7 @@ did not reduce to `isTrue` or `isFalse`.
 After unfolding the instances `baz`, `instDecidableNice`, and `instDecidableNot`, reduction got stuck at the `Decidable` instance
   ⋯ ▸ inferInstance
 
-Hint: Reduction got stuck on `▸` (Eq.rec), which suggests that one of the `Decidable` instances is defined using tactics such as `rw` or `simp`. To avoid tactics, make use of functions such as `inferInstanceAs` or `decidable_of_decidable_of_iff` to alter a proposition.
+Hint: Reduction got stuck on `▸` (Eq.rec), which suggests that one of the `Decidable` instances is defined using tactics such as `rw` or `simp`. To avoid tactics, make use of functions such as `«inferInstanceAs»` or `decidable_of_decidable_of_iff` to alter a proposition.
 -/
 #guard_msgs in
 example : ¬ Nice 102 := by decide
diff --git a/tests/elab/derivingDelta.lean b/tests/elab/derivingDelta.lean
index 9d7058f3b7..84daadbfc3 100644
--- a/tests/elab/derivingDelta.lean
+++ b/tests/elab/derivingDelta.lean
@@ -1,9 +1,13 @@
+module
+
 /-!
 # Tests for delta deriving of instances for definitions
 
 In this file we test both `deriving` clauses on definitions and `deriving instance` commands.
 -/
 
+@[expose] public section
+
 /-!
 Simple definition, body has instance immediately.
 -/
@@ -62,18 +66,23 @@ def MyNat := Nat
 deriving OfNat
 
 /--
-info: @[implicit_reducible] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
-fun _x_1 => instOfNatNat _x_1
+info: @[implicit_reducible, expose] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
+fun _x_1 => { ofNat := instOfNatMyNat._aux_1 _x_1 }
 -/
 #guard_msgs in #print instOfNatMyNat
-
+/--
+info: @[expose] def instOfNatMyNat._aux_1 : Nat → MyNat :=
+fun _x_1 => _x_1
+-/
+#guard_msgs in
+#print instOfNatMyNat._aux_1
 /-!
 Explicit parameterization
 -/
 deriving instance (n : Nat) → OfNat _ n for MyNat
 /--
-info: @[implicit_reducible] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
-fun n => instOfNatNat n
+info: @[implicit_reducible, expose] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
+fun n => { ofNat := instOfNatMyNat_1._aux_1 n }
 -/
 #guard_msgs in #print instOfNatMyNat_1
 
@@ -85,8 +94,8 @@ variable (m : Nat)
 deriving instance OfNat _ m for MyNat
 end
 /--
-info: @[implicit_reducible] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
-fun m => instOfNatNat m
+info: @[implicit_reducible, expose] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
+fun m => { ofNat := instOfNatMyNat_2._aux_1 m }
 -/
 #guard_msgs in #print instOfNatMyNat_2
 
@@ -132,8 +141,8 @@ def MyFin'' := Fin
 deriving C1
 
 /--
-info: @[implicit_reducible] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
-instC1NatFin
+info: @[implicit_reducible, expose] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
+@C1.mk Nat instDecidableEqNat MyFin''
 -/
 #guard_msgs in set_option pp.explicit true in #print instC1NatMyFin''
 
@@ -164,13 +173,13 @@ instance (n : Nat) : OfNat' n Int := {}
 def MyInt := Int
 deriving OfNat', OfNat
 /--
-info: @[implicit_reducible] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
-fun _x_1 => instOfNat'Int _x_1
+info: @[implicit_reducible, expose] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
+fun _x_1 => { }
 -/
 #guard_msgs in #print instOfNat'MyInt
 /--
-info: @[implicit_reducible] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
-fun _x_1 => instOfNat
+info: @[implicit_reducible, expose] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
+fun _x_1 => { ofNat := instOfNatMyInt._aux_1 _x_1 }
 -/
 #guard_msgs in #print instOfNatMyInt
 
@@ -201,8 +210,9 @@ def NewRing (R : Type _) [Semiring R] := R
 deriving Module R
 
 /--
-info: @[implicit_reducible] def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
-fun R [Semiring R] => instModule R
+info: @[implicit_reducible, expose] def instModuleNewRing.{u_1} : (R : Type u_1) →
+  [inst : Semiring R] → Module R (NewRing R) :=
+fun R [Semiring R] => { }
 -/
 #guard_msgs in #print instModuleNewRing
 
@@ -221,8 +231,9 @@ def NewRing' (R : Type _) := R
 deriving instance Module R for NewRing' R
 
 /--
-info: @[implicit_reducible] def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
-fun R [Semiring R] => instModule R
+info: @[implicit_reducible, expose] def instModuleNewRing'.{u_1} : (R : Type u_1) →
+  [inst : Semiring R] → Module R (NewRing' R) :=
+fun R [Semiring R] => { }
 -/
 #guard_msgs in #print instModuleNewRing'
 end
@@ -236,8 +247,8 @@ instance : C2 Type Prop := {}
 def Prop' := Prop
 deriving C2
 /--
-info: @[implicit_reducible] def instC2TypeProp' : C2 Type Prop' :=
-instC2TypeProp
+info: @[implicit_reducible, expose] def instC2TypeProp' : C2 Type Prop' :=
+{ }
 -/
 #guard_msgs in #print instC2TypeProp'
 
diff --git a/tests/elab/deriving_diamond_defeq.lean b/tests/elab/deriving_diamond_defeq.lean
index eeb5c7e0ed..858e4bc511 100644
--- a/tests/elab/deriving_diamond_defeq.lean
+++ b/tests/elab/deriving_diamond_defeq.lean
@@ -82,7 +82,7 @@ set_option pp.all true in
 
 /--
 info: @[implicit_reducible] def instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
-instHigherNat
+instMyHigherMyAlias._proof_1
 -/
 #guard_msgs in
 set_option pp.all true in
diff --git a/tests/elab/eqnsAtSimp.lean.out.expected b/tests/elab/eqnsAtSimp.lean.out.expected
index dff75461fd..5d6e08cc39 100644
--- a/tests/elab/eqnsAtSimp.lean.out.expected
+++ b/tests/elab/eqnsAtSimp.lean.out.expected
@@ -1,2 +1,2 @@
 eqnsAtSimp.lean:2:6-2:12: warning: declaration uses `sorry`
-eqnsAtSimp.lean:2:6-2:12: warning: declaration uses `sorry`
+eqnsAtSimp.lean:1:0-13:3: warning: declaration uses `sorry`
diff --git a/tests/elab/etaStruct.lean.out.expected b/tests/elab/etaStruct.lean.out.expected
index be368adfdb..95ce83b6e5 100644
--- a/tests/elab/etaStruct.lean.out.expected
+++ b/tests/elab/etaStruct.lean.out.expected
@@ -1,3 +1 @@
 etaStruct.lean:49:4-49:19: warning: declaration uses `sorry`
-etaStruct.lean:49:4-49:19: warning: declaration uses `sorry`
-etaStruct.lean:49:4-49:19: warning: declaration uses `sorry`
diff --git a/tests/elab/grind_11545.lean.out.expected b/tests/elab/grind_11545.lean.out.expected
index 526a11acea..7cda39551a 100644
--- a/tests/elab/grind_11545.lean.out.expected
+++ b/tests/elab/grind_11545.lean.out.expected
@@ -2,7 +2,6 @@ op_comp: [@Quiver.Hom.op #7 _ #4 #2 (@CategoryStruct.comp _ #6 #4 #3 #2 #1 #0)]
 op_comp: [@CategoryStruct.comp (Opposite #7) _ (@op _ #2) (@op _ #3) (@op _ #4) (@Quiver.Hom.op _ _ #3 #2 #0) (@Quiver.Hom.op _ _ #4 #3 #1)]
 grind_11545.lean:132:4-132:14: warning: declaration uses `sorry`
 grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`
-grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`
 grind_11545.lean:151:4-151:21: warning: declaration uses `sorry`
 grind_11545.lean:154:4-154:21: warning: declaration uses `sorry`
 grind_11545.lean:170:8-170:22: warning: declaration uses `sorry`
diff --git a/tests/elab/grind_canon_bug.lean.out.expected b/tests/elab/grind_canon_bug.lean.out.expected
index 61c4469219..c14ee71385 100644
--- a/tests/elab/grind_canon_bug.lean.out.expected
+++ b/tests/elab/grind_canon_bug.lean.out.expected
@@ -1,3 +1,2 @@
 grind_canon_bug.lean:13:4-13:9: warning: declaration uses `sorry`
-grind_canon_bug.lean:13:4-13:9: warning: declaration uses `sorry`
 grind_canon_bug.lean:10:0-10:7: warning: declaration uses `sorry`
diff --git a/tests/elab/grind_field_panic.lean.out.expected b/tests/elab/grind_field_panic.lean.out.expected
index 34026bb8df..a584cb4cbf 100644
--- a/tests/elab/grind_field_panic.lean.out.expected
+++ b/tests/elab/grind_field_panic.lean.out.expected
@@ -1,17 +1,9 @@
 grind_field_panic.lean:104:38-104:50: warning: fastInstance does not have a doc string
 grind_field_panic.lean:126:42-126:58: warning: letImplDetailStx does not have a doc string
 grind_field_panic.lean:180:0-180:8: warning: declaration uses `sorry`
-grind_field_panic.lean:180:0-180:8: warning: declaration uses `sorry`
-grind_field_panic.lean:180:0-180:8: warning: declaration uses `sorry`
-grind_field_panic.lean:180:0-180:8: warning: declaration uses `sorry`
-grind_field_panic.lean:180:0-180:8: warning: declaration uses `sorry`
 grind_field_panic.lean:187:0-187:8: warning: declaration uses `sorry`
 grind_field_panic.lean:188:0-188:8: warning: declaration uses `sorry`
 grind_field_panic.lean:189:18-189:35: warning: declaration uses `sorry`
 grind_field_panic.lean:198:9-198:17: warning: declaration uses `sorry`
 grind_field_panic.lean:200:31-200:44: warning: declaration uses `sorry`
-grind_field_panic.lean:200:31-200:44: warning: declaration uses `sorry`
-grind_field_panic.lean:200:31-200:44: warning: declaration uses `sorry`
-grind_field_panic.lean:200:31-200:44: warning: declaration uses `sorry`
 grind_field_panic.lean:205:31-205:43: warning: declaration uses `sorry`
-grind_field_panic.lean:223:14-223:19: warning: declaration uses `sorry`
diff --git a/tests/elab/grind_indexmap_pre.lean.out.expected b/tests/elab/grind_indexmap_pre.lean.out.expected
index 2d7ba258db..5d88191a38 100644
--- a/tests/elab/grind_indexmap_pre.lean.out.expected
+++ b/tests/elab/grind_indexmap_pre.lean.out.expected
@@ -1,20 +1,7 @@
 grind_indexmap_pre.lean:32:4-32:21: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:32:4-32:21: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:65:0-65:8: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:70:0-70:8: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:74:14-74:20: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
-grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:102:14-102:23: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:125:8-125:18: warning: declaration uses `sorry`
 grind_indexmap_pre.lean:129:8-129:22: warning: declaration uses `sorry`
diff --git a/tests/elab/grind_semiring_norm_regression.lean.out.expected b/tests/elab/grind_semiring_norm_regression.lean.out.expected
index 90d01f4125..12dde3288b 100644
--- a/tests/elab/grind_semiring_norm_regression.lean.out.expected
+++ b/tests/elab/grind_semiring_norm_regression.lean.out.expected
@@ -1,16 +1 @@
 grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
-grind_semiring_norm_regression.lean:38:9-38:33: warning: declaration uses `sorry`
diff --git a/tests/elab/heapSort.lean.out.expected b/tests/elab/heapSort.lean.out.expected
index 058d0e534f..65a9ee744a 100644
--- a/tests/elab/heapSort.lean.out.expected
+++ b/tests/elab/heapSort.lean.out.expected
@@ -1,14 +1,11 @@
 heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
 heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
-heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
-heapSort.lean:15:4-15:15: warning: declaration uses `sorry`
+heapSort.lean:13:0-36:24: warning: declaration uses `sorry`
 heapSort.lean:13:0-36:24: warning: declaration uses `sorry`
 heapSort.lean:43:4-43:10: warning: declaration uses `sorry`
 heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
 heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
-heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
-heapSort.lean:58:4-58:13: warning: declaration uses `sorry`
+heapSort.lean:56:0-69:24: warning: declaration uses `sorry`
 heapSort.lean:56:0-69:24: warning: declaration uses `sorry`
 heapSort.lean:102:4-102:13: warning: declaration uses `sorry`
-heapSort.lean:102:4-102:13: warning: declaration uses `sorry`
-heapSort.lean:102:4-102:13: warning: declaration uses `sorry`
+heapSort.lean:193:11-193:15: warning: declaration uses `sorry`
diff --git a/tests/elab/inferInstanceAs.lean b/tests/elab/inferInstanceAs.lean
new file mode 100644
index 0000000000..3447581d6e
--- /dev/null
+++ b/tests/elab/inferInstanceAs.lean
@@ -0,0 +1,47 @@
+module
+
+class C (α : Type) where
+  c : α → α
+
+/-! Trivial data wrapper -/
+
+axiom I : Type
+instance : C I where
+  c x := x
+
+def D := I
+
+instance : C D := inferInstanceAs (C I)
+
+/--
+info: @[implicit_reducible] private def instCD : C D :=
+{ c := instCD._aux_1 }
+-/
+#guard_msgs in
+#print instCD
+/--
+info: private def instCD._aux_1 : D → D :=
+fun x => x
+-/
+#guard_msgs in
+#print instCD._aux_1
+
+/-! Irreducible instances are wrapped as is. -/
+
+axiom I2 : Type
+@[instance] opaque instCI2 : C I2 := { c := fun x => x }
+def D2 := I2
+
+instance : C D2 := inferInstanceAs (C I2)
+/--
+info: @[implicit_reducible] private def instCD2 : C D2 :=
+instCD2._aux_1
+-/
+#guard_msgs in
+#print instCD2
+/--
+info: @[implicit_reducible] private def instCD2._aux_1 : C D2 :=
+instCI2
+-/
+#guard_msgs in
+#print instCD2._aux_1
diff --git a/tests/elab/interp.lean.out.expected b/tests/elab/interp.lean.out.expected
index adcb62d295..2a7cf76545 100644
--- a/tests/elab/interp.lean.out.expected
+++ b/tests/elab/interp.lean.out.expected
@@ -1 +1,2 @@
 interp.lean:60:4-60:8: warning: declaration uses `sorry`
+interp.lean:60:0-64:21: warning: declaration uses `sorry`
diff --git a/tests/elab/interp2.lean.out.expected b/tests/elab/interp2.lean.out.expected
index e357b23c4f..ce5e690678 100644
--- a/tests/elab/interp2.lean.out.expected
+++ b/tests/elab/interp2.lean.out.expected
@@ -1 +1,2 @@
 interp2.lean:59:4-59:8: warning: declaration uses `sorry`
+interp2.lean:59:0-63:21: warning: declaration uses `sorry`
diff --git a/tests/elab/issue2628.lean.out.expected b/tests/elab/issue2628.lean.out.expected
index 365574bc3d..a9481c6fa3 100644
--- a/tests/elab/issue2628.lean.out.expected
+++ b/tests/elab/issue2628.lean.out.expected
@@ -1,15 +1,12 @@
 issue2628.lean:8:4-8:7: warning: declaration uses `sorry`
-issue2628.lean:8:4-8:7: warning: declaration uses `sorry`
-issue2628.lean:28:4-28:7: warning: declaration uses `sorry`
-issue2628.lean:28:4-28:7: warning: declaration uses `sorry`
+issue2628.lean:7:0-17:3: warning: declaration uses `sorry`
 issue2628.lean:28:4-28:7: warning: declaration uses `sorry`
+issue2628.lean:27:0-40:3: warning: declaration uses `sorry`
 issue2628.lean:48:4-48:7: warning: declaration uses `sorry`
-issue2628.lean:48:4-48:7: warning: declaration uses `sorry`
-issue2628.lean:65:4-65:7: warning: declaration uses `sorry`
-issue2628.lean:65:4-65:7: warning: declaration uses `sorry`
+issue2628.lean:47:0-56:3: warning: declaration uses `sorry`
 issue2628.lean:65:4-65:7: warning: declaration uses `sorry`
+issue2628.lean:64:0-76:3: warning: declaration uses `sorry`
 issue2628.lean:86:4-86:7: warning: declaration uses `sorry`
-issue2628.lean:86:4-86:7: warning: declaration uses `sorry`
-issue2628.lean:103:4-103:7: warning: declaration uses `sorry`
-issue2628.lean:103:4-103:7: warning: declaration uses `sorry`
+issue2628.lean:85:0-94:3: warning: declaration uses `sorry`
 issue2628.lean:103:4-103:7: warning: declaration uses `sorry`
+issue2628.lean:102:0-114:3: warning: declaration uses `sorry`
diff --git a/tests/elab/issue5767.lean b/tests/elab/issue5767.lean
index 920b197c17..d7574a5a05 100644
--- a/tests/elab/issue5767.lean
+++ b/tests/elab/issue5767.lean
@@ -31,6 +31,8 @@ info: go1.induct (ss : Int) (motive : St → Prop)
       have st1 := { m := x.m, map := x.map.insert };
       st1.map.get? ss = none → motive x)
   (st0 : St) : motive st0
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check go1.induct
@@ -58,6 +60,8 @@ info: go2.induct : ∀ (motive : St → Prop),
       have st1 := { m := x.m, map := x.map.insert };
       motive st1 → motive x) →
     ∀ (st0 : St), motive st0
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check @go2.induct
diff --git a/tests/elab/issue5767.lean.out.expected b/tests/elab/issue5767.lean.out.expected
index eec5563ef3..4cca673f83 100644
--- a/tests/elab/issue5767.lean.out.expected
+++ b/tests/elab/issue5767.lean.out.expected
@@ -1,16 +1,4 @@
 issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
-issue5767.lean:12:4-12:7: warning: declaration uses `sorry`
 issue5767.lean:11:0-21:25: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:44:4-44:7: warning: declaration uses `sorry`
-issue5767.lean:43:0-53:25: warning: declaration uses `sorry`
+issue5767.lean:46:4-46:7: warning: declaration uses `sorry`
+issue5767.lean:45:0-55:25: warning: declaration uses `sorry`
diff --git a/tests/elab/issue6281.lean b/tests/elab/issue6281.lean
index 18d1900b34..3294805e5c 100644
--- a/tests/elab/issue6281.lean
+++ b/tests/elab/issue6281.lean
@@ -16,9 +16,10 @@ info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 =
       (n' + 3 + 0) % 2 = 1 → motive n'.succ.succ.succ hn 0 hm)
   (case3 :
     ∀ (n' : Nat) (hn : (n' + 3) % 2 = 1) (m' : Nat) (hm : (n' + 3 + (m' + 1)) % 2 = 1),
-      (n' + 3 + m'.succ) % 2 = 1 →
-        motive n' (f._proof_1 n') m' (f._proof_2 n' m') → motive n'.succ.succ.succ hn m'.succ hm)
+      (n' + 3 + m'.succ) % 2 = 1 → motive n' sorry m' sorry → motive n'.succ.succ.succ hn m'.succ hm)
   (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : motive n hn m hm
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check f.induct
diff --git a/tests/elab/issue6281.lean.out.expected b/tests/elab/issue6281.lean.out.expected
index 700ab6be86..d15596f641 100644
--- a/tests/elab/issue6281.lean.out.expected
+++ b/tests/elab/issue6281.lean.out.expected
@@ -1,5 +1,3 @@
 issue6281.lean:1:4-1:5: warning: declaration uses `sorry`
 issue6281.lean:1:4-1:5: warning: declaration uses `sorry`
 issue6281.lean:1:4-1:5: warning: declaration uses `sorry`
-issue6281.lean:1:4-1:5: warning: declaration uses `sorry`
-issue6281.lean:1:4-1:5: warning: declaration uses `sorry`
diff --git a/tests/elab/issue7322.lean b/tests/elab/issue7322.lean
index 44448947c9..b98c834623 100644
--- a/tests/elab/issue7322.lean
+++ b/tests/elab/issue7322.lean
@@ -34,8 +34,6 @@ warning: declaration uses `sorry`
 warning: declaration uses `sorry`
 ---
 warning: declaration uses `sorry`
----
-warning: declaration uses `sorry`
 -/
 #guard_msgs in
 def bar (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) :
diff --git a/tests/elab/issue7826.lean.out.expected b/tests/elab/issue7826.lean.out.expected
index 3924bc1a2f..0f1b77abce 100644
--- a/tests/elab/issue7826.lean.out.expected
+++ b/tests/elab/issue7826.lean.out.expected
@@ -1,7 +1,4 @@
 issue7826.lean:3:4-3:20: warning: declaration uses `sorry`
 issue7826.lean:20:4-20:12: warning: declaration uses `sorry`
 issue7826.lean:20:4-20:12: warning: declaration uses `sorry`
-issue7826.lean:20:4-20:12: warning: declaration uses `sorry`
-issue7826.lean:20:4-20:12: warning: declaration uses `sorry`
-issue7826.lean:20:4-20:12: warning: declaration uses `sorry`
 issue7826.lean:20:0-39:35: warning: declaration uses `sorry`
diff --git a/tests/elab/issue8939wf.lean.out.expected b/tests/elab/issue8939wf.lean.out.expected
index b9e89728e7..c2ba5f1586 100644
--- a/tests/elab/issue8939wf.lean.out.expected
+++ b/tests/elab/issue8939wf.lean.out.expected
@@ -44,15 +44,10 @@ WellFounded.Nat.fix
                         Nat)
                   n, m, fuel, h with
                 | 0, m, x, x_1 => fun x => m + 1
-                | n.succ, 0, f, h => fun x =>
-                  x ⟨n, ⟨1, ⟨f - 1, ackermann_fuel''._unary._proof_1 n f⟩⟩⟩ (ackermann_fuel''._unary._proof_2 n f h)
+                | n.succ, 0, f, h => fun x => x ⟨n, ⟨1, ⟨f - 1, sorry⟩⟩⟩ (id ((fun f => sorry) f))
                 | n.succ, m.succ, f, h => fun x =>
-                  x
-                    ⟨n,
-                      ⟨x ⟨n + 1, ⟨m, ⟨f - 1, ackermann_fuel''._unary._proof_3 n m f⟩⟩⟩
-                          (ackermann_fuel''._unary._proof_4 n m f h),
-                        ⟨f - 1, ackermann_fuel''._unary._proof_6 n m f h x⟩⟩⟩
-                    (ackermann_fuel''._unary._proof_8 n m f h x))
+                  x ⟨n, ⟨x ⟨n + 1, ⟨m, ⟨f - 1, sorry⟩⟩⟩ (id ((fun f => sorry) f)), ⟨f - 1, sorry⟩⟩⟩
+                    (id ((fun f => sorry) f)))
                 a)
             a)
         a)
diff --git a/tests/elab/lazyListRotateUnfoldProof.lean b/tests/elab/lazyListRotateUnfoldProof.lean
index bcc67ee74e..f1577a440c 100644
--- a/tests/elab/lazyListRotateUnfoldProof.lean
+++ b/tests/elab/lazyListRotateUnfoldProof.lean
@@ -62,6 +62,8 @@ a✝ : ∀ (h : t.get.length + 1 = R.length), (rotate t.get R nil h).length = t.
     (rotate (LazyList.delayed t) R nil h).length = (LazyList.delayed t).length + R.length
 ---
 warning: declaration uses `sorry`
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 theorem rotate_inv' {F : LazyList τ} {R : List τ} : (h : F.length + 1 = R.length) → (rotate F R nil h).length = F.length + R.length := by
diff --git a/tests/elab/lazyListRotateUnfoldProof.lean.out.expected b/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
index c24afa2782..b93b1532d4 100644
--- a/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
+++ b/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
@@ -1,4 +1,5 @@
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
+lazyListRotateUnfoldProof.lean:29:36-29:42: warning: declaration uses `sorry`
 lazyListRotateUnfoldProof.lean:27:8-27:18: warning: declaration uses `sorry`
diff --git a/tests/elab/match_lit_regression.lean.out.expected b/tests/elab/match_lit_regression.lean.out.expected
index 0828b767d7..40f6cdf2e5 100644
--- a/tests/elab/match_lit_regression.lean.out.expected
+++ b/tests/elab/match_lit_regression.lean.out.expected
@@ -9,4 +9,3 @@ match_lit_regression.lean:1:0-4:44: warning: declaration uses `sorry`
 match_lit_regression.lean:1:0-4:44: warning: declaration uses `sorry`
 match_lit_regression.lean:1:0-4:44: warning: declaration uses `sorry`
 match_lit_regression.lean:6:4-6:11: warning: declaration uses `sorry`
-match_lit_regression.lean:6:4-6:11: warning: declaration uses `sorry`
diff --git a/tests/elab/nestedIssueMatch.lean.out.expected b/tests/elab/nestedIssueMatch.lean.out.expected
index e1066bc512..12df449402 100644
--- a/tests/elab/nestedIssueMatch.lean.out.expected
+++ b/tests/elab/nestedIssueMatch.lean.out.expected
@@ -1,5 +1,5 @@
 nestedIssueMatch.lean:1:4-1:5: warning: declaration uses `sorry`
-nestedIssueMatch.lean:1:4-1:5: warning: declaration uses `sorry`
+nestedIssueMatch.lean:1:0-8:29: warning: declaration uses `sorry`
 g.eq_1 (n : Nat) :
   g n.succ =
     match g n with
diff --git a/tests/elab/nestedWF.lean.out.expected b/tests/elab/nestedWF.lean.out.expected
index ca7efa6434..ed899aac12 100644
--- a/tests/elab/nestedWF.lean.out.expected
+++ b/tests/elab/nestedWF.lean.out.expected
@@ -1,10 +1,5 @@
 nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
-nestedWF.lean:4:4-4:5: warning: declaration uses `sorry`
+nestedWF.lean:3:0-25:3: warning: declaration uses `sorry`
 Ex1.g.eq_1 (c a b n : Nat) :
   g c n.succ a b =
     match g c n a b with
@@ -25,7 +20,7 @@ Ex1.f.eq_1 (c x : Nat) :
     | 0 => 1
     | r => f c r
 nestedWF.lean:42:4-42:5: warning: declaration uses `sorry`
-nestedWF.lean:42:4-42:5: warning: declaration uses `sorry`
+nestedWF.lean:42:0-49:29: warning: declaration uses `sorry`
 Ex2.g.eq_1 (n : Nat) :
   g n.succ =
     match g n with
diff --git a/tests/elab/order.lean b/tests/elab/order.lean
index 1feca79185..d68c45e804 100644
--- a/tests/elab/order.lean
+++ b/tests/elab/order.lean
@@ -28,7 +28,7 @@ namespace LinearOrderPackage
 
 scoped instance packageOfLE : Std.LinearOrderPackage X := .ofLE X
 
-example : instLE = (inferInstanceAs (Std.PreorderPackage X)).toLE := rfl
+example : instLE = (inferInstance : Std.PreorderPackage X).toLE := rfl
 example : Std.IsLinearOrder X := inferInstance
 example : Std.LawfulOrderLT X := inferInstance
 example : Std.LawfulOrderOrd X := inferInstance
@@ -46,7 +46,7 @@ scoped instance packageOfLE : Std.LinearPreorderPackage X := .ofLE X
 scoped instance instMin : Min X := .leftLeaningOfLE X
 scoped instance instMax : Max X := .leftLeaningOfLE X
 
-example : instLE = (inferInstanceAs (Std.LinearPreorderPackage X)).toLE := rfl
+example : instLE = (inferInstance : Std.LinearPreorderPackage X).toLE := rfl
 example : Std.IsLinearPreorder X := inferInstance
 example : Std.LawfulOrderLT X := inferInstance
 example : Std.LawfulOrderOrd X := inferInstance
diff --git a/tests/elab/order.lean.out.expected b/tests/elab/order.lean.out.expected
index bda5b910ae..9c4b8e2389 100644
--- a/tests/elab/order.lean.out.expected
+++ b/tests/elab/order.lean.out.expected
@@ -1,2 +1 @@
 order.lean:98:26-98:42: warning: declaration uses `sorry`
-order.lean:98:26-98:42: warning: declaration uses `sorry`
diff --git a/tests/elab/partial_fixpoint_aeneas2.lean b/tests/elab/partial_fixpoint_aeneas2.lean
index e128c85906..008305b1b9 100644
--- a/tests/elab/partial_fixpoint_aeneas2.lean
+++ b/tests/elab/partial_fixpoint_aeneas2.lean
@@ -54,6 +54,7 @@ namespace Primitives
   open Lean.Order
 
   instance : PartialOrder (Result α) := inferInstanceAs (PartialOrder (FlatOrder (.fail .nontermination)))
+  set_option backward.inferInstanceAs.wrap.reuseSubInstances false in
   noncomputable instance : CCPO (Result α) := inferInstanceAs (CCPO (FlatOrder (.fail .nontermination)))
   noncomputable instance : MonoBind Result where
     bind_mono_left h := by
diff --git a/tests/elab/partial_fixpoint_aeneas2.lean.out.expected b/tests/elab/partial_fixpoint_aeneas2.lean.out.expected
index 8849531860..5b893d395c 100644
--- a/tests/elab/partial_fixpoint_aeneas2.lean.out.expected
+++ b/tests/elab/partial_fixpoint_aeneas2.lean.out.expected
@@ -1,12 +1,12 @@
-partial_fixpoint_aeneas2.lean:103:6-103:15: warning: declaration uses `sorry`
 partial_fixpoint_aeneas2.lean:104:6-104:15: warning: declaration uses `sorry`
 partial_fixpoint_aeneas2.lean:105:6-105:15: warning: declaration uses `sorry`
 partial_fixpoint_aeneas2.lean:106:6-106:15: warning: declaration uses `sorry`
 partial_fixpoint_aeneas2.lean:107:6-107:15: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:124:6-124:19: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:125:6-125:23: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:108:6-108:15: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:125:6-125:19: warning: declaration uses `sorry`
 partial_fixpoint_aeneas2.lean:126:6-126:23: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:127:6-127:24: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:128:6-128:31: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:129:6-129:35: warning: declaration uses `sorry`
-partial_fixpoint_aeneas2.lean:132:6-132:31: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:127:6-127:23: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:128:6-128:24: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:129:6-129:31: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:130:6-130:35: warning: declaration uses `sorry`
+partial_fixpoint_aeneas2.lean:133:6-133:31: warning: declaration uses `sorry`
diff --git a/tests/elab/robinson.lean.out.expected b/tests/elab/robinson.lean.out.expected
index 4cc4c2e296..d228b9cf28 100644
--- a/tests/elab/robinson.lean.out.expected
+++ b/tests/elab/robinson.lean.out.expected
@@ -2,38 +2,22 @@ robinson.lean:23:8-23:17: warning: declaration uses `sorry`
 robinson.lean:28:8-28:18: warning: declaration uses `sorry`
 robinson.lean:33:4-33:12: warning: declaration uses `sorry`
 robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
-robinson.lean:33:4-33:12: warning: declaration uses `sorry`
 robinson.lean:33:0-47:30: warning: declaration uses `sorry`
+robinson.lean:33:0-47:30: warning: declaration uses `sorry`
+robinson.lean:49:11-49:15: warning: declaration uses `sorry`
+robinson.lean:49:11-49:15: warning: declaration uses `sorry`
+robinson.lean:49:11-49:15: warning: declaration uses `sorry`
+robinson.lean:49:11-49:15: warning: declaration uses `sorry`
 robinson.eq_1 (l₁ r₁ l₂ r₂ : Term) :
   robinson (l₁.Cons r₁) (l₂.Cons r₂) =
     match robinson l₁ l₂ with
-    | ⟨none, h⟩ => ⟨none, robinson._proof_1 l₁ r₁ l₂ r₂⟩
+    | ⟨none, h⟩ => ⟨none, sorry⟩
     | ⟨some f, h⟩ =>
       match robinson (act f r₁) (act f r₂) with
-      | ⟨none, h⟩ => ⟨none, robinson._proof_2 l₁ r₁ l₂ r₂⟩
-      | ⟨some g, h⟩ => ⟨some (g ∘ f), robinson._proof_3 l₁ r₁ l₂ r₂ f g⟩
-robinson.eq_2 (i : Nat) (l r : Term) : robinson (Term.Var i) (l.Cons r) = ⟨none, robinson._proof_4 i l r⟩
-robinson.eq_3 (l r : Term) (i : Nat) : robinson (l.Cons r) (Term.Var i) = ⟨none, robinson._proof_5 l r i⟩
+      | ⟨none, h⟩ => ⟨none, sorry⟩
+      | ⟨some g, h⟩ => ⟨some (g ∘ f), sorry⟩
+robinson.eq_2 (i : Nat) (l r : Term) : robinson (Term.Var i) (l.Cons r) = ⟨none, sorry⟩
+robinson.eq_3 (l r : Term) (i : Nat) : robinson (l.Cons r) (Term.Var i) = ⟨none, sorry⟩
 robinson.eq_4 (i j : Nat) :
-  robinson (Term.Var i) (Term.Var j) =
-    if i = j then ⟨some id, robinson._proof_6 i j⟩ else ⟨some fun n => if n = i then j else n, robinson._proof_7 i j⟩
+  robinson (Term.Var i) (Term.Var j) = if i = j then ⟨some id, sorry⟩ else ⟨some fun n => if n = i then j else n, sorry⟩
 robinson.lean:57:8-57:10: warning: declaration uses `sorry`
diff --git a/tests/elab/splitIssue2.lean.out.expected b/tests/elab/splitIssue2.lean.out.expected
index bf90cc5d22..78cc10d974 100644
--- a/tests/elab/splitIssue2.lean.out.expected
+++ b/tests/elab/splitIssue2.lean.out.expected
@@ -3,11 +3,6 @@ splitIssue2.lean:19:8-19:19: warning: declaration uses `sorry`
 splitIssue2.lean:39:8-39:17: warning: declaration uses `sorry`
 splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
 splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
-splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
 splitIssue2.lean:48:0-57:41: warning: declaration uses `sorry`
+splitIssue2.lean:67:21-67:25: warning: declaration uses `sorry`
+splitIssue2.lean:63:8-63:20: warning: declaration uses `sorry`
diff --git a/tests/elab/splitIssue3.lean.out.expected b/tests/elab/splitIssue3.lean.out.expected
index e98c951586..1ab1d8733e 100644
--- a/tests/elab/splitIssue3.lean.out.expected
+++ b/tests/elab/splitIssue3.lean.out.expected
@@ -1,5 +1,5 @@
 splitIssue3.lean:8:4-8:7: warning: declaration uses `sorry`
-splitIssue3.lean:8:4-8:7: warning: declaration uses `sorry`
+splitIssue3.lean:8:0-16:17: warning: declaration uses `sorry`
 @len.eq_1 : ∀ {α : Type u_1}, len [] = 0
 @len.eq_2 : ∀ {α : Type u_1} (a : α), len [a] = 1
 @len.eq_3 : ∀ {α : Type u_1} (fst snd : List α),
diff --git a/tests/elab/structWithAlgTCSynth.lean b/tests/elab/structWithAlgTCSynth.lean
index f788a8cc37..0c25e54a11 100644
--- a/tests/elab/structWithAlgTCSynth.lean
+++ b/tests/elab/structWithAlgTCSynth.lean
@@ -338,11 +338,11 @@ class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
 
 instance (priority := 100) CommSemiring.toNonUnitalCommSemiring [CommSemiring α] :
     NonUnitalCommSemiring α :=
-  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }
+  { (inferInstance : CommMonoid α), (inferInstance : CommSemiring α) with }
 
 instance (priority := 100) CommSemiring.toCommMonoidWithZero [CommSemiring α] :
     CommMonoidWithZero α :=
-  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }
+  { (inferInstance : CommMonoid α), (inferInstance : CommSemiring α) with }
 
 section HasDistribNeg
 
@@ -361,7 +361,7 @@ section MulZeroClass
 variable [MulZeroClass α] [HasDistribNeg α]
 
 instance (priority := 100) MulZeroClass.negZeroClass : NegZeroClass α :=
-  { inferInstanceAs (Zero α), inferInstanceAs (InvolutiveNeg α) with
+  { (inferInstance : Zero α), (inferInstance : InvolutiveNeg α) with
     neg_zero := sorry }
 
 end MulZeroClass
@@ -719,7 +719,7 @@ def AddMonoidAlgebra :=
   G →₀ k
 
 instance AddMonoidAlgebra.addCommMonoid : AddCommMonoid (AddMonoidAlgebra k G) :=
-  inferInstanceAs (AddCommMonoid (G →₀ k))
+  (inferInstance : AddCommMonoid (G →₀ k))
 
 end
 
diff --git a/tests/elab/structWithAlgTCSynth.lean.out.expected b/tests/elab/structWithAlgTCSynth.lean.out.expected
index 71c9433efa..ca83cc7806 100644
--- a/tests/elab/structWithAlgTCSynth.lean.out.expected
+++ b/tests/elab/structWithAlgTCSynth.lean.out.expected
@@ -1,54 +1,31 @@
 structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:292:27-292:63: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:363:27-363:52: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:387:27-387:47: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:387:27-387:47: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:392:27-392:46: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:392:27-392:46: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:471:9-471:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:476:9-476:25: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:481:9-481:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:481:9-481:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:488:9-488:18: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:488:9-488:18: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:509:9-509:17: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:600:4-600:10: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:619:9-619:12: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:624:9-624:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:633:9-633:12: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:636:9-636:12: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:639:9-639:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:642:9-642:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:642:9-642:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:666:9-666:22: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:769:9-769:26: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:776:9-776:25: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:776:9-776:25: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:796:9-796:30: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:880:9-880:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:883:9-883:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:886:9-886:20: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:886:9-886:20: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:893:9-893:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:893:9-893:21: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:899:0-899:8: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:902:9-902:15: warning: declaration uses `sorry`
@@ -56,39 +33,23 @@ structWithAlgTCSynth.lean:905:9-905:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:908:9-908:17: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:916:4-916:28: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:949:9-949:18: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1003:29-1003:70: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1005:29-1005:67: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1029:32-1029:73: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1037:29-1037:70: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1039:29-1039:70: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1047:33-1047:75: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1051:0-1051:8: warning: declaration uses `sorry`
+structWithAlgTCSynth.lean:1071:4-1071:60: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1117:12-1117:15: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1117:12-1117:15: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1120:12-1120:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1120:12-1120:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1123:12-1123:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1126:12-1126:15: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1126:12-1126:15: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1130:12-1130:16: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1136:12-1136:16: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
-structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1203:9-1203:25: warning: declaration uses `sorry`
 structWithAlgTCSynth.lean:1237:0-1237:8: warning: declaration uses `sorry`
diff --git a/tests/elab/tryHeuristicPerfIssue.lean.out.expected b/tests/elab/tryHeuristicPerfIssue.lean.out.expected
index a1d527139c..ed86e2bc38 100644
--- a/tests/elab/tryHeuristicPerfIssue.lean.out.expected
+++ b/tests/elab/tryHeuristicPerfIssue.lean.out.expected
@@ -1,18 +1,2 @@
 tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:128:23-128:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
 tryHeuristicPerfIssue.lean:129:23-129:27: warning: declaration uses `sorry`
diff --git a/tests/elab/tryHeuristicPerfIssue2.lean.out.expected b/tests/elab/tryHeuristicPerfIssue2.lean.out.expected
index 85860ffb72..53f10bdad3 100644
--- a/tests/elab/tryHeuristicPerfIssue2.lean.out.expected
+++ b/tests/elab/tryHeuristicPerfIssue2.lean.out.expected
@@ -1,18 +1,2 @@
 tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:130:23-130:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
-tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
 tryHeuristicPerfIssue2.lean:131:23-131:27: warning: declaration uses `sorry`
diff --git a/tests/elab/wfEqns1.lean.out.expected b/tests/elab/wfEqns1.lean.out.expected
index 5b169d3ea1..1182bd439d 100644
--- a/tests/elab/wfEqns1.lean.out.expected
+++ b/tests/elab/wfEqns1.lean.out.expected
@@ -1,2 +1,2 @@
 wfEqns1.lean:2:6-2:12: warning: declaration uses `sorry`
-wfEqns1.lean:2:6-2:12: warning: declaration uses `sorry`
+wfEqns1.lean:1:0-13:3: warning: declaration uses `sorry`
diff --git a/tests/elab/wf_preprocess.lean b/tests/elab/wf_preprocess.lean
index c2bf12ffff..bd94582b92 100644
--- a/tests/elab/wf_preprocess.lean
+++ b/tests/elab/wf_preprocess.lean
@@ -148,6 +148,8 @@ structure MTree (α : Type u) where
 /--
 warning: declaration uses `sorry`
 ---
+warning: declaration uses `sorry`
+---
 trace: α : Type u_1
 t : MTree α
 x✝¹ : List (MTree α)
@@ -174,6 +176,8 @@ theorem MTree.map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α
 info: MTree.map.induct.{u_1} {α : Type u_1} (motive : MTree α → Prop)
   (case1 : ∀ (x : MTree α), (∀ (x_1 : List (MTree α)), x_1 ∈ x.cs → ∀ (x : MTree α), x ∈ x_1 → motive x) → motive x)
   (t : MTree α) : motive t
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check MTree.map.induct
@@ -243,6 +247,8 @@ inductive Expression where
 /--
 warning: declaration uses `sorry`
 ---
+warning: declaration uses `sorry`
+---
 trace: L : List (String × Expression)
 x : String × Expression
 h✝ : x ∈ L
@@ -270,6 +276,8 @@ info: Ex1.t.induct (motive : Expression → Prop) (case1 : ∀ (s : String), mot
   (case2 :
     ∀ (L : List (String × Expression)), (∀ (x : String × Expression), motive x.snd) → motive (Expression.object L))
   (exp : Expression) : motive exp
+---
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 #check t.induct
@@ -284,6 +292,8 @@ inductive Expression where
 /--
 warning: declaration uses `sorry`
 ---
+warning: declaration uses `sorry`
+---
 trace: L : List (String × Expression)
 x : String × Expression
 h✝ : x ∈ L
diff --git a/tests/elab_fail/1050.lean.out.expected b/tests/elab_fail/1050.lean.out.expected
index 2f9aeec233..5aa62fb5a4 100644
--- a/tests/elab_fail/1050.lean.out.expected
+++ b/tests/elab_fail/1050.lean.out.expected
@@ -3,4 +3,4 @@
 and for `Foo.bar_aux` is
   bs : Type u
 1050.lean:24:8-24:12: warning: declaration uses `sorry`
-1050.lean:24:8-24:12: warning: declaration uses `sorry`
+1050.lean:23:2-34:5: warning: declaration uses `sorry`
diff --git a/tests/elab_fail/906.lean.out.expected b/tests/elab_fail/906.lean.out.expected
index 0fee478e02..92e0a7de2e 100644
--- a/tests/elab_fail/906.lean.out.expected
+++ b/tests/elab_fail/906.lean.out.expected
@@ -1,4 +1,5 @@
 906.lean:2:4-2:15: warning: declaration uses `sorry`
+906.lean:2:0-7:19: warning: declaration uses `sorry`
 906.lean:14:2-14:28: error: Tactic `simp` failed with a nested error:
 maximum recursion depth has been reached
 use `set_option maxRecDepth <num>` to increase limit
diff --git a/tests/elab_fail/defInst.lean.out.expected b/tests/elab_fail/defInst.lean.out.expected
index 3852a98fe0..c1b1c4d791 100644
--- a/tests/elab_fail/defInst.lean.out.expected
+++ b/tests/elab_fail/defInst.lean.out.expected
@@ -11,4 +11,5 @@ false
 true
 true
 @[implicit_reducible] def instMonadM : Monad M :=
-ReaderT.instMonad
+{ map := @instMonadM._aux_1, mapConst := @instMonadM._aux_3, pure := @instMonadM._aux_5, seq := @instMonadM._aux_7,
+  seqLeft := @instMonadM._aux_9, seqRight := @instMonadM._aux_11, bind := @instMonadM._aux_13 }