-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem exists_leftDescent_of_ne_one {w : W} (hw : w ≠ 1) : ∃ i : B, cs.IsLeftDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
hw : cs.wordProd [] ≠ 1
h : [].length = cs.length (cs.wordProd [])
⊢ False

Tactic:
simp at hw

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
hw : w ≠ 1
⊢ ∃ i, cs.IsLeftDescent w i

Tactic:
rcases cs.exists_reduced_word w with ⟨ω, h, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hw : cs.wordProd ω ≠ 1
h : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ i, cs.IsLeftDescent (cs.wordProd ω) i

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length

Tactic:
calc
  ℓ (π ω') ≤ ω'.length                := cs.length_wordProd_le ω'
  _        < (i :: ω').length         := by simp

Result:
no goals

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hw : cs.wordProd ω ≠ 1
h : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ i, cs.IsLeftDescent (cs.wordProd ω) i

Tactic:
have h₁ : ω ≠ [] := by rintro rfl; simp at hw

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hw : cs.wordProd ω ≠ 1
h : ω.length = cs.length (cs.wordProd ω)
h₁ : ω ≠ []
⊢ ∃ i, cs.IsLeftDescent (cs.wordProd ω) i

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ cs.IsLeftDescent (cs.wordProd (i :: ω')) i

Tactic:
rw [IsLeftDescent, ← h, wordProd_cons, simple_mul_simple_cancel_left]

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ ω'.length < (i :: ω').length

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hw : cs.wordProd ω ≠ 1
h : ω.length = cs.length (cs.wordProd ω)
h₁ : ω ≠ []
⊢ ∃ i, cs.IsLeftDescent (cs.wordProd ω) i

Tactic:
rcases List.exists_cons_of_ne_nil h₁ with ⟨i, ω', rfl⟩

Result:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ ∃ i_1, cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hw : cs.wordProd ω ≠ 1
h : ω.length = cs.length (cs.wordProd ω)
⊢ ω ≠ []

Tactic:
rintro rfl

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
hw : cs.wordProd [] ≠ 1
h : [].length = cs.length (cs.wordProd [])
⊢ False

Proof state:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ ∃ i_1, cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1

Tactic:
use i

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
hw : cs.wordProd (i :: ω') ≠ 1
h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))
h₁ : i :: ω' ≠ []
⊢ cs.IsLeftDescent (cs.wordProd (i :: ω')) i