[Merged by Bors] - feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair

Mathlib/GroupTheory/Perm/Fin.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser, Yi Yuan
 -/
 module
 
+public import Mathlib.Data.Fin.Pigeonhole
 public import Mathlib.GroupTheory.Perm.Cycle.Type
 public import Mathlib.GroupTheory.Perm.Option
 public import Mathlib.Logic.Equiv.Fin.Rotate
@@ -523,3 +524,16 @@ theorem Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod {R : Type*} [CommRing R]
   apply Finset.prod_comm' (by simp)
 
 end Sign
+
+section Extension
+
+/-! ### Extension of injective functions to permutations -/
+
+/-- Injective `k : Fin m → Fin n` extends to a permutation agreeing with `k` on `Fin.castLE`. -/
+theorem Equiv.Perm.exists_extending_injective {m n : ℕ} (k : Fin m → Fin n)
+    (hk : Function.Injective k) :
+    ∃ σ : Perm (Fin n), ∀ i : Fin m, σ (Fin.castLE (Fin.le_of_injective k hk) i) = k i :=
+  let e := (Fin.castLEquiv (Fin.le_of_injective k hk)).symm.trans (Equiv.ofInjective k hk)
+  ⟨e.extendSubtype, fun i => Equiv.extendSubtype_apply_of_mem e _ i.isLt⟩
+
+end Extension