English
The construction rcons : Pair M i → Word M is injective; distinct pairs yield distinct words.
Русский
Окончание rcons : Pair M i → Word M инъективно: различные пары дают разные слова.
LaTeX
$$$\\operatorname{Injective}(\\mathrm{rcons})$$$
Lean4
theorem rcons_inj {i} : Function.Injective (rcons : Pair M i → Word M) :=
by
rintro ⟨m, w, h⟩ ⟨m', w', h'⟩ he
by_cases hm : m = 1 <;> by_cases hm' : m' = 1
· simp only [rcons, dif_pos hm, dif_pos hm'] at he
simp_all
· exfalso
simp only [rcons, dif_pos hm, dif_neg hm'] at he
rw [he] at h
exact h rfl
· exfalso
simp only [rcons, dif_pos hm', dif_neg hm] at he
rw [← he] at h'
exact h' rfl
· have : m = m' ∧ w.toList = w'.toList := by
simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk, heq_iff_eq,
← Subtype.ext_iff] using he
rcases this with ⟨rfl, h⟩
congr
exact Word.ext h
