English
For ts is l, if l ~ is ++ ts then either l = is' ++ ts for some is' with is' ~ is, or l ∈ permutationsAux ts is.
Русский
Для ts, is, l: если l ~ is ++ ts, то либо существует is' такое что l = is' ++ ts и is' ~ is, либо l ∈ permutationsAux ts is.
LaTeX
$$$$\forall \text{ts,is,l},\ l \sim is ++ ts \rightarrow (\exists is' , is' \sim is \land l = is' ++ ts) \lor l \in permutationsAux ts is$$$$
Lean4
theorem mem_permutationsAux_of_perm :
∀ {ts is l : List α}, l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is :=
by
show ∀ (ts is l : List α), l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is
refine permutationsAux.rec (by simp) ?_
intro t ts is IH1 IH2 l p
rw [permutationsAux_cons, mem_foldr_permutationsAux2]
rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)
· clear p
subst e
rcases append_of_mem (p'.symm.subset mem_cons_self) with ⟨l₁, l₂, e⟩
subst is'
have p := (perm_middle.symm.trans p').cons_inv
rcases l₂ with - | ⟨a, l₂'⟩
· exact Or.inl ⟨l₁, by simpa using p⟩
· exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)
· exact Or.inr (Or.inl m)
