∀ (declName : Lean.Name) (database : Mathlib.StacksTag.Database) (tag comment : String),
  sizeOf { declName := declName, database := database, tag := tag, comment := comment } =
    1 + sizeOf declName + sizeOf database + sizeOf tag + sizeOf comment