awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < (cs.rightInvSeq ω).length
cs₁ :
  ∀
    (dup :
      getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
        getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'),
    False
⊢ getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ≠
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'

Tactic:
(dup : (rightInvSeq cs ω)[j]? = (rightInvSeq cs ω)[j']?)
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < (cs.rightInvSeq ω).length
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
⊢ j' < ω.length

Tactic:
simpa using j'_lt_length
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < (cs.rightInvSeq ω).length
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
⊢ j' < ω.length

Tactic:
replace j'_lt_length : j' < List.length ω := by simpa using j'_lt_length
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
j'_lt_length : j' < ω.length
simp : j < ω.length
⊢ j < (cs.rightInvSeq ω).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
j'_lt_length : j' < ω.length
⊢ j < ω.length

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯) =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
simp : j' < ω.length
⊢ j' < (cs.rightInvSeq ω).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯) =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
⊢ j' < ω.length

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
j'_lt_length : j' < ω.length
⊢ some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯) =
    some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯)

Tactic:
rw [getElem?_eq_getElem (by simp; lia), getElem?_eq_getElem (by simp; lia)] at dup

Premises used: List.getElem?_eq_getElem
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯) =
    some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯)
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯ =
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯

Tactic:
apply Option.some_injective at dup

Premises used: Option.some_injective
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯ =
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯
⊢ (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1

Tactic:
rw [← getD_eq_getElem _ 1, ← getD_eq_getElem _ 1] at dup

Premises used: List.getD_eq_getElem, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
⊢ let t := (cs.rightInvSeq ω).getD j 1;
  t = (cs.rightInvSeq ω).getD j 1

Tactic:
set! t := (ris ω).getD j 1 with h₁
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
⊢ let t' := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1;
  t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1

Tactic:
set! t' := (ris (ω.eraseIdx j)).getD (j' - 1) 1 with h₂
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
⊢ t' = (cs.rightInvSeq ω).getD j' 1

Tactic:
grind only [cs.getD_rightInvSeq, = eraseIdx_eq_take_drop_succ, = getElem?_eraseIdx,
      = drop_append, drop_of_length_le, drop_drop, = length_append, = length_take, = length_drop,
      = min_def]

Premises used: List.getElem?_eraseIdx, List.drop_drop, List.length_drop, List.length_append, List.length_take, List.drop_of_length_le, min_def, List.eraseIdx_eq_take_drop_succ, List.drop_append, CoxeterSystem.getD_rightInvSeq
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
⊢ t' = (cs.rightInvSeq ω).getD j' 1

Tactic:
have h₃ : t' = (ris ω).getD j' 1 := by
    grind only [cs.getD_rightInvSeq, = eraseIdx_eq_take_drop_succ, = getElem?_eraseIdx,
      = drop_append, drop_of_length_le, drop_drop, = length_append, = length_take, = length_drop,
      = min_def]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
rw : (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1
⊢ t * t' = 1

Tactic:
rw [h₁, h₃, dup]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1

Tactic:
cs.getD_rightInvSeq_mul_self _ _

Premises used: CoxeterSystem.getD_rightInvSeq_mul_self
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1

Tactic:
exact cs.getD_rightInvSeq_mul_self _ _

Premises used: CoxeterSystem.getD_rightInvSeq_mul_self
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ t * t' = 1

Tactic:
have h₄ : t * t' = 1 := by
    rw [h₁, h₃, dup]
    exact cs.getD_rightInvSeq_mul_self _ _
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
rw : cs.wordProd ω = cs.wordProd ω * 1
⊢ cs.wordProd ω = cs.wordProd ω * t * t'

Tactic:
rw [mul_assoc, h₄]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * 1

Tactic:
group
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))

Tactic:
have h₅ := calc
    π ω = π ω * t * t' := by rw [mul_assoc, h₄]; group
    _ = (π (ω.eraseIdx j)) * t' :=
        congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _)
    _ = π ((ω.eraseIdx j).eraseIdx (j' - 1)) :=
        cs.wordProd_mul_getD_rightInvSeq _ _
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
⊢ ω.length ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length

Tactic:
have h₆ := calc
    ω.length = ℓ (π ω) := rω.symm
    _ = ℓ (π ((ω.eraseIdx j).eraseIdx (j' - 1))) := congrArg cs.length h₅
    _ ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length := cs.length_wordProd_le _
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
h₆ : ω.length ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length
⊢ False

Tactic:
grind
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
simp : (cs.rightInvSeq ω.reverse).Nodup
⊢ (cs.leftInvSeq ω).Nodup

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, nodup_reverse]

Premises used: List.nodup_reverse, _private.0.CoxeterSystem.leftInvSeq_eq_reverse_rightInvSeq_reverse
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
rω₁ : cs.IsReduced ω.reverse
⊢ (cs.rightInvSeq ω.reverse).Nodup

Tactic:
apply nodup_rightInvSeq

Premises used: CoxeterSystem.IsReduced.nodup_rightInvSeq
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω rω₁ rω₂ rω₃ rω₄ : cs.IsReduced ω
⊢ cs.IsReduced ω.reverse

Tactic:
rwa [isReduced_reverse_iff]

Premises used: CoxeterSystem.isReduced_reverse_iff
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
simp : k < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord j i (2 * p))).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (alternatingWord i j (2 * p)).length

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
simp : k < 2 * p
⊢ k < (alternatingWord j i (2 * p)).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
rw :
  cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) *
        cs.simple
          (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) ⋯) *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (cs.wordProd (take k (alternatingWord j i (2 * p))) *
          cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k ⋯) *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) (k + 1) ⋯ =
    (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord j i (2 * p))) k ⋯)

Tactic:
rw [cs.getElem_leftInvSeq (alternatingWord i j (2 * p)) (k + 1) (by simp [h]),
    cs.getElem_leftInvSeq (alternatingWord j i (2 * p)) k (by simp; lia)]

Premises used: HMul.hMul, CoxeterSystem.alternatingWord, HAdd.hAdd, CoxeterSystem.getElem_leftInvSeq, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
simp :
  cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) ⋯) =
    cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k ⋯)
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) *
        cs.simple
          (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) ⋯) *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (cs.wordProd (take k (alternatingWord j i (2 * p))) *
          cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k ⋯) *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)

Tactic:
simp only [MulAut.conj, listTake_succ_alternatingWord i j p k h, cs.wordProd_cons, mul_assoc,
    mul_inv_rev, inv_simple, MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.coe_mk, Equiv.coe_fn_mk,
    mul_right_inj, mul_left_inj]

Premises used: CoxeterSystem.inv_simple, mul_assoc, mul_left_inj, OneHom.coe_mk, CoxeterSystem.wordProd_cons, MulEquiv.coe_mk, MulAut.conj, mul_right_inj, MonoidHom.coe_mk, Equiv.coe_fn_mk, CoxeterSystem.listTake_succ_alternatingWord, mul_inv_rev
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h rw : k + 1 < 2 * p
⊢ cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) ⋯) =
    cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k ⋯)

Tactic:
rw [getElem_alternatingWord_swapIndices i j (2 * p) k]

Premises used: HMul.hMul, CoxeterSystem.getElem_alternatingWord_swapIndices, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h simp : k < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k < 2 * p
⊢ k < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < (alternatingWord i j (2 * p)).length

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
i j : B
h : 0 < 2 * p
zero :
  cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) 0 ⋯) =
    cs.simple i
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) 0 ⋯ =
    cs.wordProd (alternatingWord j i (HMul.hMul (α := ℕ) 2 0 + 1))

Tactic:
simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]),
      take_zero, wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append,
      nil_append, wordProd_singleton]

Premises used: HMul.hMul, inv_one, List.take_zero, CoxeterSystem.alternatingWord, List.concat_eq_append, CoxeterSystem.wordProd_singleton, CoxeterSystem.wordProd_nil, List.nil_append, mul_one, CoxeterSystem.getElem_leftInvSeq, OfNat.ofNat, one_mul
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < 2 * p

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
i j : B
h : 0 < 2 * p
⊢ cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) 0 ⋯) =
    cs.simple i

Tactic:
simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two,
      Even.mul_right, ↓reduceIte]

Premises used: HMul.hMul, even_two, Even.mul_right, CoxeterSystem.getElem_alternatingWord, reduceIte, add_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
      cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
      cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
succ :
  cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * cs.wordProd (alternatingWord j i (2 * (k + 1)))
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) (k + 1) ⋯ =
    cs.wordProd (alternatingWord j i (2 * (k + 1) + 1))

Tactic:
simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by lia),
      MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
      ↓reduceIte, wordProd_cons]

Premises used: CoxeterSystem.inv_simple, even_two, CoxeterSystem.getElem_succ_leftInvSeq_alternatingWord, CoxeterSystem.wordProd_cons, Even.mul_right, MulAut.conj_apply, CoxeterSystem.alternatingWord_succ', reduceIte