feat: add linter

[markusdemedeiros]

Description

Adds the batteries linter to the project. This should not be merged until the linter is fully configured and the code passes lint.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[Kaptch]

Is it possible to configure the linter to ignore some files, so that we gradually change them to meet the standards? I am bit worried of bulk changes, especially if it is not only formatting.

[Kaptch]

Seems it is possible. Then I would propose to ignore existing files in the very beginning, require passing linter from future PRs, and add chore to make old files pass the linter gradually, similar what is done with Rocq annotations.

[markusdemedeiros]

That is a good idea! We should still discuss the linting rules we want to follow beforehand, but I agree with a gradual rollout.