-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isReflection_of_mem_rightInvSeq (ω : List B) {t : W} (ht : t ∈ ris ω) :
    cs.IsReflection t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
induction' ω with i ω ih

Result:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : t ∈ cs.rightInvSeq []
⊢ cs.IsReflection t

case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ cs.rightInvSeq (i :: ω)
⊢ cs.IsReflection t

Proof state:
case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
exact ih mem

Result:
no goals

Proof state:
case cons.head
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

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
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
rcases ht with _ | ⟨_, mem⟩

Result:
case cons.head
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

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
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹

Tactic:
group

Result:
no goals

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ cs.rightInvSeq (i :: ω)
⊢ cs.IsReflection t

Tactic:
dsimp [rightInvSeq] at ht

Result:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
⊢ cs.IsReflection t

Proof state:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : t ∈ cs.rightInvSeq []
⊢ cs.IsReflection t

Tactic:
simp at ht

Result:
no goals