chore: Fin.castLE consistency + README version drift fix

[cameronfreer]

Summary

Small batched cleanup PR with two unrelated-but-trivial items:

1. Fin.castLE consistency — two open-coded fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt h⟩ inclusions are replaced with the mathlib spelling Fin.castLE h. The codebase already uses Fin.castLE in many places (Core.lean, the recently refactored Contractability.exists_perm_extending_strictMono from refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines) #18, and the new Core.exists_approxPerm from refactor: route Core.approxPerm through Equiv.Perm.exists_extending_pair (−31 lines) #20); these two sites had been missed.
2. README version drift fix — README.md:51 still claimed lean-toolchain was pinned to 4.27.0-rc1; the v4.30.0-rc2 bump (bump Lean to v4.30.0-rc2 + mathlib v4.30.0-rc2 #17) missed updating it. Rather than re-pin (and re-drift on the next bump), point at the file itself.

Net diff: 3 files, +7 / −13 (−6 lines).

What changed

Lean (proof-body-only, statements unchanged)

File	Site	Change
Exchangeability/Contractability.lean:470	contractable_of_exchangeable call site	let ι := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩ → let ι := Fin.castLE hmn. Existing simpa [ι] and simp [..., ι] calls work unchanged (still unfold the let).
Exchangeability/Util/FinsetHelpers.lean:32	filter_val_lt_card	Same let substitution. Inline hf_inj collapses from a 3-line proof to Fin.castLE_injective h. The Finset.image ext-step's simp only [f] is replaced by direct Fin.ext rfl / rintro ⟨j, rfl⟩.

Contractability.lean:408 was deliberately left alone — that let is inside a lemma statement (not the proof body), and per agreed scope this PR is proof-body-only churn. A statement-level cleanup pass can address it later if desired.

Docs

File	Before	After
README.md:51	(this project uses lean-toolchain pinned to 4.27.0-rc1)	(see lean-toolchain for the pinned version)

This makes the README impervious to future bump drift.

Verification

Check	Baseline (main = 18bf7ab)	This branch
lake build	clean (3531 jobs)	clean (3531 jobs)
Axioms (11 theorem decls)	standard only	standard only
Sorries (Exchangeability + ForMathlib)	0	0
Proof-file churn	—	2 files, +5 / −12
Docs churn	—	1 file, +1 / −1

Notes for review

• Statement-level Fin.castLE cleanup at Contractability.lean:408 is out of scope; it's inside a lemma statement.
• This concludes the targeted permutation-extension follow-up sequence (refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines) #18 → refactor: route Core.approxPerm through Equiv.Perm.exists_extending_pair (−31 lines) #20 → this). The next item in the broader follow-up menu is Kernel.IndepFun.comp and other PR chore: autoGolf proof bodies across 61 files (−841 lines) #16 safe-subset replacements.