refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines)

[cameronfreer]

Summary

First in the post-bump series of targeted mathlib-refactor PRs. Replaces the local 58-line proof of exists_perm_extending_strictMono in Contractability.lean with a 13-line wrapper around mathlib's Equiv.Perm.exists_extending_pair (landed via mathlib #34599) plus Fin.castLE / Fin.castLE_injective for the initial-segment inclusion, and updates two stale docstrings that still described the old subtype-equivalence construction.

Net diff: 1 file, +15 / −61 (−46 lines), across two commits.

Why now

The exchangeability-papers#1 camera-ready revisions explicitly flagged the local permutation-extension code as a candidate for refactoring against existing mathlib infrastructure, and mathlib #34599 landed exactly this API. With the toolchain now at v4.30.0-rc2 (PR #17), Equiv.Perm.exists_extending_pair is directly available.

Commits

Commit	Scope
07695a91 — refactor: thin exists_perm_extending_strictMono via mathlib API	Replaces the 58-line proof body with a 13-line wrapper. Statement, signature, and the single call site (contractable_of_exchangeable) are unchanged.
c6d3cb95 — docs: update Contractability docstrings to match refactored proof	Module header (lines 55–58) and the lemma's own docstring no longer describe the deleted subtype-equivalence construction; they now point at Equiv.Perm.exists_extending_pair.

What the new proof body looks like

let f : Fin m → Fin n := Fin.castLE hmn
let g : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
have hf : Function.Injective f := Fin.castLE_injective hmn
have hg : Function.Injective g := fun i j hij =>
  hk_mono.injective (Fin.mk.inj hij)
obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g hf hg
exact ⟨σ, fun i => congrArg Fin.val (hσ i)⟩

Verification

Check	Baseline (main)	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	—	1 file, +15 / −61

Out of scope (planned follow-up PR)

The refactor exposes some spillover cleanup that does not belong here:

• Three open-coded fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩ inclusions that could become Fin.castLE hmn (Contractability.lean:410, :472, Util/FinsetHelpers.lean:32).
• Core.approxPerm and its companion approxEquiv use the same Equiv.extendSubtype pattern (~32 lines of approxEquiv machinery) and can collapse via the same Equiv.Perm.exists_extending_pair route, saving ~35 lines.

Both will land as a single follow-up PR after this merges.

Notes for review

• The ForMathlib/Combinatorics/PermutationExtension.lean file proposed in PR refactor: Extract general-purpose lemmas to ForMathlib for upstream contribution #13 was never merged to main, so nothing to delete there.
• Statement simplification (restating the conclusion as σ (Fin.castLE hmn i) = ⟨k i, hk_bound i⟩ to match the mathlib API shape directly) is deferred — it would broaden the PR semantically.