style: consolidate error message construction

Author: jrr6

src/Lean/Elab/MutualInductive.lean

@@ -970,18 +970,14 @@ private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) : T
   for { view, .. } in elabs do
     let typeDeclName := privateToUserName view.declName
     if let some (prevNameIsType, prevRef) := uniqueNames[typeDeclName]? then
-      if prevNameIsType then
-        throwErrorsAt prevRef view.declId m!"cannot define multiple inductive types with the same name '{typeDeclName}'"
-      else
-        throwErrorsAt prevRef view.declId m!"cannot define an inductive type and a constructor with the same name '{typeDeclName}'"
+      let declKinds := if prevNameIsType then "multiple inductive types" else "an inductive type and a constructor"
+      throwErrorsAt prevRef view.declId m!"cannot define {declKinds} with the same name '{typeDeclName}'"
     uniqueNames := uniqueNames.insert typeDeclName (true, view.declId)
     for ctor in view.ctors do
       let ctorName := privateToUserName ctor.declName
       if let some (prevNameIsType, prevRef) := uniqueNames[ctorName]? then
-        if prevNameIsType then
-          throwErrorsAt prevRef ctor.declId m!"cannot define an inductive type and a constructor with the same name '{typeDeclName}'"
-        else
-          throwErrorsAt prevRef ctor.declId m!"cannot define multiple constructors with the same name '{ctorName}'"
+        let declKinds := if prevNameIsType then "an inductive type and a constructor" else "multiple constructors"
+        throwErrorsAt prevRef ctor.declId m!"cannot define {declKinds} with the same name '{ctorName}'"
       uniqueNames := uniqueNames.insert ctorName (false, ctor.declId)
 
 private def applyComputedFields (indViews : Array InductiveView) : CommandElabM Unit := do