Documentation for Lean Version Upgrade

Since Yatima is not currently in active development, it would be great to have documentation on how to upgrade the Lean version of the current project so that user may be able to still use compiler as the `lake upgrade` command suggested after `lake run setup` does not seem to bump everything properly.

Currently after pulling `main` and running `lake run setup` produces
```
warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'LSpec' of 'Yatima' not in manifest, use `lake update` to update
```

while running `lake update` produces

```
warning: improperly formatted manifest: incompatible manifest version `4`
error: ./lake-packages/YatimaStdLib/lakefile.lean:14:15: error: invalid field 'oleanDir', the environment does not contain 'Lake.Package.oleanDir'
pkg
has type
Package
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:33: error: unknown identifier 'defaultLibDir'
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:57: error: application type mismatch
List.cons job
argument
job
has type
CustomData (Package.name pkg, `importTarget) : Type
but is expected to have type
BuildJob FilePath : Type
error: ./lake-packages/YatimaStdLib/lakefile.lean: package configuration has errors
```

Might be an issue with Lean4 Arch (AUR) package, however.

Start by reproducing the reported results of `lake run setup` and `lake update` after pulling `main`, then inspect `lake-packages/YatimaStdLib/lakefile.lean` and the project’s existing setup documentation. Done means the supported Lean version upgrade procedure is documented clearly enough for users to avoid or understand the manifest and Lake API errors.

Written by the indexing model from the issue text.