-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isReduced_alternatingWord (i i' : B) {m : ℕ} (hM : M i i' ≠ 0) (hm : m > M i i') :
    ¬cs.IsReduced (alternatingWord i i' m)

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1

Tactic:
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 _

Result:
no goals

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1

Tactic:
rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by omega

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1

Tactic:
omega

Result:
no goals

Proof state:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced ((if Even m then i' else i) :: alternatingWord i i' m)
⊢ cs.IsReduced (alternatingWord i i' m)

Tactic:
apply IsReduced.drop (j := 1) at ih

Result:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced (drop 1 ((if Even m then i' else i) :: alternatingWord i i' m))
⊢ cs.IsReduced (alternatingWord i i' m)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ M.M i i' + 1 ≤ M.M i i' * 2

Tactic:
linarith [Nat.one_le_iff_ne_zero.mpr hM]

Result:
no goals

Proof state:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : ¬cs.IsReduced (alternatingWord i i' m)
⊢ ¬cs.IsReduced (alternatingWord i i' m.succ)

Tactic:
contrapose! ih

Result:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced (alternatingWord i i' m.succ)
⊢ cs.IsReduced (alternatingWord i i' m)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1

Tactic:
omega

Result:
no goals

Proof state:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced (drop 1 ((if Even m then i' else i) :: alternatingWord i i' m))
⊢ cs.IsReduced (alternatingWord i i' m)

Tactic:
simpa using ih

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
hm : m > M.M i i'
⊢ ¬cs.IsReduced (alternatingWord i i' m)

Tactic:
induction' hm with m _ ih

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : ¬cs.IsReduced (alternatingWord i i' m)
⊢ ¬cs.IsReduced (alternatingWord i i' m.succ)

Proof state:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
rw [this]

Result:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
unfold IsReduced

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i').succ)) = (alternatingWord i i' (M.M i i').succ).length

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i').succ)) = (alternatingWord i i' (M.M i i').succ).length

Tactic:
rw [Nat.succ_eq_add_one, length_alternatingWord]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1

Proof state:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced (alternatingWord i i' m.succ)
⊢ cs.IsReduced (alternatingWord i i' m)

Tactic:
rw [alternatingWord_succ'] at ih

Result:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝ : ℕ
hM : M.M i i' ≠ 0
m : ℕ
a✝ : (M.M i i').succ.le m
ih : cs.IsReduced ((if Even m then i' else i) :: alternatingWord i i' m)
⊢ cs.IsReduced (alternatingWord i i' m)