diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index bd12fb48fa..10a5c3d116 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
   (strongIndefiniteDescription p h).property
 
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
-  epsilon_spec_aux (nonempty_of_exists hex) p hex
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α hex.nonempty p) :=
+  epsilon_spec_aux hex.nonempty p hex
 
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
   @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 0bd6cbad7d..0e4a7fa156 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1212,10 +1212,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
 instance : Inhabited Prop where
   default := True
 
-deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
-
-theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
-  | ⟨w, _⟩ => ⟨w⟩
+deriving instance Inhabited for NonScalar, PNonScalar, True
 
 /-! # Subsingleton -/
 
@@ -1389,16 +1386,7 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
 instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
   Nonempty.elim h (fun b => ⟨Sum.inr b⟩)
 
-instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
-  match a, b with
-  | Sum.inl a, Sum.inl b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inr b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
-  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
+deriving instance DecidableEq for Sum
 
 end
 
diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 92286dcb2f..ef65744546 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
-instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
-instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
+attribute [instance] Float.decLt Float.decLe
 
 /--
 Converts a floating-point number to a string.
diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean
index 1427c2a1f8..08824d9736 100644
--- a/src/Init/Data/Float32.lean
+++ b/src/Init/Data/Float32.lean
@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
 
@@ -154,13 +154,10 @@ Compares two floating point numbers for non-strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
 
-instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
-instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
-
 /--
 Converts a floating-point number to a string.
 
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index a9862633ad..1f8dbc57e9 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -57,9 +57,6 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
-instance : Hashable ByteArray where
-  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
-
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 
diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean
index 56b30d5eff..380e9710c0 100644
--- a/src/Init/Data/Int/LemmasAux.lean
+++ b/src/Init/Data/Int/LemmasAux.lean
@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
 /-! ### min and max -/
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega
-instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
+instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
 
 @[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
   rw [← Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
   rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]
 
 @[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
-instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
+instance : Std.Associative (α := Int) max := ⟨Int.max_assoc⟩
 
 @[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
   rw [← Int.max_assoc, Int.max_self]
diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 4a17b745aa..32fef3471f 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -849,13 +849,4 @@ comparisons.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
-/--
-Constructs an order which compares elements of an `Array` in lexicographic order.
--/
-protected def arrayOrd [a : Ord α] : Ord (Array α) where
-  compare x y :=
-    let _ : LT α := a.toLT
-    let _ : BEq α := a.toBEq
-    if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
-
 end Ord
diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 45544bb839..102bac4964 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -429,8 +429,8 @@ Examples:
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
-instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
+attribute [instance] Int8.decLt Int8.decLe
+
 instance : Max Int8 := maxOfLe
 instance : Min Int8 := minOfLe
 
@@ -800,8 +800,8 @@ Examples:
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
-instance (a b : Int16) : Decidable (a ≤ b) := Int16.decLe a b
+attribute [instance] Int16.decLt Int16.decLe
+
 instance : Max Int16 := maxOfLe
 instance : Min Int16 := minOfLe
 
@@ -1187,8 +1187,8 @@ Examples:
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
-instance (a b : Int32) : Decidable (a ≤ b) := Int32.decLe a b
+attribute [instance] Int32.decLt Int32.decLe
+
 instance : Max Int32 := maxOfLe
 instance : Min Int32 := minOfLe
 
@@ -1593,8 +1593,8 @@ Examples:
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
-instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
+attribute [instance] Int64.decLt Int64.decLe
+
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
 
@@ -1986,7 +1986,7 @@ Examples:
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
-instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
+attribute [instance] ISize.decLt ISize.decLe
+
 instance : Max ISize := maxOfLe
 instance : Min ISize := minOfLe
diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index 45371af529..33c8340fdc 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/src/Init/Data/String/Lemmas.lean
@@ -32,22 +32,4 @@ protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
   have := String.lt_irrefl a
   intro h; subst h; contradiction
 
-instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
-  irrefl := Char.lt_irrefl
-
-instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
-  refl := Char.le_refl
-
-instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
-  trans := Char.le_trans
-
-instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
-  antisymm _ _ := Char.le_antisymm
-
-instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
-  asymm _ _ := Char.lt_asymm
-
-instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
-  total := Char.le_total
-
 end String
diff --git a/src/Init/Data/Sum/Basic.lean b/src/Init/Data/Sum/Basic.lean
index a66aad79a4..ca812f4134 100644
--- a/src/Init/Data/Sum/Basic.lean
+++ b/src/Init/Data/Sum/Basic.lean
@@ -44,7 +44,6 @@ universe signature in consequence. The `Prop` version is `Or`.
 
 namespace Sum
 
-deriving instance DecidableEq for Sum
 deriving instance BEq for Sum
 
 section get
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index c41c39ba40..47d66c760b 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -222,8 +222,8 @@ Examples:
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
-instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
+attribute [instance] UInt8.decLt UInt8.decLe
+
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
@@ -438,8 +438,8 @@ Examples:
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
-instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
+attribute [instance] UInt16.decLt UInt16.decLe
+
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
@@ -586,8 +586,7 @@ set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 
 instance : Div UInt32       := ⟨UInt32.div⟩
-instance : LT UInt32        := ⟨UInt32.lt⟩
-instance : LE UInt32        := ⟨UInt32.le⟩
+-- `LT` and `LE` are already defined in `Init.Prelude`
 
 /--
 Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
@@ -832,8 +831,8 @@ Examples:
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
-instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
+attribute [instance] UInt64.decLt UInt64.decLe
+
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index d469c03b16..dd81eaf1e7 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -437,5 +437,4 @@ Examples:
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-instance (a b : USize) : Decidable (a < b) := USize.decLt a b
-instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
+attribute [instance] USize.decLt USize.decLe
diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean
index b40c0da417..a893bca9c3 100644
--- a/src/Init/Data/Vector/DecidableEq.lean
+++ b/src/Init/Data/Vector/DecidableEq.lean
@@ -44,12 +44,6 @@ theorem isEqv_self [DecidableEq α] (xs : Vector α n) : Vector.isEqv xs xs (·
   rcases xs with ⟨xs, rfl⟩
   simp [Array.isEqv_self]
 
-instance [DecidableEq α] : DecidableEq (Vector α n) :=
-  fun xs ys =>
-    match h:isEqv xs ys (fun x y => x = y) with
-    | true  => isTrue (eq_of_isEqv xs ys h)
-    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
-
 theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
     (xs == ys) = decide (∀ (i : Nat) (h' : i < n), xs[i] == ys[i]) := by
   simp [BEq.beq, isEqv_eq_decide]
diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean
index 8e5f873a61..8e469defac 100644
--- a/src/Init/Grind/CommRing/Poly.lean
+++ b/src/Init/Grind/CommRing/Poly.lean
@@ -189,7 +189,7 @@ def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Mon) (p : Poly)
-  deriving BEq, Inhabited, Hashable
+  deriving BEq, Repr, Inhabited, Hashable
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 48027853b5..84ce3b2964 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2303,8 +2303,8 @@ Examples:
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
-instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
-instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
+attribute [instance] UInt32.decLt UInt32.decLe
+
 instance : Max UInt32 := maxOfLe
 instance : Min UInt32 := minOfLe
 
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index e91531afc3..914b31443a 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -309,6 +309,10 @@ theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x :=
 
 theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩
 
+@[deprecated Exists.nonempty (since := "2025-05-19")]
+theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
+  | ⟨w, _⟩ => ⟨w⟩
+
 theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x
   | ⟨x, hn⟩, h => hn (h x)
 
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index e16ff3475c..71ecb88922 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -255,8 +255,7 @@ abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
 abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
   measure sizeOf
 
-instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
-  sizeOfWFRel
+attribute [instance low] sizeOfWFRel
 
 namespace Prod
 open WellFounded
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 3d19a2ada0..86e17ee263 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -77,12 +77,9 @@ def lt (a b : JsonNumber) : Bool :=
     else if ae > be then false
     else am < bm
 
-def ltProp : LT JsonNumber :=
+instance ltProp : LT JsonNumber :=
   ⟨fun a b => lt a b = true⟩
 
-instance : LT JsonNumber :=
-  ltProp
-
 instance (a b : JsonNumber) : Decidable (a < b) :=
   inferInstanceAs (Decidable (lt a b = true))
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
index 36bc6e6dbd..cc9db86b35 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
@@ -14,8 +14,6 @@ namespace Lean.Meta.Grind.Arith.CommRing
 export Lean.Grind.CommRing (Var Power Mon Poly)
 abbrev RingExpr := Grind.CommRing.Expr
 
-deriving instance Repr for Power, Mon, Poly
-
 mutual
 
 structure EqCnstr where
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index cab2ee4ee0..8bc2179594 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -75,7 +75,7 @@ inductive Origin where
   | stx (id : Name) (ref : Syntax)
   /-- It is local, but we don't have a local hypothesis for it. -/
   | local (id : Name)
-  deriving Inhabited, Repr, BEq
+  deriving Inhabited, Repr
 
 /-- A unique identifier corresponding to the origin. -/
 def Origin.key : Origin → Name
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index 7eec2e4d11..b32a1c92d9 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -15,7 +15,6 @@ namespace Lean.Widget
 open Elab Server
 
 deriving instance TypeName for InfoWithCtx
-deriving instance TypeName for MessageData
 deriving instance TypeName for LocalContext
 deriving instance TypeName for Elab.ContextInfo
 deriving instance TypeName for Elab.TermInfo
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index 4c6e5e715b..1ea67941de 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -252,7 +252,7 @@ namespace BVExpr
 instance : Hashable (BVExpr w) where
   hash expr := expr.hashCode _
 
-def decEq : DecidableEq (BVExpr w) := fun l r =>
+instance decEq : DecidableEq (BVExpr w) := fun l r =>
   withPtrEqDecEq l r fun _ =>
     if h : hash l ≠ hash r then
       .isFalse (ne_of_apply_ne hash h)
@@ -365,9 +365,6 @@ def decEq : DecidableEq (BVExpr w) := fun l r =>
         | .const .. | .var .. | .extract .. | .bin .. | .un .. | .append .. | .replicate ..
         | .shiftRight .. | .shiftLeft .. => .isFalse (by simp)
 
-
-instance : DecidableEq (BVExpr w) := decEq
-
 def toString : BVExpr w → String
   | .var idx => s!"var{idx}"
   | .const val => ToString.toString val
diff --git a/tests/lean/run/4928.lean b/tests/lean/run/4928.lean
index 3376aa6eec..21c725960f 100644
--- a/tests/lean/run/4928.lean
+++ b/tests/lean/run/4928.lean
@@ -46,8 +46,8 @@ end
 /--
 error: tactic 'fail' failed
 x : List Nat
-⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) instWellFoundedRelationOfSizeOf).1
-    (PSum.inr x.tail) (PSum.inl x)
+⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) sizeOfWFRel).1 (PSum.inr x.tail)
+    (PSum.inl x)
 -/
 #guard_msgs in
 set_option debug.rawDecreasingByGoal true in