English
Characterizes when a letter (i,m) appears in the tail of the equivPair(j,w); it appears either in the tail of w, or (i ≠ j and it appears as the head of w when appropriate, with a witness from the nonempty list).
Русский
Характеризуется, когда пара (i,m) входит в хвост пары equivPair(j,w); либо она входит в хвост w, либо (i ≠ j и она является головой списка w при наличии ненулевого списка, с существованием свидетеля).
LaTeX
$$$$ (i,m) \\in (equivPair(j,w)).tail = tail.(equivPair(j,w)) \\Rightarrow (i,m) \\in w.tail \\ \\lor\\ (i \\neq j \\land \\exists h:\\ w.toList \\neq []\\, \\whead h = \\langle i,m\\rangle) $$$$
Lean4
theorem mem_equivPair_tail_iff {i j : ι} {w : Word M} (m : M i) :
(⟨i, m⟩ ∈ (equivPair j w).tail.toList) ↔
⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ h : w.toList ≠ [], w.toList.head h = ⟨i, m⟩ :=
by
simp only [equivPair, equivPairAux, ne_eq, Equiv.coe_fn_mk]
induction w using consRecOn with
| empty => simp
| cons k g tail h1 h2 ih =>
simp only [consRecOn_cons]
split_ifs with h
· subst k
by_cases hij : j = i <;> simp_all
· by_cases hik : i = k
· subst i; simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]
· simp [hik, Ne.symm hik]
