diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 868c818f66..51cc3c1cc9 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -435,7 +435,7 @@ private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
       match fieldMap.find? fieldName with
       | some (prevField::restFields) =>
         if field.isSimple || prevField.isSimple then
-          throwErrorAt field.ref "field '{fieldName}' has already beed specified"
+          throwErrorAt field.ref "field '{fieldName}' has already been specified"
         else
           return fieldMap.insert fieldName (field::prevField::restFields)
       | _ => return fieldMap.insert fieldName [field]
diff --git a/tests/lean/structInst1.lean.expected.out b/tests/lean/structInst1.lean.expected.out
index 9903d88d86..6cd127f3e2 100644
--- a/tests/lean/structInst1.lean.expected.out
+++ b/tests/lean/structInst1.lean.expected.out
@@ -1,3 +1,3 @@
-structInst1.lean:12:11-12:19: error: field 'toA' has already beed specified
+structInst1.lean:12:11-12:19: error: field 'toA' has already been specified
 f5 : C → A → C
 f6 : C → A → A