fix: update to work with newer Lean toolchain

[tydeu]

Thanks for the contribution! The test suite is failing because the attribute names in the tests' lakefiles were not similarly updated.