-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_simple_ne (w : W) (i : B) : ℓ (w * s i) ≠ ℓ w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
⊢ False

Tactic:
rcases Nat.mod_two_eq_zero_or_one (ℓ w) with even | odd

Result:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
even : cs.length w % 2 = 0
⊢ False

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
odd : cs.length w % 2 = 1
⊢ False

Proof state:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : 1 = 0
odd : cs.length w % 2 = 1
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False

Tactic:
rw [eq, length_simple] at length_mod_two

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
⊢ False

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
⊢ False

Tactic:
have length_mod_two := cs.length_mul_mod_two w (s i)

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) ≠ cs.length w

Tactic:
intro eq

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
⊢ False

Proof state:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
even : cs.length w % 2 = 0
⊢ False

Tactic:
rw [even, Nat.succ_mod_two_eq_one_iff.mpr even] at length_mod_two

Result:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : 0 = 1
even : cs.length w % 2 = 0
⊢ False

Proof state:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : 0 = 1
even : cs.length w % 2 = 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
odd : cs.length w % 2 = 1
⊢ False

Tactic:
rw [odd, Nat.succ_mod_two_eq_zero_iff.mpr odd] at length_mod_two

Result:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : 1 = 0
odd : cs.length w % 2 = 1
⊢ False