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

* refactor: thin exists_perm_extending_strictMono via mathlib API

Reduces the local proof from 58 lines of hand-built subtype
equivalences + `Equiv.extendSubtype` to a 13-line wrapper around
`Equiv.Perm.exists_extending_pair` (landed in mathlib via PR
#34599) plus `Fin.castLE` / `Fin.castLE_injective` for the
initial-segment inclusion.

Statement is unchanged; only the proof body is touched. The
single call site (`contractable_of_exchangeable`) is unaffected.

- Exchangeability/Contractability.lean: -44 net lines.

* docs: update Contractability docstrings to match refactored proof

Two docstrings still described the old subtype-equivalence
construction, which no longer matches the refactored proof body.

- Module header (lines 55-58): "uses `Equiv.extendSubtype` to
  extend a bijection between subtypes" -> "thin wrapper around
  mathlib's `Equiv.Perm.exists_extending_pair`".
- `exists_perm_extending_strictMono` docstring: 4-step
  "Construction outline" describing domain/codomain partition +
  manual `extendSubtype` -> short note pointing at
  `Equiv.Perm.exists_extending_pair` with the choice of `f` and
  `g`.

Statement, signature, and behavior are unchanged.

Author: cameronfreer

Exchangeability/Contractability.lean

@@ -54,8 +54,8 @@ extension argument.
 
 The key technical challenge is constructing permutations that extend strictly monotone
 selections. Given `k : Fin m → ℕ` with `k(0) < k(1) < ... < k(m-1)`, we construct
-a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for `i < m`. This uses
-`Equiv.extendSubtype` to extend a bijection between subtypes to a full permutation.
+a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for `i < m`. This is a thin
+wrapper around mathlib's `Equiv.Perm.exists_extending_pair`.
 
 ## References
 
@@ -301,11 +301,9 @@ as the image of the first `m` positions. Since `k` is strictly increasing, it's
 injective, so its image has cardinality `m`. We can extend this to a full
 permutation by arbitrarily pairing up the remaining elements.
 
-**Construction outline:**
-1. **Domain partition:** `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n`
-2. **Codomain partition:** `{k(0),...,k(m-1)}` ∪ `complement` = `Fin n`
-3. Map first `m` positions to `k`-values: `σ(i) = k(i)` for `i < m`
-4. Extend arbitrarily to remaining positions using `Equiv.extendSubtype`
+**Construction:** Thin wrapper around mathlib's `Equiv.Perm.exists_extending_pair`,
+applied to `f = Fin.castLE hmn` (initial-segment inclusion) and
+`g i = ⟨k i, hk_bound i⟩` (strictly monotone embedding via `k`).
 
 This is the key combinatorial lemma enabling `contractable_of_exchangeable`:
 any strictly increasing subsequence can be realized via a permutation.
@@ -314,60 +312,16 @@ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ)
     (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) :
     ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m),
       (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by
-  classical
-  -- Embed `Fin m` into `Fin n` via the initial segment.
-  let ι : Fin m → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩
-  let p : Fin n → Prop := fun x => x.val < m
-  let q : Fin n → Prop := fun x => ∃ i : Fin m, x = ⟨k i, hk_bound i⟩
-  have hι_mem : ∀ i : Fin m, p (ι i) := fun i => i.isLt
-  let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
-  have hk_mem : ∀ i : Fin m, q (kFin i) := fun i => ⟨i, rfl⟩
-  haveI : DecidablePred p := fun x => inferInstance
-  haveI : DecidablePred q := fun x => inferInstance
-  -- Equivalence between the first `m` coordinates and `Fin m`.
-  let e_dom : {x : Fin n // p x} ≃ Fin m :=
-    { toFun := fun x => ⟨x.1.val, x.2⟩
-      , invFun := fun i => ⟨ι i, by
-          dsimp [p, ι]
-          exact i.isLt⟩
-      , left_inv := by
-          rintro ⟨x, hx⟩
-          ext; simp [ι]
-      , right_inv := by
-          intro i
-          cases i with
-          | mk i hi =>
-            simp [ι] }
-  -- Equivalence between the image of `k` and `Fin m`.
-  -- For injectivity of k, we use that it's strictly monotone
-  have hk_inj : Function.Injective kFin :=
-    fun i j hij => hk_mono.injective (Fin.ext_iff.mp hij)
-  let e_cod : Fin m ≃ {x : Fin n // q x} :=
-    { toFun := fun i => ⟨kFin i, hk_mem i⟩
-      , invFun := fun y => Classical.choose y.2
-      , left_inv := by
-          intro i
-          have h_spec := Classical.choose_spec (hk_mem i)
-          have : k (Classical.choose (hk_mem i)) = k i := by
-            simpa [kFin] using (Fin.ext_iff.mp h_spec).symm
-          exact hk_mono.injective this
-      , right_inv := by
-          rintro ⟨y, hy⟩
-          apply Subtype.ext
-          simp only [kFin]
-          exact (Classical.choose_spec hy).symm }
-  -- Equivalence between the subtypes describing the first `m` coordinates and the image of `k`.
-  let e : {x : Fin n // p x} ≃ {x : Fin n // q x} := e_dom.trans e_cod
-  -- Extend this equivalence to a permutation of `Fin n`.
-  let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype e
-  have hσ_apply : ∀ i : Fin m, σ (ι i) = kFin i := by
-    intro i
-    have h_apply := Equiv.extendSubtype_apply_of_mem (e:=e) (x:=ι i) (hι_mem i)
-    dsimp [σ, e, Equiv.trans, e_dom, e_cod, ι, Fin.castLEEmb, kFin] at h_apply
-    simpa using h_apply
-  refine ⟨σ, fun i => ?_⟩
-  have hσ_val : (σ (ι i)).val = k i := by simpa [kFin] using congrArg Fin.val (hσ_apply i)
-  simpa [ι] using hσ_val
+  -- Wrap mathlib's `Equiv.Perm.exists_extending_pair`: given injective `f g : Fin m → Fin n`,
+  -- there is a permutation of `Fin n` sending `f` to `g`. Take `f` = initial-segment inclusion
+  -- and `g` = the strictly monotone embedding via `k`.
+  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)⟩
 
 /- Helper: relabeling coordinates by a finite permutation is measurable as a map
 from (Fin n → α) to itself (with product σ-algebra). -/