Tracking issue: indentation linter enhancements

#27473 adds a syntax linter for indentation of declarations. This issue tracks further checks within the same framework.

Each of these is fairly conservative, so hopefully has almost no false positives.

• the first line of the declaration (i.e, the lemma, theorem statement, etc.) is not indented (#27473 implements this already, right?)
• if there are further lines, at least one of these is indented by four spaces
  (in other words, indenting everything by six spaces should give an error)
  We don't check more strictly to give maximum flexibility with line breaks.
• checking for lines indented by an odd number of spaces can happen in the future

In a proof body,

• every line is indented by at least two spaces
  (stronger version: proofs of a have, suffices, etc. are indented by at least two spaces more than the have/suffices itself)
• some line is indented by exactly two spaces
  i.e., indenting everything by four spaces is caught
  Lean will check most of the remaining consistency issues: for instance, a proof

  simp
    exact foo
  

  (which is meant to be equivalent to simp; exact foo) will already error.

Another check, similar but conceptually independent of this PR: if there is just a second line for the statement and the proof is longer than X (20 characters? 30 characters); it should be on a separate line

instance of_hasKernel_of_hasCokernel [HasKernel S.g] [HasCokernel (kernel.lift S.g S.f S.zero)] :
    S.HasLeftHomology := HasLeftHomology.mk' (LeftHomologyData.ofHasKernelOfHasCokernel S)

should be flagged

Another check: where (in a structure definition) should be on a separate line ---

noncomputable instance colimitOne : One (M.{v, u} F) where one := M.mk F ⟨IsFiltered.nonempty.some,1⟩

should be linted

Start with the syntax linter framework introduced by #27473 and review how its existing indentation check handles declarations. Implement and validate the listed declaration, proof-body, long-statement, and where-layout checks, including the proposed thresholds and examples; done means the intended violations are flagged without the conservative cases producing false positives.