-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isLeftInversion_of_mem_leftInvSeq {ω : List B} (hω : cs.IsReduced ω) {t : W}
    (ht : t ∈ lis ω) : cs.IsLeftInversion (π ω) t

Proof state:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length ((cs.leftInvSeq ω)[j] * cs.wordProd ω) < cs.length (cs.wordProd ω)

Tactic:
rw [← List.getD_eq_getElem _ 1 hj, getD_leftInvSeq_mul_wordProd]

Result:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < ω.length

Tactic:
rw [← List.length_eraseIdx_add_one hj]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Proof state:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Tactic:
rw [cs.length_leftInvSeq] at hj

Result:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsLeftInversion (cs.wordProd ω) t

Tactic:
constructor

Result:
case left
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)

Proof state:
case left
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

Tactic:
exact cs.isReflection_of_mem_leftInvSeq ω ht

Result:
no goals

Proof state:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Tactic:
calc
  ℓ (π (ω.eraseIdx j))
  _ ≤ (ω.eraseIdx j).length   := cs.length_wordProd_le _
  _ < ω.length                := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
  _ = ℓ (π ω)                 := hω.symm

Result:
no goals

Proof state:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)

Tactic:
obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht

Result:
case right.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length ((cs.leftInvSeq ω)[j] * cs.wordProd ω) < cs.length (cs.wordProd ω)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Tactic:
exact lt_add_one _

Result:
no goals