feat: unfold and rewrap instances in inferInstanceAs and deriving

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.
2026-03-22 10:35:13 +00:00 · 2026-03-22 10:35:13 +00:00 · 88b746dd48
commit 88b746dd48
parent 2a25e4f3ae
101 changed files with 536 additions and 436 deletions
--- 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
--- 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

--- 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]
--- 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
--- 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 β]
--- 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
 ```
--- 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 γ]
--- 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



--- 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
--- 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
--- 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
--- 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?
--- 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
--- 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
--- 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

--- 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
--- 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}`, \
--- 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
--- 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
--- 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
--- 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 ..
--- 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
--- 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`.
--- a/src/Lean/Meta/InstanceNormalForm.lean
+++ 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
--- 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
--- 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)⟩
--- 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
--- 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`
--- 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
--- 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`
--- 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`
--- 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
--- 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`
--- 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 :=
--- 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`
--- 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`
--- 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 }
--- 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`
--- 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`
--- 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`
--- 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`
--- 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
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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
--- 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
--- 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



--- 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`
--- 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`
--- 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`
--- 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
--- 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
--- 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'

--- 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
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- 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`
--- a/tests/elab/inferInstanceAs.lean
+++ 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
--- 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`
--- 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`
--- 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`
--- 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
--- 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`
--- 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
--- 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`
--- 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) :
--- 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`
--- 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)
--- 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
--- 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`
--- 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`
--- 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
--- 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
--- 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
--- 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`
--- 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
--- 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`
--- 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`
--- 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`
--- 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 α),
--- 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

--- 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`
--- 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`
--- 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`
--- 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`
--- 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
--- 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`
--- 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
--- a/Show more
+++ b/Show more