English
Let l be a finite list of permutations of α and x an element of α. If x is moved by the product l.prod, then there exists a permutation f in l such that x is moved by f.
Русский
Пусть l — конечный список перестановок на α, и x ∈ α. Если x переставляется произведением l.prod, то существует перестановка f из l такая, что x переставляется f.
LaTeX
$$$\text{For a finite list } l \text{ of permutations of } \alpha \text{ and } x \in \alpha,\quad x \in (l_{\operatorname{prod}}).\operatorname{support} \Rightarrow \exists f \in l,\ x \in f.\operatorname{support}. $$$
Lean4
theorem exists_mem_support_of_mem_support_prod {l : List (Perm α)} {x : α} (hx : x ∈ l.prod.support) :
∃ f : Perm α, f ∈ l ∧ x ∈ f.support := by
contrapose! hx
simp_rw [mem_support, not_not] at hx ⊢
induction l with
| nil => rfl
| cons f l ih =>
rw [List.prod_cons, mul_apply, ih, hx]
· simp only [List.mem_cons, true_or]
grind
