English
For every x, the function permutations'Aux x is injective: if permutations'Aux x s = permutations'Aux x t, then s = t.
Русский
Для каждого x функция permutations'Aux x инъективна: если permutations'Aux x s = permutations'Aux x t, то s = t.
LaTeX
$$$\forall x,\, \operatorname{Function.Injective}(\operatorname{permutations'Aux} x)$$$
Lean4
theorem injective_permutations'Aux (x : α) : Function.Injective (permutations'Aux x) :=
by
intro s t h
apply insertIdx_injective s.length x
dsimp
have hl : s.length = t.length := by simpa using congr_arg length h
rw [← get_permutations'Aux s x s.length (by simp), ← get_permutations'Aux t x s.length (by simp [hl])]
simp only [get_eq_getElem, h, hl]