English
If ω is reduced, then ris ω contains no duplicates.
Русский
Если ω редукрировано, то ris ω состоит без повторов элементов.
LaTeX
$$0$$
Lean4
theorem nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List.Nodup (ris ω) :=
by
apply List.nodup_iff_getElem?_ne_getElem?.mpr
intro j j' j_lt_j' j'_lt_length (dup : (rightInvSeq cs ω)[j]? = (rightInvSeq cs ω)[j']?)
show False
replace j'_lt_length : j' < List.length ω := by simpa using j'_lt_length
rw [getElem?_eq_getElem (by simp; cutsat), getElem?_eq_getElem (by simp; cutsat)] at dup
apply Option.some_injective at dup
rw [← getD_eq_getElem _ 1, ← getD_eq_getElem _ 1] at dup
set! t := (ris ω).getD j 1 with h₁
set! t' := (ris(ω.eraseIdx j)).getD (j' - 1) 1 with h₂
have h₃ : t' = (ris ω).getD j' 1 :=
by
rw [h₂, cs.getD_rightInvSeq, cs.getD_rightInvSeq, (Nat.sub_add_cancel (by cutsat) : j' - 1 + 1 = j'),
eraseIdx_eq_take_drop_succ, drop_append, drop_of_length_le (by simp [j_lt_j'.le]), length_take, drop_drop,
nil_append, min_eq_left_of_lt (j_lt_j'.trans j'_lt_length), Nat.add_comm, ← add_assoc,
Nat.sub_add_cancel (by cutsat), mul_left_inj, mul_right_inj]
congr 2
show (List.take j ω ++ List.drop (j + 1) ω)[j' - 1]? = ω[j']?
rw [getElem?_append_right (by simp [Nat.le_sub_one_of_lt j_lt_j']), getElem?_drop]
grind
have h₄ : t * t' = 1 := by
rw [h₁, h₃, dup]
exact cs.getD_rightInvSeq_mul_self _ _
have h₅ :=
calc
π ω = π ω * t * t' := by rw [mul_assoc, h₄]; group
_ = (π(ω.eraseIdx j)) * t' := (congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _))
_ = π((ω.eraseIdx j).eraseIdx (j' - 1)) := cs.wordProd_mul_getD_rightInvSeq _ _
have h₆ :=
calc
ω.length = ℓ(π ω) := rω.symm
_ = ℓ(π((ω.eraseIdx j).eraseIdx (j' - 1))) := (congrArg cs.length h₅)
_ ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length := cs.length_wordProd_le _
grind
