English
The head of the i-th equivPair is determined by whether there exists a nonempty representation of w whose first coordinate equals i; if such exists, the head is that second component; otherwise it is 1.
Русский
Голова пары equivPair(i,w) определяется наличием непустого представления w c первой координатой i; если такое существует, голова равна второй компоненте этого элемента, иначе равна 1.
LaTeX
$$$$ (equivPair(i,w)).head = \\begin{cases} m & \\text{if } \\exists h:\\ w.toList \\neq [] \\, \\text{ и } (w.toList.head h).1 = i \\text{ и соответствующий элемент имеет второй компонент } m, \\\\ 1 & \\text{в противном случае}. \\end{cases} $$$$
Lean4
theorem mem_of_mem_equivPair_tail {i j : ι} {w : Word M} (m : M i) :
(⟨i, m⟩ ∈ (equivPair j w).tail.toList) → ⟨i, m⟩ ∈ w.toList :=
by
rw [mem_equivPair_tail_iff]
rintro (h | h)
· exact List.mem_of_mem_tail h
· revert h; cases w.toList <;> simp +contextual
