English
If l1 ∈ permutations l2, then l1 is a permutation of l2. More generally, if l1 ∈ permutations l2, then l1 ~ l2.
Русский
Если l1 принадлежит permutations l2, то l1 является перестановкой l2. В частности, l1 ∈ permutations l2 → l1 ~ l2.
LaTeX
$$$$l_1 \in permutations(l_2) \rightarrow l_1 \sim l_2$$$$
Lean4
theorem perm_of_mem_permutations {l₁ l₂ : List α} (h : l₁ ∈ permutations l₂) : l₁ ~ l₂ :=
(eq_or_mem_of_mem_cons h).elim (fun e => e ▸ Perm.refl _) fun m => append_nil l₂ ▸ perm_of_mem_permutationsAux m