Lean4
/-- Shrink an injective function slicing a segment in the middle of the domain and removing
the corresponding elements in the codomain, hence maintaining the property that
one is a permutation of the other.
-/
protected def shrink {α : Type} [DecidableEq α] : InjectiveFunction α → List (InjectiveFunction α)
| ⟨_, h₀, h₁⟩ => do
let ⟨xs', ys', h₀, h₁⟩ ← InjectiveFunction.shrinkPerm ⟨_, _, h₀, h₁⟩
have h₃ : xs'.length ≤ ys'.length := le_of_eq (List.Perm.length_eq h₀)
have h₄ : ys'.length ≤ xs'.length := le_of_eq (List.Perm.length_eq h₀.symm)
pure
⟨(List.zip xs' ys').map Prod.toSigma, by
simp only [comp_def, List.map_fst_zip, List.map_snd_zip, *, Prod.fst_toSigma, Prod.snd_toSigma, List.map_map],
by simp only [comp_def, List.map_snd_zip, *, Prod.snd_toSigma, List.map_map]⟩
