English
If f is in permsOfList(l), then for every x with f(x) ≠ x, we have x ∈ l.
Русский
Если f ∈ permsOfList(l), то для каждого x с f(x) ≠ x имеем x ∈ l.
LaTeX
$$$f \\in \\mathrm{permsOfList}(l) \\Rightarrow \\forall x, f(x) \\neq x \\Rightarrow x \\in l$$$
Lean4
theorem mem_of_mem_permsOfList : ∀ {l : List α} {f : Perm α}, f ∈ permsOfList l → {x : α} → f x ≠ x → x ∈ l
| [], f, h, heq_iff_eq => by
have : f = 1 := by simpa [permsOfList] using h
rw [this]; simp
| a :: l, f, h, x =>
(mem_append.1 h).elim (fun h hx => mem_cons_of_mem _ (mem_of_mem_permsOfList h hx)) fun h hx =>
let ⟨y, hy, hy'⟩ := List.mem_flatMap.1 h
let ⟨g, hg₁, hg₂⟩ := List.mem_map.1 hy'
if hxa : x = a then by simp [hxa]
else
if hxy : x = y then mem_cons_of_mem _ <| by rwa [hxy]
else
mem_cons_of_mem a <|
mem_of_mem_permsOfList hg₁ <|
by
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]
split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
