not_isReduced_alternatingWord — Mathlib

English

For certain alternating words of length m, if a certain condition on M holds, the word is not reduced.

Русский

Для некоторых чередующихся слов длины m при выполнении условия на M данное слово не является редуцированным.

LaTeX

$$$$ \\text{Not } cs.IsReduced(\\\\text{alternatingWord } i i' m) $$$$

Lean4

theorem not_isReduced_alternatingWord (i i' : B) {m : ℕ} (hM : M i i' ≠ 0) (hm : m > M i i') :
    ¬cs.IsReduced (alternatingWord i i' m) := by
  induction hm with
  | refl => -- Base case; m = M i i' + 1

    suffices h : ℓ(π(alternatingWord i i' (M i i' + 1))) < M i i' + 1
      by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      cutsat
    have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
    rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
    have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by omega
    rw [this]
    calc
      ℓ(π(alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := (cs.length_wordProd_le _)
      _ = M i i' - 1 := (length_alternatingWord _ _ _)
      _ ≤ M i i' := (Nat.sub_le _ _)
      _ < M i i' + 1 := Nat.lt_succ_self _
  | step m ih => -- Inductive step

    contrapose! ih
    rw [alternatingWord_succ'] at ih
    apply IsReduced.drop (j := 1)at ih
    simpa using ih

Похожие утверждения