English
If l ∈ permutationsAux ts is, then l is a permutation of ts ++ is. Precisely, l ∈ permutationsAux ts is → l ~ ts ++ is.
Русский
Если l ∈ permutationsAux ts is, то l является перестановкой ts ++ is. То есть l ∈ permutationsAux ts is → l ~ ts ++ is.
LaTeX
$$$$l \in permutationsAux\ ts\ is \rightarrow l \sim ts ++ is$$$$
Lean4
theorem perm_of_mem_permutationsAux : ∀ {ts is l : List α}, l ∈ permutationsAux ts is → l ~ ts ++ is :=
by
show ∀ (ts is l : List α), l ∈ permutationsAux ts is → l ~ ts ++ is
refine permutationsAux.rec (by simp) ?_
introv IH1 IH2 m
rw [permutationsAux_cons, permutations, mem_foldr_permutationsAux2] at m
rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)
· exact (IH1 _ m).trans perm_middle
· have p : l₁ ++ l₂ ~ is := by
simp only [mem_cons] at m
rcases m with e | m
· simp [e]
exact is.append_nil ▸ IH2 _ m
exact ((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)
