English
Characterizes when l' belongs to the second projection of permutationsAux2 t ts [] ys with a given insertion l ++ ·.
Русский
Характеризуется принадлежность l' ко второй проекции permutationsAux2 для заданной вставки l ++ ·.
LaTeX
$$$\forall {t},{ts},{ys}:{l'\in (permutationsAux2\ t\ ts\ []\ ys (l ++ \cdot)).2} \iff \exists l_1 l_2, l_2 \neq \emptyset \\, ys = l_1 ++ l_2 \\, l' = l_1 ++ l \!+\! t :: l_2 ++ ts$$$
Lean4
theorem mem_permutationsAux2 {t : α} {ts : List α} {ys : List α} {l l' : List α} :
l' ∈ (permutationsAux2 t ts [] ys (l ++ ·)).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts :=
by
induction ys generalizing l with
| nil => simp +contextual
| cons y ys ih => ?_
rw [permutationsAux2_snd_cons, show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp, mem_cons, ih]
constructor
· rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
· exact ⟨[], y :: ys, by simp⟩
· exact ⟨y :: l₁, l₂, l0, by simp⟩
· rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
· simp [ye]
· simp only [cons_append] at ye
rcases ye with ⟨rfl, rfl⟩
exact Or.inr ⟨l₁, l₂, l0, by simp⟩
