refactor(LocallyNameless): Extract depth into a dedicated module

[lengyijun]

Make LcAt.lean cleaner

[chenson2018]

ci failed, which is out of my scope

No, this particular failure falls to the PR author. As the error message indicates you should run lake exe mk_all to update Cslib.lean, which is required because you were adding a new module.

[lengyijun]

ci failed, which is out of my scope

No, this particular failure falls to the PR author. As the error message indicates you should run lake exe mk_all to update Cslib.lean, which is required because you were adding a new module.

Fixed, thx