diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 7ccc9bffd3ba..531fe04444e7 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -167,6 +167,8 @@ structure StructFieldInfo where
   binfo    : BinderInfo
   /-- Overrides for the parameters' binder infos when making the projections. The first component is a ref for the binder. -/
   paramInfoOverrides : ExprMap (Syntax × BinderInfo) := {}
+  /-- Number of binders for the field's type, used for elaborating the default value for the field (if present). -/
+  numBinders : Nat := 0
   /--
   Structure names that are responsible for this field being here.
   - Empty if the field is a `newField`.
@@ -947,72 +949,63 @@ However, now `α` does not know its relationship to `toMagma`.
 
 This was not robust, since in diamond inheritance `α` only remembered *one* of its parents in this indirect way.
 -/
-private def solveParentMVars (e : Expr) : StructElabM Expr := do
-  let env ← getEnv
-  Term.synthesizeSyntheticMVars (postpone := .yes)
+private def solveParentMVars (e : Expr) : StructElabM Unit := do
   let mvars ← getMVarsNoDelayed e
-  for mvar in mvars do
-    unless ← mvar.isAssigned do
-      let decl ← mvar.getDecl
-      if decl.kind.isNatural then
-        if let .const name .. := (← whnf decl.type).getAppFn then
-          if isStructure env name then
-            if let some parentInfo ← findParentFieldInfo? name then
-              if ← isDefEq (← mvar.getType) (← inferType parentInfo.fvar) then
-                discard <| MVarId.checkedAssign mvar parentInfo.fvar
-  return e
+  unless mvars.isEmpty do
+    Term.synthesizeSyntheticMVars (postpone := .yes)
+    for mvar in mvars do
+      unless ← mvar.isAssigned do
+        let decl ← mvar.getDecl
+        if decl.kind.isNatural then
+          withLCtx decl.lctx decl.localInstances do
+            if let .const name .. := (← whnf decl.type).getAppFn then
+              if let some parentInfo ← findParentFieldInfo? name then
+                if ← isDefEq (← mvar.getType) (← inferType parentInfo.fvar) then
+                  discard <| MVarId.checkedAssign mvar parentInfo.fvar
 
 private def elabParamInfoUpdatesForField (structParams : Array Expr) (binders : Array Syntax) : StructElabM (Array Syntax × ExprMap (Syntax × BinderInfo)) := do
   elabParamInfoUpdates structParams binders
     -- Filter out all fields. We assume the remaining fvars are the possible parameters.
     (fun fvarId => return (← findFieldInfoByFVarId? fvarId).isNone)
 
-private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldView) :
-    StructElabM (Option Expr × ExprMap (Syntax × BinderInfo) × Option StructFieldDefault) := do
+/--
+Elaborates the field's type, returning
+1. the type
+2. the parameter binder info overrides
+3. the number of binders for the type
+-/
+private def elabFieldType (structParams : Array Expr) (view : StructFieldView) :
+    StructElabM (Expr × ExprMap (Syntax × BinderInfo) × Nat) := do
   withoutExporting (when := view.modifiers.isPrivate) do
   let state ← get
   let binders := view.binders.getArgs
   let (binders, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams binders
-  Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders binders fun params => do
-    match view.type? with
-    | none =>
-      match view.default? with
-      | none => return (none, paramInfoOverrides, none)
-      | some (.optParam valStx) =>
-        Term.synthesizeSyntheticMVarsNoPostponing
-        let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
-        let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
-        let value ← runStructElabM (init := state) <| solveParentMVars value
-        registerFailedToInferFieldType view.name (← inferType value) view.nameId
-        registerFailedToInferDefaultValue view.name value valStx
-        let value ← mkLambdaFVars params value
-        return (none, paramInfoOverrides, StructFieldDefault.optParam value)
-      | some (.autoParam tacticStx) =>
-        throwErrorAt tacticStx "Invalid field declaration: Type must be provided when auto-param tactic is used"
-    | some typeStx =>
-      let type ← Term.elabType typeStx
-      let type ← runStructElabM (init := state) <| solveParentMVars type
-      registerFailedToInferFieldType view.name type typeStx
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
-      match view.default? with
+  Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <|
+  Term.elabBinders binders fun params => do
+    let type ←
+      match view.type? with
+      | some typeStx =>
+        let type ← Term.elabType typeStx
+        runStructElabM (init := state) <| solveParentMVars type
+        registerFailedToInferFieldType view.name type typeStx
+        pure type
       | none =>
-        let type ← mkForallFVars params type
-        return (type, paramInfoOverrides, none)
-      | some (.optParam valStx) =>
-        let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
-        let value ← runStructElabM (init := state) <| solveParentMVars value
-        registerFailedToInferDefaultValue view.name value valStx
-        Term.synthesizeSyntheticMVarsNoPostponing
-        let type  ← mkForallFVars params type
-        let value ← mkLambdaFVars params value
-        return (type, paramInfoOverrides, StructFieldDefault.optParam value)
-      | some (.autoParam tacticStx) =>
-        let name := mkAutoParamFnOfProjFn view.declName
-        discard <| Term.declareTacticSyntax tacticStx name
-        let type ← mkForallFVars params type
-        return (type, paramInfoOverrides, StructFieldDefault.autoParam <| .const name [])
+        let type ← mkFreshTypeMVar
+        registerFailedToInferFieldType view.name type view.nameId
+        pure type
+    Term.synthesizeSyntheticMVarsNoPostponing
+    let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
+    let type ← mkForallFVars params type
+    return (type, paramInfoOverrides, params.size)
+
+private def throwExistingDefaultValue (name : Name) : StructElabM α :=
+  throwError "A default value for field `{name}` has already been set for this structure"
+
+/--
+Elaborates the types of the fields.
 
+Default values are elaborated later, once the full local context has been created.
+-/
 private partial def withFields (structParams : Array Expr) (views : Array StructFieldView) (k : StructElabM α) : StructElabM α := do
   go 0
 where
@@ -1028,68 +1021,23 @@ where
         throwError "Field `{view.name}` has already been declared as a projection for parent `{.ofConstName parent.structName}`"
       match ← findFieldInfo? view.name with
       | none      =>
-        let (type?, paramInfoOverrides, default?) ← elabFieldTypeValue structParams view
-        match type?, default? with
-        | none,      none => throwError "Invalid field: Type expected"
-        | some type, _    =>
-          withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do
-            addFieldInfo { ref := view.nameId, sourceStructNames := [],
-                           name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?,
-                           binfo := view.binderInfo, paramInfoOverrides,
-                           kind := StructFieldKind.newField }
-            withExporting (isExporting := wasExporting) do
-              go (i+1)
-        | none, some (.optParam value) =>
-          let type ← inferType value
-          withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do
-            addFieldInfo { ref := view.nameId, sourceStructNames := [],
-                           name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?,
-                           binfo := view.binderInfo, paramInfoOverrides,
-                           kind := StructFieldKind.newField }
-            withExporting (isExporting := wasExporting) do
-              go (i+1)
-        | none, some (.autoParam _) =>
-          throwError "Field `{view.name}` has an auto-param but no type"
+        let (type, paramInfoOverrides, numBinders) ← elabFieldType structParams view
+        /-
+        Currently, having autoParams with binders is accepted for new fields.
+        This code is a possibility in case it should be an error.
+        (However, we could also arrange for the tactic to enter `numBinders` automatically!)
+        -- if numBinders > 0 && view.default? matches some (.autoParam ..) then
+        --   throwErrorAt view.binders "Invalid field: Unexpected binders for field `{view.name}` when setting auto-param tactic"
+        -/
+        withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do
+          addFieldInfo { ref := view.nameId, sourceStructNames := [],
+                         name := view.name, declName := view.declName,
+                         numBinders, fvar := fieldFVar, default? := none,
+                         binfo := view.binderInfo, paramInfoOverrides,
+                         kind := StructFieldKind.newField }
+          withExporting (isExporting := wasExporting) do
+            go (i+1)
       | some info =>
-        let updateDefaultValue : StructElabM α := do
-          match view.default? with
-          | none       => throwError "Field `{view.name}` has already been declared in a parent structure"
-          | some (.optParam valStx) =>
-            if let some type := view.type? then
-              throwErrorAt type "Omit the type of field `{view.name}` to set its default value"
-            else
-              if info.default?.isSome then
-                throwError "A new default value for field `{view.name}` has already been set in this structure"
-              let mut valStx := valStx
-              let (binders, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams view.binders.getArgs
-              unless paramInfoOverrides.isEmpty do
-                let params := MessageData.joinSep (paramInfoOverrides.toList.map (m!"{·.1}")) ", "
-                throwError "Cannot override structure parameter binder kinds when overriding the default value: {params}"
-              if binders.size > 0 then
-                valStx ← `(fun $binders* => $valStx:term)
-              let fvarType ← inferType info.fvar
-              let value ← Term.elabTermEnsuringType valStx fvarType
-              registerFailedToInferDefaultValue view.name value valStx
-              pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
-              if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn)
-              replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.optParam value }
-              withExporting (isExporting := wasExporting) do
-                go (i+1)
-          | some (.autoParam tacticStx) =>
-            if let some type := view.type? then
-              throwErrorAt type "Omit the type of field `{view.name}` to set its auto-param tactic"
-            else
-              if info.default?.isSome then
-                throwError "A new default value for field `{view.name}` has already been set in this structure"
-              if view.binders.getArgs.size > 0 then
-                throwErrorAt view.binders "Invalid field: Unexpected binders when setting auto-param tactic for inherited field"
-              let name := mkAutoParamFnOfProjFn view.declName
-              discard <| Term.declareTacticSyntax tacticStx name
-              replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.autoParam (.const name []) }
-              pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
-              if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn)
-              withExporting (isExporting := wasExporting) do
-                go (i+1)
         match info.kind with
         | StructFieldKind.newField      => throwError "Field `{view.name}` has already been declared"
         | StructFieldKind.subobject n
@@ -1103,10 +1051,77 @@ where
           throwError m!"Field `{view.name}` has already been declared as a projection for an indirect parent structure `{.ofConstName n}`"
             ++ .note m!"This projection was inherited from {inheritanceMsg}"
         | StructFieldKind.copiedField
-        | StructFieldKind.fromSubobject => updateDefaultValue
+        | StructFieldKind.fromSubobject =>
+          match view.default? with
+          | none => throwError "Field `{view.name}` has already been declared in a parent structure"
+          | some default =>
+            -- Prepare the default value for later elaboration by `elabStructFieldDefaults`.
+            if let some projFn := info.projFn? then Term.addTermInfo' view.ref (← mkConstWithLevelParams projFn)
+            pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
+            match default with
+            | .optParam _ =>
+              let (_, paramInfoOverrides) ← elabParamInfoUpdatesForField structParams view.binders.getArgs
+              unless paramInfoOverrides.isEmpty do
+                let params := MessageData.joinSep (paramInfoOverrides.toList.map (m!"{·.1}")) ", "
+                throwError "Cannot override structure parameter binder kinds when overriding the default value: {params}"
+              withExporting (isExporting := wasExporting) do
+                go (i+1)
+            | .autoParam _ =>
+              if let some type := view.type? then
+                throwErrorAt type "Invalid field: Uexpected type for field `{view.name}` when setting auto-param tactic for inherited field"
+              unless view.binders.getArgs.isEmpty do
+                throwErrorAt view.binders "Invalid field: Unexpected binders for field `{view.name}` when setting auto-param tactic for inherited field"
+              withExporting (isExporting := wasExporting) do
+                go (i+1)
     else
       k
 
+/--
+Elaborates the field defaults, with all the fields in scope.
+
+The behavior is slightly different between new fields and inherited fields:
+- New fields: We re-enter the binders elaborated in `elabFieldType`, then elaborate the value.
+- Inherited fields: We wrap the value in `fun` syntax to make use of the binders, then elaborate that.
+
+For inherited fields, we have already done checks that the binders and types are suitable.
+-/
+private def elabStructFieldDefaults (views : Array StructFieldView) : StructElabM Unit := do
+  for view in views do
+    if let some defaultView := view.default? then
+      withoutExporting (when := isPrivateName view.declName) do
+      withRef view.ref do
+        let some info ← findFieldInfo? view.name | unreachable!
+        if info.default?.isSome then
+          throwExistingDefaultValue info.name
+        match defaultView with
+        | .optParam valStx =>
+          let type ← inferType info.fvar
+          -- Prevent default values from being able to refer to the field itself,
+          -- since such recursive default values cannot be applied.
+          let fieldDeps ← collectForwardDeps #[info.fvar] (preserveOrder := false)
+          let value ← withErasedFVars (fieldDeps.map (·.fvarId!)) do
+            if info.kind.isFromSubobject then
+              -- Inherited field. Use `fun` to elaborate binders.
+              let mut valStx := valStx
+              if let some fieldType := view.type? then
+                valStx ← `(($valStx:term : $fieldType:term))
+              let binders := view.binders.getArgs
+              if binders.size > 0 then
+                valStx ← `(fun $binders* => $valStx:term)
+              Term.elabTermEnsuringType valStx type
+            else
+              -- New field. Use the pre-elaborated binders.
+              forallBoundedTelescope type info.numBinders fun xs type => do
+                let value ← Term.elabTermEnsuringType valStx type
+                mkLambdaFVars xs value
+          solveParentMVars value
+          registerFailedToInferDefaultValue view.name value valStx
+          replaceFieldInfo { info with default? := StructFieldDefault.optParam value }
+        | .autoParam tacticStx =>
+          let name := mkAutoParamFnOfProjFn view.declName
+          discard <| Term.declareTacticSyntax tacticStx name
+          replaceFieldInfo { info with default? := StructFieldDefault.autoParam (.const name []) }
+
 private def collectUsedFVars (lctx : LocalContext) (localInsts : LocalInstances) (fieldInfos : Array StructFieldInfo) :
     StateRefT CollectFVars.State MetaM Unit := do
   withLCtx lctx localInsts do
@@ -1511,6 +1526,7 @@ def elabStructureCommand : InductiveElabDescr where
         withParents view rs r.indFVar do
         withFields params view.fields do
         withRef view.ref do
+          elabStructFieldDefaults view.fields
           Term.synthesizeSyntheticMVarsNoPostponing
           resolveFieldDefaults view.declName
           let state ← get
diff --git a/tests/elab/struct3.lean b/tests/elab/struct3.lean
index c547a806d3b1..864fce91a607 100644
--- a/tests/elab/struct3.lean
+++ b/tests/elab/struct3.lean
@@ -20,3 +20,16 @@ class Monad4 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m,
   seq f x      := Bind2.bind f fun y => Functor.map y (x ())
   seqLeft x y  := Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
   seqRight x y := Bind2.bind x fun _ => y ()
+
+/-!
+Can provide type signatures when setting defaults of inherited fields.
+-/
+class Monad5 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
+  map {α β} (f : α → β) (x : m α) : m β :=
+    Bind2.bind x (pure ∘ f)
+  seq {α β} (f : m (α → β)) (x : Unit -> m α) : m β :=
+    Bind2.bind f fun y => Functor.map y (x ())
+  seqLeft {α β} (x : m α) (y : Unit → m β) :=
+    Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
+  seqRight {α β} (x : m α) (y : Unit → m β) :=
+    Bind2.bind x fun _ => y ()
diff --git a/tests/elab/structureElab.lean b/tests/elab/structureElab.lean
index 0a49f85cc3f6..b9d69c76067b 100644
--- a/tests/elab/structureElab.lean
+++ b/tests/elab/structureElab.lean
@@ -449,41 +449,134 @@ structure S4 extends S2, S3
 
 end TestO2
 
+namespace TestOptParam
+
+/-!
+All fields are in scope when elaborating default values.
+-/
+structure Loop where
+  x : Nat := y
+  y : Nat := x
+  deriving Repr
+
+/-- info: { x := 1, y := 1 } -/
+#guard_msgs in #eval { x := 1 : Loop }
+/-- info: { x := 2, y := 2 } -/
+#guard_msgs in #eval { y := 2 : Loop }
+/-- info: { x := 1, y := 2 } -/
+#guard_msgs in #eval { x := 1, y := 2 : Loop }
+
+/-!
+Testing a loop that goes through the parent structure.
+-/
+structure Base where
+  x : Nat
+  y : Nat := x
+  deriving Repr
+structure Loop2 extends Base where
+  x := y
+  deriving Repr
+/-- info: { toBase := { x := 1, y := 1 } } -/
+#guard_msgs in #eval { x := 1 : Loop2 }
+/-- info: { toBase := { x := 2, y := 2 } } -/
+#guard_msgs in #eval { y := 2 : Loop2 }
+
+/-!
+Restating the type of an inherited field is OK
+-/
+structure RestateType extends Base where
+  x : Nat := 1
+  deriving Repr
+/-- info: { toBase := { x := 1, y := 1 } } -/
+#guard_msgs in #eval { : RestateType }
+
+/-!
+Restating the type of an inherited field is a valid
+way to change the binder names.
+-/
+structure A (m : Type → Type) where
+  map (f : α → β) : m α → m β
+structure A' extends A List where
+  map {α β} (g : α → β) (xs : List α) : List β := List.map g xs
+
+/-- info: A'.mk (A.mk fun {α β} g xs => List.map g xs) : A' -/
+#guard_msgs in #check { : A'}
+
+/-!
+Default values cannot refer to the field.
+-/
+/-- error: Unknown identifier `x` -/
+#guard_msgs in
+structure InapplicableDefault1 where
+  x : Nat := x + 1
+
+/-!
+Default values can refer to later fields.
+-/
+structure ApplicableDefault2 where
+  x : Nat := y + 1
+  y : Fin 2
+
+/-!
+Default values cannot refer to later fields if they depend on the field.
+-/
+/-- error: Unknown identifier `y` -/
+#guard_msgs in
+structure InpplicableDefault3 where
+  x : Nat := y + 1
+  y : Fin x
+
+/-!
+Default values cannot refer to the field, even for inherited fields.
+-/
+structure Base2 where
+  x : Nat
+/-- error: Unknown identifier `x` -/
+#guard_msgs in
+structure InapplicableDefault2 extends Base2 where
+  x := x
+
+end TestOptParam
+
 /-!
 Some failures from unsupported autoparams
 -/
 namespace TestFail1
 
-/-- error: Invalid field declaration: Type must be provided when auto-param tactic is used -/
+/-- error: Failed to infer type of field `x` -/
 #guard_msgs in
 structure F1 where
   x := by exact 0
 
 structure F2 where
   x (n : Nat) : Nat
-/-- error: Omit the type of field `x` to set its auto-param tactic -/
+/--
+error: Invalid field: Uexpected type for field `x` when setting auto-param tactic for inherited field
+-/
 #guard_msgs in
 structure F3 extends F2 where
   x : Nat → Nat := by exact 0
 
-/-- error: Invalid field: Unexpected binders when setting auto-param tactic for inherited field -/
+/--
+error: Invalid field: Unexpected binders for field `x` when setting auto-param tactic for inherited field
+-/
 #guard_msgs in
 structure F4 extends F2 where
   x (n : Nat) := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F5 extends F2 where
   x := by exact 0
   x := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F6 extends F2 where
   x := id
   x := by exact 0
 
-/-- error: A new default value for field `x` has already been set in this structure -/
+/-- error: A default value for field `x` has already been set for this structure -/
 #guard_msgs in
 structure F7 extends F2 where
   x := by exact 0
diff --git a/tests/elab_fail/mvarAtDefaultValue.lean.out.expected b/tests/elab_fail/mvarAtDefaultValue.lean.out.expected
index 8a312701e066..2746fb1b4f05 100644
--- a/tests/elab_fail/mvarAtDefaultValue.lean.out.expected
+++ b/tests/elab_fail/mvarAtDefaultValue.lean.out.expected
@@ -1,6 +1,4 @@
 mvarAtDefaultValue.lean:5:7-5:8: error: Failed to infer default value for field `x`
 mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder
 context:
-x : Nat
-toA : A := ⋯
 ⊢ Nat
diff --git a/tests/elab_fail/struct1.lean b/tests/elab_fail/struct1.lean
index 95fd8c9c2d53..a3568fab514f 100644
--- a/tests/elab_fail/struct1.lean
+++ b/tests/elab_fail/struct1.lean
@@ -36,22 +36,22 @@ structure S' extends A Nat where
 (x := true) -- error type mismatch
 
 structure S extends A Nat where
-(x : Bool := true) -- error omit type
+(x : Bool := true) -- error type mismatch
 
 structure S'' where
 (x : Nat := true) -- error type mismatch
 
-private structure S where
+private structure Spriv where
 private mk :: (x : Nat)
 
-private structure S where
+private structure Spriv where
 protected mk :: (x : Nat)
 
-private structure S where
+private structure Spriv where
 protected (x : Nat)
 
-private structure S where
+private structure Spriv where
 mk2 :: (x : Nat)
 
-#check S
+#check Spriv
 #check S.mk2
diff --git a/tests/elab_fail/struct1.lean.out.expected b/tests/elab_fail/struct1.lean.out.expected
index 7032d3761fc7..e4da83a2fce8 100644
--- a/tests/elab_fail/struct1.lean.out.expected
+++ b/tests/elab_fail/struct1.lean.out.expected
@@ -21,7 +21,12 @@ has type
   Bool
 but is expected to have type
   Nat
-struct1.lean:39:5-39:9: error: Omit the type of field `x` to set its default value
+struct1.lean:39:1-39:2: error: Type mismatch
+  true
+has type
+  Bool
+but is expected to have type
+  Nat
 struct1.lean:42:12-42:16: error: Type mismatch
   true
 has type
@@ -34,5 +39,5 @@ Hint: Remove `private` modifier from constructor
   p̵r̵i̵v̵a̵t̵e̵ ̵mk ::
 struct1.lean:48:0-48:15: error: Constructor cannot be `protected` because this structure is `private`
 struct1.lean:51:0-51:19: error: Field cannot be marked `protected` because this structure is `private`
-S : Type
-S.mk2 (x : Nat) : S
+Spriv : Type
+struct1.lean:57:7-57:12: error(lean.unknownIdentifier): Unknown constant `S.mk2`
diff --git a/tests/elab_fail/structDefValueOverride.lean.out.expected b/tests/elab_fail/structDefValueOverride.lean.out.expected
index ef2bd4f2ffa3..ba00cfc6cfb3 100644
--- a/tests/elab_fail/structDefValueOverride.lean.out.expected
+++ b/tests/elab_fail/structDefValueOverride.lean.out.expected
@@ -1 +1 @@
-structDefValueOverride.lean:6:2-6:3: error: A new default value for field `x` has already been set in this structure
+structDefValueOverride.lean:6:2-6:3: error: A default value for field `x` has already been set for this structure