-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_simple (w : W) (i : B) :
    ℓ (w * s i) = ℓ w + 1 ∨ ℓ (w * s i) + 1 = ℓ w

Proof state:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
length_le : cs.length (w * cs.simple i) ≤ cs.length w + cs.length (cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
simp only [length_simple] at length_le

Result:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
length_le : cs.length (w * cs.simple i) ≤ cs.length w + 1
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Proof state:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
have length_le := cs.length_mul_le w (s i)

Result:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
length_le : cs.length (w * cs.simple i) ≤ cs.length w + cs.length (cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Proof state:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
length_ge : cs.length w - cs.length (cs.simple i) ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
simp only [length_simple, tsub_le_iff_right] at length_ge

Result:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
length_ge : cs.length w ≤ cs.length (w * cs.simple i) + 1
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

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
lt : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
right

Result:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Proof state:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
have length_ge := cs.length_mul_ge_length_sub_length w (s i)

Result:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
length_ge : cs.length w - cs.length (cs.simple i) ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Proof state:
case inl.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
lt : cs.length (w * cs.simple i) < cs.length w
length_ge : cs.length w ≤ cs.length (w * cs.simple i) + 1
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
omega

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
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
rcases Nat.lt_or_gt_of_ne (cs.length_mul_simple_ne w i) with lt | gt

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
lt : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Proof state:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
length_le : cs.length (w * cs.simple i) ≤ cs.length w + 1
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
omega

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
gt : cs.length (w * cs.simple i) > cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
left

Result:
case inr.h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
gt : cs.length (w * cs.simple i) > cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1