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
j : ℕ
rw :
  cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
rw [take_add_one]

Premises used: List.take_add_one
-- 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
j : ℕ
inl :
  ∀ (lt : j < ω.length),
    cs.wordProd (take j ω) *
            (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
          (cs.wordProd (take j ω))⁻¹ *
        cs.wordProd
          (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
      cs.wordProd (take j ω ++ drop (j + 1) ω)
inr :
  ∀ (le : ω.length ≤ j),
    cs.wordProd (take j ω) *
            (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
          (cs.wordProd (take j ω))⁻¹ *
        cs.wordProd
          (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
      cs.wordProd (take j ω ++ drop (j + 1) ω)
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
obtain lt | le := lt_or_ge j ω.length

Premises used: lt_or_ge, List.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
j : ℕ
lt : j < ω.length
inl :
  cs.wordProd (take j ω) *
      ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt))).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) *
            (cs.wordProd (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt)).toList *
              cs.wordProd (drop (j + 1) ω))))) =
    cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]

Premises used: mul_assoc, List.getElem?_eq_getElem, CoxeterSystem.wordProd_append
-- 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
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt))).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) *
            (cs.wordProd (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt)).toList *
              cs.wordProd (drop (j + 1) ω))))) =
    cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)

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
j : ℕ
le : ω.length ≤ j
inr :
  cs.wordProd (take j ω) * (Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ Option.toList none ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_none le]

Premises used: List.getElem?_eq_none
-- 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
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω) * (Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ Option.toList none ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
left : cs.IsReflection t
right : cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)
⊢ cs.IsRightInversion (cs.wordProd ω) t

Tactic:
constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
cs.isReflection_of_mem_rightInvSeq ω ht

Premises used: CoxeterSystem.isReflection_of_mem_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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
exact cs.isReflection_of_mem_rightInvSeq ω ht

Premises used: CoxeterSystem.isReflection_of_mem_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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
right :
  ∀ (j : ℕ) (hj : j < (cs.rightInvSeq ω).length)
    (ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω),
    cs.length (cs.wordProd ω * getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj) <
      cs.length (cs.wordProd ω)
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)

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

Premises used: Iff.mp, List.mem_iff_getElem, rfl
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω
right : cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
⊢ cs.length (cs.wordProd ω * getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj) <
    cs.length (cs.wordProd ω)

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

Premises used: List.getD_eq_getElem, CoxeterSystem.wordProd_mul_getD_rightInvSeq, 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω
⊢ j < ω.length

Tactic:
rw [cs.length_rightInvSeq] at hj

Premises used: CoxeterSystem.length_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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω
hj₁ : j < ω.length
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω

Tactic:
rw [cs.length_rightInvSeq] at hj

Premises used: CoxeterSystem.length_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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) ≤ (ω.eraseIdx j).length

Tactic:
cs.length_wordProd_le _

Premises used: CoxeterSystem.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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
rw : (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1
⊢ (ω.eraseIdx j).length < ω.length

Tactic:
rw [← List.length_eraseIdx_add_one hj]

Premises used: List.length_eraseIdx_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ ω.length = cs.length (cs.wordProd ω)

Tactic:
hω.symm

Premises used: Eq.symm
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
ℓ : (ω.eraseIdx j).length < ω.length
⊢ 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

Premises used: List.eraseIdx, CoxeterSystem.length_wordProd_le, Eq.symm, List.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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
left : cs.IsReflection t
right : cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)
⊢ cs.IsLeftInversion (cs.wordProd ω) t

Tactic:
constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

Tactic:
cs.isReflection_of_mem_leftInvSeq ω ht

Premises used: CoxeterSystem.isReflection_of_mem_leftInvSeq
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

Tactic:
exact cs.isReflection_of_mem_leftInvSeq ω ht

Premises used: CoxeterSystem.isReflection_of_mem_leftInvSeq
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
right :
  ∀ (j : ℕ) (hj : j < (cs.leftInvSeq ω).length)
    (ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω),
    cs.length (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj * cs.wordProd ω) <
      cs.length (cs.wordProd ω)
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)

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

Premises used: Iff.mp, List.mem_iff_getElem, rfl
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω
right : cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
⊢ cs.length (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj * cs.wordProd ω) <
    cs.length (cs.wordProd ω)

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

Premises used: List.getD_eq_getElem, CoxeterSystem.getD_leftInvSeq_mul_wordProd, 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω
⊢ j < ω.length

Tactic:
rw [cs.length_leftInvSeq] at hj

Premises used: CoxeterSystem.length_leftInvSeq
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω
hj₁ : j < ω.length
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω

Tactic:
rw [cs.length_leftInvSeq] at hj

Premises used: CoxeterSystem.length_leftInvSeq
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) ≤ (ω.eraseIdx j).length

Tactic:
cs.length_wordProd_le _

Premises used: CoxeterSystem.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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
rw : (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1
⊢ (ω.eraseIdx j).length < ω.length

Tactic:
rw [← List.length_eraseIdx_add_one hj]

Premises used: List.length_eraseIdx_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ ω.length = cs.length (cs.wordProd ω)

Tactic:
hω.symm

Premises used: Eq.symm
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
ℓ : (ω.eraseIdx j).length < ω.length
⊢ 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

Premises used: List.eraseIdx, CoxeterSystem.length_wordProd_le, Eq.symm, List.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
⊢ (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹

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 : B
ω : List B
ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
⊢ (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹

Tactic:
simp [rightInvSeq, ih, wordProd_cons]

Premises used: CoxeterSystem.wordProd_cons, CoxeterSystem.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
nil : (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹
cons :
  ∀ (i : B) (ω : List B) (ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹),
    (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
induction ω with
  | nil => simp
  | cons i ω ih => simp [rightInvSeq, ih, wordProd_cons]

Premises used: CoxeterSystem.wordProd_cons, List.cons, CoxeterSystem.rightInvSeq, List.nil
-- 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
simp : prod (List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse)) = cs.wordProd ω
⊢ (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]

Premises used: List.prod_reverse_noncomm, _private.0.CoxeterSystem.leftInvSeq_eq_reverse_rightInvSeq_reverse, inv_inj
-- 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
h : ∀ a ∈ cs.rightInvSeq ω.reverse, a⁻¹ = id a
⊢ List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = List.map id (cs.rightInvSeq ω.reverse)

Tactic:
apply List.map_congr_left

Premises used: List.map_congr_left
-- 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
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ t⁻¹ = id t

Tactic:
(cs.isReflection_of_mem_rightInvSeq _ ht).inv

Premises used: CoxeterSystem.IsReflection.inv, CoxeterSystem.isReflection_of_mem_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
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ t⁻¹ = id t

Tactic:
exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv

Premises used: CoxeterSystem.IsReflection.inv, CoxeterSystem.isReflection_of_mem_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
⊢ List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse

Tactic:
have : List.map (fun x ↦ x⁻¹) (ris ω.reverse) = ris ω.reverse := calc
    List.map (fun x ↦ x⁻¹) (ris ω.reverse)
    _ = List.map id (ris ω.reverse) := by
        apply List.map_congr_left
        intro t ht
        exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv
    _ = ris ω.reverse := map_id _
-- 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
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
rw : (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
⊢ prod (List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse)) = cs.wordProd ω

Tactic:
rw [this]
-- 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
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
nth_rw : (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω

Tactic:
nth_rw 2 [← reverse_reverse ω]

Premises used: List.reverse_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
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
rw : (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse

Tactic:
rw [wordProd_reverse]

Premises used: CoxeterSystem.wordProd_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
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹

Tactic:
cs.prod_rightInvSeq _

Premises used: CoxeterSystem.prod_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
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹

Tactic:
exact cs.prod_rightInvSeq _

Premises used: CoxeterSystem.prod_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 ω
apply :
  ∀ (i j : ℕ),
    i < j →
      j < (cs.rightInvSeq ω).length →
        getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) i ≠
          getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j
⊢ (cs.rightInvSeq ω).Nodup

Tactic:
apply List.nodup_iff_getElem?_ne_getElem?.mpr

Premises used: Iff.mpr, List.nodup_iff_getElem?_ne_getElem?