English
Every nonempty Word M can be realized as the image of some NeWord M i j; i.e., for any nonempty Word, there exist indices i, j and a NeWord w' with w'.toWord = w.
Русский
Любое ненулевое Word можно получить как образ некоторого NeWord: существует i, j и w' such that w'.toWord = w.
LaTeX
$$$$\\forall w:\\text{Word } M,\\ w \\neq \\emptyset\\Rightarrow \\exists i\\exists j\\exists w': NeWord M i j, w'.toWord = w.$$$$
Lean4
/-- Every nonempty `Word M` can be constructed as a `NeWord M i j` -/
theorem of_word (w : Word M) (h : w ≠ empty) : ∃ (i j : _) (w' : NeWord M i j), w'.toWord = w :=
by
suffices ∃ (i j : _) (w' : NeWord M i j), w'.toWord.toList = w.toList
by
rcases this with ⟨i, j, w, h⟩
refine ⟨i, j, w, ?_⟩
ext
rw [h]
obtain ⟨l, hnot1, hchain⟩ := w
induction l with
| nil => contradiction
| cons x l hi =>
rw [List.forall_mem_cons] at hnot1
rcases l with - | ⟨y, l⟩
· refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
simp [toWord]
· rw [List.isChain_cons_cons] at hchain
specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
obtain ⟨i, j, w', hw' : w'.toList = y :: l⟩ := hi
obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
simpa [toWord] using hw'
