diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 0d3b6b036a..1552cd9ebe 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -307,7 +307,7 @@ syntax (name := Lean.Parser.Command.classAbbrev)
 macro_rules
   | `($mods:declModifiers class abbrev $id $params* $[: $ty]? := $[ $parents $[,]? ]*) =>
     let ctor := mkIdentFrom id <| id.raw[0].getId.modifyBase (. ++ `mk)
-    `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
+    `($mods:declModifiers class $id $params* extends $[$parents:term],* $[: $ty:term]?
       attribute [instance] $ctor)
 
 macro_rules
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 1e6b900bef..9dff5773d6 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -28,10 +28,20 @@ open TSyntax.Compat
 
 /-! Recall that the `structure command syntax is
 ```
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
+leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields)
 ```
 -/
 
+structure StructParentView where
+  ref        : Syntax
+  /-- Ref to use for the parent projection. -/
+  projRef    : Syntax
+  /-- The name of the parent projection (without macro scopes). -/
+  name?      : Option Name
+  /-- The name of the parent projection (with macro scopes). Used for local name during elaboration. -/
+  rawName?   : Option Name
+  type       : Syntax
+
 structure StructFieldView where
   ref        : Syntax
   modifiers  : Modifiers
@@ -48,20 +58,29 @@ structure StructFieldView where
   value?     : Option Syntax
 
 structure StructView extends InductiveView where
-  parents         : Array Syntax
-  fields          : Array StructFieldView
+  parents : Array StructParentView
+  fields  : Array StructFieldView
   deriving Inhabited
 
 def StructView.ctor : StructView → CtorView
   | { ctors := #[ctor], ..} => ctor
   | _ => unreachable!
 
+/--
+Elaborated parent info.
+-/
 structure StructParentInfo where
-  ref        : Syntax
-  fvar?      : Option Expr
-  structName : Name
-  subobject  : Bool
-  type       : Expr
+  ref         : Syntax
+  /-- Whether to add term info to the ref. False if there's no user-provided parent projection. -/
+  addTermInfo : Bool
+  fvar?       : Option Expr
+  structName  : Name
+  /-- Field name for parent. -/
+  name        : Name
+  /-- Name of the projection function. -/
+  declName    : Name
+  subobject   : Bool
+  type        : Expr
   deriving Inhabited
 
 inductive StructFieldKind where
@@ -70,6 +89,9 @@ inductive StructFieldKind where
   | subobject (structName : Name)
   deriving Inhabited, DecidableEq, Repr
 
+/--
+Elaborated field info.
+-/
 structure StructFieldInfo where
   ref      : Syntax
   name     : Name
@@ -125,6 +147,45 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
       addDeclarationRangesFromSyntax declName ctor[1]
       pure { ref := ctor[1], declId := ctor[1], modifiers := ctorModifiers, declName }
 
+/--
+```
+def structParent := leading_parser optional (atomic (ident >> " : ")) >> termParser
+def «extends»    := leading_parser " extends " >> sepBy1 structParent ", "
+```
+-/
+private def expandParents (optExtendsStx : Syntax) : TermElabM (Array StructParentView) := do
+  let parentDecls := if optExtendsStx.isNone then #[] else optExtendsStx[0][1].getSepArgs
+  parentDecls.mapM fun parentDecl => withRef parentDecl do
+    unless parentDecl.isOfKind ``Parser.Command.structParent do
+      -- Old style, to avoid stage0 update
+      return {
+        ref := parentDecl
+        projRef := parentDecl
+        name? := none
+        rawName? := none
+        type := parentDecl
+      }
+    let mut projRef  := parentDecl
+    let mut rawName? := none
+    let mut name? := none
+    unless parentDecl[0].isNone do
+      let ident := parentDecl[0][0]
+      let rawName := ident.getId
+      let name := rawName.eraseMacroScopes
+      unless name.isAtomic do
+        throwErrorAt ident "invalid parent projection name '{name}', names must be atomic"
+      projRef  := ident
+      rawName? := rawName
+      name? := name
+    let type := parentDecl[1]
+    return {
+      ref := parentDecl
+      projRef
+      name?
+      rawName?
+      type
+    }
+
 def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
   if modifiers.isNoncomputable then
     throwError "invalid use of 'noncomputable' in field declaration"
@@ -215,11 +276,12 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
       }
 
 /-
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >>
+leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >>
   optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
 
 where
-def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
+def structParent := leading_parser optional (atomic (ident >> " : ")) >> termParser
+def «extends» := leading_parser " extends " >> sepBy1 structParent ", "
 def typeSpec := leading_parser " : " >> termParser
 def optType : Parser := optional typeSpec
 
@@ -234,9 +296,20 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
   let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   addDeclarationRangesForBuiltin declName modifiers.stx stx
   let binders   := stx[2]
-  let exts      := stx[3]
-  let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
-  let optType   := stx[4]
+  -- Compatibility mode (to avoid stage0 update): extract type and extends clauses from syntax:
+  let (optType, exts) ←
+    if (!stx[4].isNone && stx[4][0].isOfKind ``Parser.Term.typeSpec)
+        || (!stx[3].isNone && stx[3][0].isOfKind ``Parser.Command.extends) then
+      pure (stx[4], stx[3])
+    else if stx[3].isNone && !stx[4].isNone && !stx[4][0][2].isNone then
+      -- TODO: enable warning
+      -- logWarningAt stx[4][0][2][0] "\
+      --   Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'.\n\n\
+      --   The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections."
+      pure (stx[4][0][2], stx[4])
+    else
+      pure (stx[3], stx[4])
+  let parents   ← expandParents exts
   let derivingClasses ← getOptDerivingClasses stx[6]
   let type?     := if optType.isNone then none else some optType[0][1]
   let ctor ← expandCtor stx modifiers declName
@@ -279,6 +352,10 @@ private def replaceFieldInfo (infos : Array StructFieldInfo) (info : StructField
 
 /-- Return `some fieldName` if field `fieldName` of the parent structure `parentStructName` is already in `infos` -/
 private def findExistingField? (infos : Array StructFieldInfo) (parentStructName : Name) : CoreM (Option Name) := do
+  -- Check if `parentStructName` is represented as a subobject field.
+  if let some info := infos.find? (·.kind == .subobject parentStructName) then
+    return info.name
+  -- Otherwise check for field overlap.
   let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName
   for fieldName in fieldNames do
     if containsFieldName infos fieldName then
@@ -437,6 +514,7 @@ where
         let fieldType ← getFieldType infos parentType fieldName
         match findFieldInfo? infos fieldName with
         | some existingFieldInfo =>
+          -- TODO: make sure parent projections are checked too
           let existingFieldType ← inferType existingFieldInfo.fvar
           unless (← isDefEq fieldType existingFieldType) do
             throwError "parent field type mismatch, field '{fieldName}' from parent '{.ofConstName parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
@@ -444,7 +522,27 @@ where
           copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames
         | none =>
           let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
-          let addNewField : TermElabM α := do
+          if let some fieldParentStructName := fieldInfo.subobject? then
+            if (← findExistingField? infos fieldParentStructName).isSome then
+              -- See comment at `copyDefaultValue?`
+              let expandedStructNames := expandedStructNames.insert fieldParentStructName
+              copyFields infos expandedStructNames fieldType fun infos nestedFieldMap expandedStructNames => do
+                let fieldVal ← mkCompositeField fieldType nestedFieldMap
+                copy (i+1) infos (fieldMap.insert fieldName fieldVal) expandedStructNames
+            else
+              let subfieldNames := getStructureFieldsFlattened (← getEnv) fieldParentStructName
+              let fieldName := fieldInfo.fieldName
+              -- This error should never happen:
+              if let some info := infos.find? (·.kind == .subobject fieldParentStructName) then
+                throwError "projection field name conflict, ancestor '{.ofConstName fieldParentStructName}' \
+                  has projection fields '{info.name}' and '{fieldName}'"
+              withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar => do
+                let infos := infos.push { ref := (← getRef)
+                                          name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar,
+                                          kind := StructFieldKind.subobject fieldParentStructName }
+                processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos =>
+                  copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames
+          else
             withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do
               let fieldMap := fieldMap.insert fieldName fieldFVar
               let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
@@ -455,25 +553,6 @@ where
                                         name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
                                         kind := StructFieldKind.copiedField }
               copy (i+1) infos fieldMap expandedStructNames
-          if let some parentParentStructName := fieldInfo.subobject? then
-            let fieldParentStructName ← getStructureName fieldType
-            if (← findExistingField? infos fieldParentStructName).isSome then
-              -- See comment at `copyDefaultValue?`
-              let expandedStructNames := expandedStructNames.insert fieldParentStructName
-              copyFields infos expandedStructNames fieldType fun infos nestedFieldMap expandedStructNames => do
-                let fieldVal ← mkCompositeField fieldType nestedFieldMap
-                copy (i+1) infos (fieldMap.insert fieldName fieldVal) expandedStructNames
-            else
-              let subfieldNames := getStructureFieldsFlattened (← getEnv) fieldParentStructName
-              let fieldName := fieldInfo.fieldName
-              withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar => do
-                let infos := infos.push { ref := (← getRef)
-                                          name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar,
-                                          kind := StructFieldKind.subobject parentParentStructName }
-                processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos =>
-                  copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames
-          else
-            addNewField
       else
         let infos ← processOveriddenDefaultValues infos fieldMap expandedStructNames parentStructName
         k infos fieldMap expandedStructNames
@@ -496,15 +575,12 @@ where
       | none => throwError "failed to copy fields from parent structure{indentExpr parentType}" -- TODO improve error message
     return result
 
-private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) : Name := Id.run do
-  let base := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString!
-  if p base then
-    base
-  else
-    let rec go (i : Nat) : Name :=
-      let curr := base.appendIndexAfter i
-      if p curr then curr else go (i+1)
-    go 1
+private partial def mkToParentName (parentView : StructParentView) (parentStructName : Name) : Name × Name :=
+  match parentView.rawName?, parentView.name? with
+  | some rawName, some name => (rawName, name)
+  | _, _ => Id.run do
+    let toParentName := Name.mkSimple <| "to" ++ parentStructName.eraseMacroScopes.getString!
+    (toParentName, toParentName)
 
 private def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr)
     (k : Array StructFieldInfo → Array StructParentInfo → TermElabM α) : TermElabM α := do
@@ -512,37 +588,88 @@ private def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFV
 where
   go (i : Nat) (infos : Array StructFieldInfo) (parents : Array StructParentInfo) : TermElabM α := do
     if h : i < view.parents.size then
-      let parent := view.parents[i]
-      withRef parent do
+      let parentView := view.parents[i]
+      withRef parentView.ref do
       -- The only use case for autobound implicits for parents might be outParams, but outParam is not propagated.
-      let type ← Term.withoutAutoBoundImplicit <| Term.elabType parent
-      let parentType ← whnf type
+      let parentType ← whnf <| ← Term.withoutAutoBoundImplicit <| Term.elabType parentView.type
       if parentType.getAppFn == indFVar then
         logWarning "structure extends itself, skipping"
         return ← go (i + 1) infos parents
       if rs.any (fun r => r.indFVar == parentType.getAppFn) then
         throwError "structure cannot extend types defined in the same mutual block"
-      let parentStructName ← getStructureName parentType
-      if parents.any (fun info => info.structName == parentStructName) then
+      let parentStructName ← try
+          getStructureName parentType
+        catch ex =>
+          throwErrorAt parentView.type "{ex.toMessageData}\n\n\
+            This error is possibly due to a change in the 'structure' syntax. \
+            Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'.\n\n\
+            The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections."
+      let (rawToParentName, toParentName) := mkToParentName parentView parentStructName
+      -- Name of the parent projection declaration
+      let declName := view.declName ++ toParentName
+      withRef parentView.projRef do checkNotAlreadyDeclared declName
+      let throwParentNameError {β} : TermElabM β := withRef parentView.projRef do
+        if parentView.name?.isSome then
+          throwError "field '{toParentName}' has already been declared"
+        else
+          throwError "field '{toParentName}' has already been declared, \
+            use 'toParent : P' syntax to give a unique name for the parent projection"
+      if parents.any (·.structName == parentStructName) then
         logWarning m!"duplicate parent structure '{.ofConstName parentStructName}', skipping"
         go (i + 1) infos parents
-      else if let some existingFieldName ← findExistingField? infos parentStructName then
+      else if (← findExistingField? infos parentStructName).isSome || (findFieldInfo? infos toParentName).isSome then
         if structureDiamondWarning.get (← getOptions) then
-          logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
-        let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType }
-        copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos parents
+          if let some existingFieldName ← findExistingField? infos parentStructName then
+            logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
+        copyNewFieldsFrom view.declName infos parentType fun infos => do
+          if let some info := infos.find? (·.kind == .subobject parentStructName) then
+            if info.name != toParentName then
+              throwError "parent is an ancestor of a previous parent, but projection name '{toParentName}' does not match '{info.name}'"
+            pure ()
+          else
+            if let some info := findFieldInfo? infos toParentName then
+              unless ← isDefEq (← inferType info.fvar) parentType do
+                throwParentNameError
+            if (parents.find? (·.name == toParentName)).isSome then
+              throwParentNameError
+          let parents := parents.push {
+            ref := parentView.projRef
+            addTermInfo := parentView.name?.isSome
+            fvar? := none
+            subobject := false
+            structName := parentStructName
+            name := toParentName
+            declName
+            type := parentType
+          }
+          go (i + 1) infos parents
         -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
       else
         let env ← getEnv
         let subfieldNames := getStructureFieldsFlattened env parentStructName
-        let toParentName := mkToParentName parentStructName fun n => !containsFieldName infos n && !subfieldNames.contains n
+        if containsFieldName infos toParentName || subfieldNames.contains toParentName || (parents.find? (·.name == toParentName)).isSome then
+          throwParentNameError
         let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
-        withLocalDecl toParentName binfo parentType fun parentFVar =>
-          let infos := infos.push { ref := parent,
-                                    name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar,
-                                    kind := StructFieldKind.subobject parentStructName }
-          let parents := parents.push { ref := parent, fvar? := parentFVar, subobject := true, structName := parentStructName, type := parentType }
-          processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos parents
+        withLocalDecl rawToParentName binfo parentType fun parentFVar =>
+          let infos := infos.push {
+            ref := parentView.projRef
+            name := toParentName
+            declName
+            fvar := parentFVar
+            kind := StructFieldKind.subobject parentStructName
+          }
+          let parents := parents.push {
+            ref := parentView.projRef
+            addTermInfo := parentView.name?.isSome
+            fvar? := parentFVar
+            subobject := true
+            structName := parentStructName
+            name := toParentName
+            declName
+            type := parentType
+          }
+          processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos =>
+            go (i+1) infos parents
     else
       k infos parents
 
@@ -585,13 +712,15 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
         let value ← mkLambdaFVars params value
         return (type, value)
 
-private partial def withFields (views : Array StructFieldView) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
+private partial def withFields (parents : Array StructParentInfo) (views : Array StructFieldView) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
   go 0 {} infos
 where
   go (i : Nat) (defaultValsOverridden : NameSet) (infos : Array StructFieldInfo) : TermElabM α := do
     if h : i < views.size then
       let view := views[i]
       withRef view.ref do
+      if let some parent := parents.find? (·.name == view.name) then
+        throwError "field '{view.name}' has already been declared as a projection for parent '{.ofConstName parent.structName}'"
       match findFieldInfo? infos view.name with
       | none      =>
         let (type?, value?) ← elabFieldTypeValue view
@@ -806,7 +935,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
         result := mkApp result fieldVal
     return result
   let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType)))
-  let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n)
+  let declName := parent.declName
   -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque)
   let cval : ConstantVal := { name := declName, levelParams, type := declType }
   if isProp then
@@ -894,7 +1023,7 @@ def elabStructureCommand : InductiveElabDescr where
       view := view.toInductiveView
       elabCtors := fun rs r params => do
         withParents view rs r.indFVar fun parentFieldInfos parents =>
-        withFields view.fields parentFieldInfos fun fieldInfos => do
+        withFields parents view.fields parentFieldInfos fun fieldInfos => do
         withRef view.ref do
           Term.synthesizeSyntheticMVarsNoPostponing
           let lctx ← getLCtx
@@ -916,6 +1045,11 @@ def elabStructureCommand : InductiveElabDescr where
                     Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
             finalize := fun levelParams params replaceIndFVars => do
               let parentInfos ← mkRemainingProjections levelParams params view parents fieldInfos
+              withSaveInfoContext do
+                -- Add terminfo for parents now that all parent projections exist.
+                for parent in parents do
+                  if parent.addTermInfo then
+                    Term.addTermInfo' parent.ref (← mkConstWithLevelParams parent.declName) (isBinder := true)
               setStructureParents view.declName parentInfos
               checkResolutionOrder view.declName
               if view.isClass then
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 2a3808a841..ea86e88a24 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -226,13 +226,16 @@ def structureTk          := leading_parser
   "structure "
 def classTk              := leading_parser
   "class "
+def structParent        := leading_parser
+  optional (atomic (ident >> " : ")) >> termParser
 def «extends»            := leading_parser
-  " extends " >> sepBy1 termParser ", "
+  -- The optType is to catch code that uses the old order for optType and extends.
+  " extends " >> sepBy1 structParent ", " >> Term.optType
 def «structure»          := leading_parser
     (structureTk <|> classTk) >>
     -- Note: no error recovery here due to clashing with the `class abbrev` syntax
     declId >>
-    ppIndent (many (ppSpace >> Term.bracketedBinder) >> optional «extends» >> Term.optType) >>
+    ppIndent (many (ppSpace >> Term.bracketedBinder) >> Term.optType >> optional «extends») >>
     optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >>
     optDeriving
 @[builtin_command_parser] def declaration := leading_parser
diff --git a/tests/lean/diamond5.lean b/tests/lean/diamond5.lean
index f359a4bb62..d708df5888 100644
--- a/tests/lean/diamond5.lean
+++ b/tests/lean/diamond5.lean
@@ -12,6 +12,10 @@ set_option structureDiamondWarning false
 
 def D.toC (x : Nat) := x
 
+/-- error: 'D.toC' has already been declared -/
+#guard_msgs in
 class D (α : Type) extends B α, C α
 
+class D (α : Type) extends B α, toC_1 : C α
+
 #check D.toC_1
diff --git a/tests/lean/interactive/structNameParentProj.lean b/tests/lean/interactive/structNameParentProj.lean
new file mode 100644
index 0000000000..cea02ef783
--- /dev/null
+++ b/tests/lean/interactive/structNameParentProj.lean
@@ -0,0 +1,8 @@
+/-!
+# Testing named parent projections for `structure`s
+-/
+
+structure S where
+
+structure S' extends toParent : S where
+                     --^ textDocument/hover
diff --git a/tests/lean/interactive/structNameParentProj.lean.expected.out b/tests/lean/interactive/structNameParentProj.lean.expected.out
new file mode 100644
index 0000000000..da5a62e9d6
--- /dev/null
+++ b/tests/lean/interactive/structNameParentProj.lean.expected.out
@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file:///structNameParentProj.lean"},
+ "position": {"line": 6, "character": 23}}
+{"range":
+ {"start": {"line": 6, "character": 21}, "end": {"line": 6, "character": 29}},
+ "contents":
+ {"value": "```lean\nS'.toParent (self : S') : S\n```", "kind": "markdown"}}
diff --git a/tests/lean/run/3150.lean b/tests/lean/run/3150.lean
index a7cafeb5fd..4bb5f22555 100644
--- a/tests/lean/run/3150.lean
+++ b/tests/lean/run/3150.lean
@@ -11,7 +11,7 @@ structure Subone where
   mem : R → Prop
   one_mem : mem One.one
 
-structure Subalgebra [OneHom R A] extends Subone A : Type where
+structure Subalgebra [OneHom R A] : Type extends Subone A where
   algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
   one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
 
diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean
index 2d89e9d912..0febd7b3ba 100644
--- a/tests/lean/run/3807.lean
+++ b/tests/lean/run/3807.lean
@@ -954,8 +954,8 @@ structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass
 
 infixr:25 " →+ " => AddMonoidHom
 
-class AddMonoidHomClass (F M N : Type _) [AddZeroClass M] [AddZeroClass N] [FunLike F M N]
-  extends AddHomClass F M N, ZeroHomClass F M N : Prop
+class AddMonoidHomClass (F M N : Type _) [AddZeroClass M] [AddZeroClass N] [FunLike F M N] : Prop
+  extends AddHomClass F M N, ZeroHomClass F M N
 
 section One
 
@@ -1053,8 +1053,8 @@ structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] ex
 infixr:25 " →* " => MonoidHom
 
 class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
-  [FunLike F M N]
-  extends MulHomClass F M N, OneHomClass F M N : Prop
+  [FunLike F M N] : Prop
+  extends MulHomClass F M N, OneHomClass F M N
 
 instance MonoidHom.instFunLike : FunLike (M →* N) M N where
   coe f := f.toFun
@@ -1120,7 +1120,7 @@ variable {F α β γ δ : Type _} [MulZeroOneClass α] [MulZeroOneClass β] [Mul
   [MulZeroOneClass δ]
 
 class MonoidWithZeroHomClass (F : Type _) (α β : outParam (Type _)) [MulZeroOneClass α]
-  [MulZeroOneClass β] [FunLike F α β] extends MonoidHomClass F α β, ZeroHomClass F α β : Prop
+  [MulZeroOneClass β] [FunLike F α β] : Prop extends MonoidHomClass F α β, ZeroHomClass F α β
 
 structure MonoidWithZeroHom (α β : Type _) [MulZeroOneClass α] [MulZeroOneClass β]
   extends ZeroHom α β, MonoidHom α β
@@ -1211,8 +1211,8 @@ infixr:25 " →+* " => RingHom
 section RingHomClass
 
 class RingHomClass (F : Type _) (α β : outParam (Type _))
-    [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β]
-  extends MonoidHomClass F α β, AddMonoidHomClass F α β, MonoidWithZeroHomClass F α β : Prop
+    [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] : Prop
+  extends MonoidHomClass F α β, AddMonoidHomClass F α β, MonoidWithZeroHomClass F α β
 
 variable [FunLike F α β]
 
@@ -1870,7 +1870,7 @@ universe u v w
 section AddSubmonoidWithOneClass
 
 class AddSubmonoidWithOneClass (S R : Type _) [AddMonoidWithOne R]
-  [SetLike S R] extends AddSubmonoidClass S R : Prop
+  [SetLike S R] : Prop extends AddSubmonoidClass S R
 
 variable {S R : Type _} [AddMonoidWithOne R] [SetLike S R] (s : S)
 
@@ -1889,7 +1889,7 @@ variable {R : Type u} {S : Type v} [NonAssocSemiring R]
 section SubsemiringClass
 
 class SubsemiringClass (S : Type _) (R : Type u) [NonAssocSemiring R]
-  [SetLike S R] extends SubmonoidClass S R, AddSubmonoidClass S R : Prop
+  [SetLike S R] : Prop extends SubmonoidClass S R, AddSubmonoidClass S R
 
 instance (priority := 100) SubsemiringClass.addSubmonoidWithOneClass (S : Type _)
     (R : Type u) [NonAssocSemiring R] [SetLike S R] [h : SubsemiringClass S R] :
@@ -1963,8 +1963,8 @@ variable {R : Type u} {S : Type v} {T : Type w} [Ring R]
 
 section SubringClass
 
-class SubringClass (S : Type _) (R : Type u) [Ring R] [SetLike S R] extends
-  SubsemiringClass S R : Prop
+class SubringClass (S : Type _) (R : Type u) [Ring R] [SetLike S R] : Prop
+  extends SubsemiringClass S R
 
 instance (priority := 100) SubringClass.addSubmonoidClass (S : Type _) (R : Type u)
     [SetLike S R] [Ring R] [h : SubringClass S R] : AddSubmonoidClass S R :=
@@ -2070,7 +2070,7 @@ notation:25 A " →ₐ[" R "] " B => AlgHom R A B
 from `A` to `B`.  -/
 class AlgHomClass (F : Type _) (R A B : outParam (Type _))
   [Semiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
-  [FunLike F A B] extends RingHomClass F A B : Prop where
+  [FunLike F A B] : Prop extends RingHomClass F A B where
   commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
 
 namespace AlgHom
@@ -2179,8 +2179,8 @@ section Mathlib.Algebra.Algebra.Subalgebra.Basic
 universe u u' v w
 
 /-- A subalgebra is a sub(semi)ring that includes the range of `algebraMap`. -/
-structure Subalgebra (R : Type u) (A : Type v) [Semiring R] [Semiring A] [Algebra R A] extends
-    Subsemiring A : Type v where
+structure Subalgebra (R : Type u) (A : Type v) [Semiring R] [Semiring A] [Algebra R A] : Type v
+  extends Subsemiring A  where
 
 namespace Subalgebra
 
@@ -2346,7 +2346,7 @@ variable {K : Type u} {L : Type v}
 variable [DivisionRing K] [DivisionRing L]
 
 /-- `SubfieldClass S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
-class SubfieldClass (S K : Type _) [DivisionRing K] [SetLike S K] extends SubringClass S K : Prop
+class SubfieldClass (S K : Type _) [DivisionRing K] [SetLike S K] : Prop extends SubringClass S K
 
 namespace SubfieldClass
 
diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean
index acd5481360..37c98842ad 100644
--- a/tests/lean/run/4171.lean
+++ b/tests/lean/run/4171.lean
@@ -55,7 +55,7 @@ universe v u
 
 namespace CategoryTheory
 
-class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
   id : ∀ X : obj, Hom X X
   comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
 
@@ -63,7 +63,7 @@ scoped notation "𝟙" => CategoryStruct.id
 
 scoped infixr:80 " ≫ " => CategoryStruct.comp
 
-class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
   id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
   comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
 
@@ -79,8 +79,8 @@ namespace CategoryTheory
 
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
-structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂
+    extends Prefunctor C D where
 
 infixr:26 " ⥤ " => Functor
 
diff --git a/tests/lean/run/4595_slowdown.lean b/tests/lean/run/4595_slowdown.lean
index 3c1e2d9c55..7024152182 100644
--- a/tests/lean/run/4595_slowdown.lean
+++ b/tests/lean/run/4595_slowdown.lean
@@ -20,7 +20,7 @@ section Mathlib.CategoryTheory.Category.Basic
 
 namespace CategoryTheory
 
-class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
   id : ∀ X : obj, Hom X X
   comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
 
@@ -28,7 +28,7 @@ scoped notation "𝟙" => CategoryStruct.id
 
 scoped infixr:80 " ≫ " => CategoryStruct.comp
 
-class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
   id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
   comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
 
@@ -40,8 +40,8 @@ section Mathlib.CategoryTheory.Functor.Basic
 
 namespace CategoryTheory
 
-structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂
+    extends Prefunctor C D where
 
 infixr:26 " ⥤ " => Functor
 
diff --git a/tests/lean/run/6123_cat_adjunction.lean b/tests/lean/run/6123_cat_adjunction.lean
index af810102de..39f2879643 100644
--- a/tests/lean/run/6123_cat_adjunction.lean
+++ b/tests/lean/run/6123_cat_adjunction.lean
@@ -57,14 +57,14 @@ universe v u
 
 namespace CategoryTheory
 
-class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
   id : ∀ X : obj, Hom X X
   comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
 
 scoped notation "𝟙" => CategoryStruct.id
 scoped infixr:80 " ≫ " => CategoryStruct.comp
 
-class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
 
 end CategoryTheory
 
@@ -76,8 +76,8 @@ namespace CategoryTheory
 
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
-structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂
+    extends Prefunctor C D where
 
 infixr:26 " ⥤ " => Functor
 
@@ -401,7 +401,7 @@ class IsPreconnected (J : Type u₁) [Category.{v₁} J] : Prop where
   iso_constant :
     ∀ {α : Type u₁} (F : J ⥤ Discrete α) (j : J), False
 
-class IsConnected (J : Type u₁) [Category.{v₁} J] extends IsPreconnected J : Prop where
+class IsConnected (J : Type u₁) [Category.{v₁} J] : Prop extends IsPreconnected J where
   [is_nonempty : Nonempty J]
 
 variable {J : Type u₁} [Category.{v₁} J]
diff --git a/tests/lean/run/binop_binrel_perf_issue.lean b/tests/lean/run/binop_binrel_perf_issue.lean
index 2aef4272dd..2968c515cd 100644
--- a/tests/lean/run/binop_binrel_perf_issue.lean
+++ b/tests/lean/run/binop_binrel_perf_issue.lean
@@ -479,13 +479,13 @@ variable [AddZeroClass A] {t : Set A}
 
 structure Submonoid (M : Type _) [MulOneClass M] extends Subsemigroup M where
 
-class SubmonoidClass (S : Type _) (M : Type _) [MulOneClass M] [SetLike S M] extends
-  MulMemClass S M : Prop
+class SubmonoidClass (S : Type _) (M : Type _) [MulOneClass M] [SetLike S M] : Prop extends
+  MulMemClass S M
 
 structure AddSubmonoid (M : Type _) [AddZeroClass M] extends AddSubsemigroup M where
 
-class AddSubmonoidClass (S : Type _) (M : Type _) [AddZeroClass M] [SetLike S M] extends
-  AddMemClass S M : Prop
+class AddSubmonoidClass (S : Type _) (M : Type _) [AddZeroClass M] [SetLike S M] : Prop extends
+  AddMemClass S M
 
 namespace AddSubmonoid
 
@@ -806,8 +806,8 @@ universe u v
 
 variable {R : Type u} {M : Type v}
 
-structure Submodule (R : Type u) (M : Type v) [Mul R] [AddCommMonoid M] [SMul R M] extends
-  AddSubmonoid M : Type v
+structure Submodule (R : Type u) (M : Type v) [Mul R] [AddCommMonoid M] [SMul R M] : Type v
+  extends AddSubmonoid M
 
 instance setLike [Mul R] [AddCommMonoid M] [SMul R M] : SetLike (Submodule R M) M where
   coe s := s.carrier
diff --git a/tests/lean/run/inductive_univ.lean b/tests/lean/run/inductive_univ.lean
index b6e2a750ef..e7eadd343e 100644
--- a/tests/lean/run/inductive_univ.lean
+++ b/tests/lean/run/inductive_univ.lean
@@ -101,4 +101,4 @@ which is not less than or equal to the structure's resulting universe level
   1
 -/
 #guard_msgs in
-structure B extends A' : Type
+structure B : Type extends A'
diff --git a/tests/lean/run/linearCategory_perf_issue.lean b/tests/lean/run/linearCategory_perf_issue.lean
index 087b6e37f2..e195a964b9 100644
--- a/tests/lean/run/linearCategory_perf_issue.lean
+++ b/tests/lean/run/linearCategory_perf_issue.lean
@@ -182,14 +182,14 @@ section Mathlib.CategoryTheory.Category.Basic
 
 namespace CategoryTheory
 
-class CategoryStruct (obj : Type u₁) extends Quiver.{v₁ + 1} obj : Type max u₁ (v₁ + 1) where
+class CategoryStruct (obj : Type u₁) : Type max u₁ (v₁ + 1) extends Quiver.{v₁ + 1} obj where
   id : ∀ X : obj, Hom X X
   comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
 
 scoped notation "𝟙" => CategoryStruct.id  -- type as \b1
 scoped infixr:80 " ≫ " => CategoryStruct.comp -- type as \gg
 
-class Category (obj : Type u₁) extends CategoryStruct.{v₁} obj : Type max u₁ (v₁ + 1) where
+class Category (obj : Type u₁) : Type max u₁ (v₁ + 1) extends CategoryStruct.{v₁} obj where
   id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
   comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
   assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
@@ -202,8 +202,8 @@ section Mathlib.CategoryTheory.Functor.Basic
 
 namespace CategoryTheory
 
-structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
-    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂
+    extends Prefunctor C D where
 
 infixr:26 " ⥤ " => Functor -- type as \func
 
diff --git a/tests/lean/run/mathlibetaissue.lean b/tests/lean/run/mathlibetaissue.lean
index aa6598d4b1..248a518b73 100644
--- a/tests/lean/run/mathlibetaissue.lean
+++ b/tests/lean/run/mathlibetaissue.lean
@@ -86,8 +86,8 @@ section Mathlib.Algebra.GroupWithZero.Defs
 class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
 class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
 class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
-class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
-  extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
+class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop
+  extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀
 class NoZeroDivisors (M₀ : Type _) [Mul M₀] [Zero M₀] : Prop where
 class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀
 class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
@@ -122,7 +122,7 @@ class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
 class CommRing (α : Type u) extends Ring α, CommMonoid α
 instance CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
   { s with }
-class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop
+class IsDomain (α : Type u) [Semiring α] : Prop extends IsCancelMulZero α, Nontrivial α
 
 end Mathlib.Algebra.Ring.Defs
 
diff --git a/tests/lean/run/simpConfigPropagationIssue3.lean b/tests/lean/run/simpConfigPropagationIssue3.lean
index fe49dd5f30..4a9f1d781e 100644
--- a/tests/lean/run/simpConfigPropagationIssue3.lean
+++ b/tests/lean/run/simpConfigPropagationIssue3.lean
@@ -12,7 +12,7 @@ theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt := by
 end OrientedCmp
 
 /-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
-class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class TransCmp (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- The comparator operation is transitive. -/
   le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
 
diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean
index fd219bbf46..c547a806d3 100644
--- a/tests/lean/run/struct3.lean
+++ b/tests/lean/run/struct3.lean
@@ -3,19 +3,19 @@ universe u v
 class Bind2 (m : Type u → Type v) where
   bind : ∀ {α β : Type u}, m α → (α → m β) → m β
 
-class Monad2 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
+class Monad2 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
   map      := fun f x => Bind2.bind x (pure ∘ f)
   seq      := fun f x => Bind2.bind f fun y => Functor.map y (x ())
   seqLeft  := fun x y => Bind2.bind x fun a => Bind2.bind (y ()) fun _ => pure a
   seqRight := @fun α β x y => Bind2.bind x fun _ => y () -- Recall that `@` disables implicit lambda support
 
-class Monad3 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
+class Monad3 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
   map (f x)      := Bind2.bind x (pure ∘ f)
   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 ()
 
-class Monad4 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where
+class Monad4 (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind2 m where
   map f x      := Bind2.bind x (pure ∘ f)
   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
diff --git a/tests/lean/run/structInstFast.lean b/tests/lean/run/structInstFast.lean
index 6992ebf549..e398a09469 100644
--- a/tests/lean/run/structInstFast.lean
+++ b/tests/lean/run/structInstFast.lean
@@ -68,7 +68,7 @@ where go (val : TSyntax `ident) (width depth : Nat) (cmds : Array <| TSyntax `co
     let newTerm' (s : String) := if len = 1 then baseIdent else mkIdent' s (m+1)
     let fieldsStx ← mkFieldsStx type (s!"x{m}_") width
     let nextStruct ←
-      `(structure $(mkIdent' "A" m) extends $(newTerm "A") where
+      `(structure $(mkIdent' "A" m) extends $(newTerm "A"):term where
         $fieldsStx:structFields)
     let structVals ← (List.range width).mapM fun j =>
       `(Term.structInstField| $(mkIdent' s!"x{m}_" j):ident := $val)
diff --git a/tests/lean/run/structNamedParentProj.lean b/tests/lean/run/structNamedParentProj.lean
new file mode 100644
index 0000000000..db630f05ff
--- /dev/null
+++ b/tests/lean/run/structNamedParentProj.lean
@@ -0,0 +1,104 @@
+/-!
+# Testing named parent projections for `structure`s
+-/
+
+structure S where
+  x : Nat
+structure T where
+  y : Nat
+structure U where
+  x : Nat
+
+/-!
+Non-atomic parent projections are not allowed.
+-/
+/-- error: invalid parent projection name 'non.atomic', names must be atomic -/
+#guard_msgs in structure S' extends non.atomic : S
+
+/-!
+Shadowing other fields is not allowed.
+-/
+/-- error: field 'x' has already been declared -/
+#guard_msgs in structure S' extends x : S
+
+/-!
+Duplicate parent projections
+-/
+/-- error: field 'toP' has already been declared -/
+#guard_msgs in structure S' extends toP : S, toP : T
+
+/-!
+Duplicate parent projections because from different namespaces
+-/
+structure NS1.S
+structure NS2.S
+/--
+error: field 'toS' has already been declared, use 'toParent : P' syntax to give a unique name for the parent projection
+-/
+#guard_msgs in structure S' extends NS1.S, NS2.S
+
+/-!
+Duplicate parent projections, when there are overlapping fields
+-/
+/-- error: field 'toS' has already been declared -/
+#guard_msgs in structure S' extends S, toS : U
+/-- error: field 'toP' has already been declared -/
+#guard_msgs in structure S' extends toP : S, toP : T
+
+/-!
+Duplicate parent projections because from different namespaces, when there are duplicate fields
+-/
+structure NS1.S' where x : Nat
+structure NS2.S' where x : Nat
+/--
+error: field 'toS'' has already been declared, use 'toParent : P' syntax to give a unique name for the parent projection
+-/
+#guard_msgs in structure S' extends NS1.S', NS2.S'
+
+/-!
+Field conflicts with projection
+-/
+/-- error: field 'toS' has already been declared as a projection for parent 'S' -/
+#guard_msgs in structure S' extends S where
+  toS : Nat
+
+/-!
+Checking that the projection name is honored.
+-/
+structure S2 extends toTheS : S where
+  y : Nat
+/--
+info: structure S2 : Type
+number of parameters: 0
+parents:
+  S2.toTheS : S
+fields:
+  S.x : Nat
+  S2.y : Nat
+constructor:
+  S2.mk (toTheS : S) (y : Nat) : S2
+field notation resolution order:
+  S2, S
+-/
+#guard_msgs in #print S2
+
+/-!
+Checking that the projection name is honored.
+-/
+structure S2' extends toTheS : S, toTheU : U where
+  y : Nat
+/--
+info: structure S2' : Type
+number of parameters: 0
+parents:
+  S2'.toTheS : S
+  S2'.toTheU : U
+fields:
+  S.x : Nat
+  S2'.y : Nat
+constructor:
+  S2'.mk (toTheS : S) (y : Nat) : S2'
+field notation resolution order:
+  S2', S, U
+-/
+#guard_msgs in #print S2'
diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean
index 4fae68c94c..3ae927584e 100644
--- a/tests/lean/run/structWithAlgTCSynth.lean
+++ b/tests/lean/run/structWithAlgTCSynth.lean
@@ -606,8 +606,8 @@ end Mathlib.Algebra.Quotient
 
 section Mathlib.Algebra.Module.Submodule.Basic
 
-structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] extends
-  AddSubmonoid M : Type v
+structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
+  extends AddSubmonoid M
 
 def Submodule.toAddSubgroup [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) : AddSubgroup M :=
   { p.toAddSubmonoid with }
diff --git a/tests/lean/run/synthInstsIssue.lean b/tests/lean/run/synthInstsIssue.lean
index b646012316..3c6c8538d6 100644
--- a/tests/lean/run/synthInstsIssue.lean
+++ b/tests/lean/run/synthInstsIssue.lean
@@ -91,8 +91,8 @@ variable {R S S₃ T M M₃ : Type _}
 
 class LinearMapClass (F : Type _) (R : outParam (Type _))
   (M M₂ : outParam (Type _)) [Add M] [Add M₂]
-    [SMul R M] [SMul R M₂] [FunLike F M M₂]
-    extends MulActionSemiHomClass F (id : R → R) M M₂ : Prop
+    [SMul R M] [SMul R M₂] [FunLike F M M₂] : Prop
+    extends MulActionSemiHomClass F (id : R → R) M M₂
 
 variable (F : Type _)
 variable [Zero R]
diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out
index 9b39f4291d..1db6684d68 100644
--- a/tests/lean/struct1.lean.expected.out
+++ b/tests/lean/struct1.lean.expected.out
@@ -1,5 +1,9 @@
 struct1.lean:9:14-9:17: error: invalid resulting type, expecting 'Type _' or 'Prop'
 struct1.lean:12:20-12:29: error: expected structure
+
+This error is possibly due to a change in the 'structure' syntax. Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'.
+
+The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections.
 struct1.lean:15:28-15:33: warning: field 'x' from 'B' has already been declared
 struct1.lean:16:1-16:2: error: field 'x' has been declared in parent structure
 struct1.lean:17:30-17:35: warning: duplicate parent structure 'A', skipping
diff --git a/tests/lean/toFieldNameIssue.lean b/tests/lean/toFieldNameIssue.lean
index abd3f37eb4..d262906e9e 100644
--- a/tests/lean/toFieldNameIssue.lean
+++ b/tests/lean/toFieldNameIssue.lean
@@ -4,7 +4,7 @@ structure Foo.A where
 structure Boo.A extends Foo.A where
   y : Nat
 
-structure B extends Boo.A where
+structure B extends toA_1 : Boo.A where
   z : Nat
 
 def f1 (x y z : Nat) : B :=
@@ -26,7 +26,7 @@ structure Boo.C where
   x : Nat
   z : Nat
 
-structure D extends Foo.C, Boo.C
+structure D extends Foo.C, toC_1 : Boo.C
 
 def f2 (x y z : Nat) : D :=
   { x, y, z }