From 88b746dd48d902a0fddff65eedcf1a84c0a9c621 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 22 Mar 2026 10:35:13 +0000
Subject: [PATCH] feat: unfold and rewrap instances in `inferInstanceAs` and
 `deriving`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adjusts the results of `inferInstanceAs` and the `def` `deriving` handler to conform to recently strengthened restrictions on reducibility. This change ensures that when deriving or inferring an instance for a semireducible type definition, the definition's RHS is not leaked when the instance is reduced at lower than semireducible transparency.

More specifically, given the "source type" and "target type" (the given and expected type for `inferInstanceAs`, the right-hand side and applied left-hand side of the `def` for `deriving`), we synthesize an instance for the source type and then unfold and rewrap its components (fields, nested instances) as necessary to make them compatible with the target type. The individual steps are represented by the following options, which all default to enabled and can be disabled to help with porting:
- `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs` and the default `deriving` handler
- `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type 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 (proof fields are always wrapped)

This PR is an extension and rewrite of prior work in Mathlib: https://github.com/leanprover-community/mathlib4/pull/36420

Last(?) part of fix for #9077

🤖 Prepared with Claude Code

# Breaking changes

Proofs that relied on the prior "defeq abuse" of these instance or that depended on their specific structure may need adjustments. As `inferInstanceAs A` now needs to know the source and target types exactly before it can continue, it cannot be used anymore as a synonym for `(inferInstance : A)`, use the latter instead when source and target type are identical.
---
 doc/examples/interp.lean.out.expected         |   1 +
 .../Control/Lawful/MonadAttach/Instances.lean |   4 +-
 src/Init/Data/List/MinMaxIdx.lean             |  20 +-
 src/Init/Data/List/MinMaxOn.lean              |  72 +++----
 src/Init/Data/Order/MinMaxOn.lean             |  20 +-
 src/Init/Data/Order/Opposite.lean             |   2 +-
 src/Init/Internal/Order/Basic.lean            |   2 +-
 src/Init/Prelude.lean                         |  15 +-
 src/Lean/Compiler/LCNF/CompilerM.lean         |   2 +-
 src/Lean/Compiler/LCNF/Simp/SimpM.lean        |   2 +-
 src/Lean/CoreM.lean                           |   2 +-
 src/Lean/Elab/BuiltinTerm.lean                |  34 +++-
 src/Lean/Elab/Command.lean                    |   2 +-
 src/Lean/Elab/Deriving/Basic.lean             |  29 ++-
 src/Lean/Elab/PreDefinition/Basic.lean        |   1 +
 src/Lean/Elab/Tactic/Basic.lean               |   2 +-
 src/Lean/Elab/Tactic/Decide.lean              |   2 +-
 src/Lean/Elab/Tactic/Grind/Basic.lean         |   2 +-
 src/Lean/Elab/Term/TermElabM.lean             |   2 +-
 src/Lean/Meta.lean                            |   1 +
 src/Lean/Meta/AbstractNestedProofs.lean       |   9 +-
 src/Lean/Meta/Basic.lean                      |   2 +-
 src/Lean/Meta/Closure.lean                    |   9 +-
 src/Lean/Meta/InstanceNormalForm.lean         | 190 ++++++++++++++++++
 src/Lean/Parser/Term.lean                     |   8 +
 src/Std/Time/Time/Unit/Second.lean            |   2 +-
 src/lake/Lake/Build/Target/Fetch.lean         |   2 +-
 tests/elab/1017.lean.out.expected             |   3 -
 tests/elab/10234.lean                         |   4 +
 tests/elab/10234.lean.out.expected            |   2 +-
 tests/elab/1024.lean.out.expected             |   6 +
 tests/elab/1026.lean                          |   4 +-
 tests/elab/1026.lean.out.expected             |   1 +
 tests/elab/11719.lean                         |   4 -
 tests/elab/1237.lean.out.expected             |   2 -
 tests/elab/1361b.lean.out.expected            |   1 -
 tests/elab/1986.lean                          |   4 +-
 tests/elab/1986.lean.out.expected             |   5 -
 tests/elab/2736.lean.out.expected             |   1 -
 tests/elab/2899.lean.out.expected             |   3 +-
 tests/elab/3705.lean.out.expected             |   1 -
 tests/elab/3807.lean                          |   7 +-
 tests/elab/3965.lean.out.expected             |   1 +
 tests/elab/3965_2.lean.out.expected           |   5 -
 tests/elab/3965_3.lean.out.expected           |  15 --
 tests/elab/4171.lean.out.expected             |   7 -
 tests/elab/4390.lean.out.expected             |   1 +
 tests/elab/4595_slowdown.lean.out.expected    |   9 -
 .../6123_cat_adjunction.lean.out.expected     |   3 -
 tests/elab/6123_mod_cast.lean.out.expected    |   2 -
 tests/elab/988.lean.out.expected              |   1 +
 tests/elab/Reformat.lean.input                |   2 +-
 tests/elab/Reformat.lean.out.expected         |   2 +-
 tests/elab/Reparen.lean.out.expected          |  15 +-
 tests/elab/bhaviksSampler.lean.out.expected   |   3 +-
 .../binop_binrel_perf_issue.lean.out.expected |   8 +-
 tests/elab/bintreeGoal.lean.out.expected      |   1 +
 tests/elab/congrSimpMathlibIssue.lean         |   2 +-
 tests/elab/decideTactic.lean                  |   4 +-
 tests/elab/derivingDelta.lean                 |  49 +++--
 tests/elab/deriving_diamond_defeq.lean        |   2 +-
 tests/elab/eqnsAtSimp.lean.out.expected       |   2 +-
 tests/elab/etaStruct.lean.out.expected        |   2 -
 tests/elab/grind_11545.lean.out.expected      |   1 -
 tests/elab/grind_canon_bug.lean.out.expected  |   1 -
 .../elab/grind_field_panic.lean.out.expected  |   8 -
 .../elab/grind_indexmap_pre.lean.out.expected |  13 --
 ...semiring_norm_regression.lean.out.expected |  15 --
 tests/elab/heapSort.lean.out.expected         |   9 +-
 tests/elab/inferInstanceAs.lean               |  47 +++++
 tests/elab/interp.lean.out.expected           |   1 +
 tests/elab/interp2.lean.out.expected          |   1 +
 tests/elab/issue2628.lean.out.expected        |  15 +-
 tests/elab/issue5767.lean                     |   4 +
 tests/elab/issue5767.lean.out.expected        |  16 +-
 tests/elab/issue6281.lean                     |   5 +-
 tests/elab/issue6281.lean.out.expected        |   2 -
 tests/elab/issue7322.lean                     |   2 -
 tests/elab/issue7826.lean.out.expected        |   3 -
 tests/elab/issue8939wf.lean.out.expected      |  11 +-
 tests/elab/lazyListRotateUnfoldProof.lean     |   2 +
 ...azyListRotateUnfoldProof.lean.out.expected |   1 +
 .../match_lit_regression.lean.out.expected    |   1 -
 tests/elab/nestedIssueMatch.lean.out.expected |   2 +-
 tests/elab/nestedWF.lean.out.expected         |   9 +-
 tests/elab/order.lean                         |   4 +-
 tests/elab/order.lean.out.expected            |   1 -
 tests/elab/partial_fixpoint_aeneas2.lean      |   1 +
 ...partial_fixpoint_aeneas2.lean.out.expected |  14 +-
 tests/elab/robinson.lean.out.expected         |  38 +---
 tests/elab/splitIssue2.lean.out.expected      |   9 +-
 tests/elab/splitIssue3.lean.out.expected      |   2 +-
 tests/elab/structWithAlgTCSynth.lean          |   8 +-
 .../structWithAlgTCSynth.lean.out.expected    |  53 +----
 .../tryHeuristicPerfIssue.lean.out.expected   |  16 --
 .../tryHeuristicPerfIssue2.lean.out.expected  |  16 --
 tests/elab/wfEqns1.lean.out.expected          |   2 +-
 tests/elab/wf_preprocess.lean                 |  10 +
 tests/elab_fail/1050.lean.out.expected        |   2 +-
 tests/elab_fail/906.lean.out.expected         |   1 +
 tests/elab_fail/defInst.lean.out.expected     |   3 +-
 101 files changed, 536 insertions(+), 436 deletions(-)
 create mode 100644 src/Lean/Meta/InstanceNormalForm.lean
 create mode 100644 tests/elab/inferInstanceAs.lean

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 }