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 : ℕ
nhj : ¬j < ω.length
⊢ ω.length ≤ j

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

Tactic:
rw [getElem?_eq_none_iff.mpr (by lia)]

Premises used: Iff.mpr, List.getElem?_eq_none_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
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple none).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple none).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    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 : ℕ
simp_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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
⊢ (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1

Tactic:
simp_rw [getD_leftInvSeq, mul_assoc]

Premises used: CoxeterSystem.getD_leftInvSeq, 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
j : ℕ
inl :
  ∀ (hj : 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 ω) *
              ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
                (cs.wordProd (take j ω))⁻¹)))) =
      1
inr :
  ∀ (nhj : ¬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 ω) *
              ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
                (cs.wordProd (take 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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
rcases em (j < ω.length) with hj | nhj

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

Tactic:
rw [getElem?_eq_getElem hj]

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

Tactic:
simp [← mul_assoc]

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

Tactic:
rw [getElem?_eq_none_iff.mpr (by lia)]

Premises used: Iff.mpr, List.getElem?_eq_none_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
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple none).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple none).getD 1 * (cs.wordProd (take 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
⊢ cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)

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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])

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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
succ : cs.rightInvSeq (drop j ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
succ₁ : drop j (cs.rightInvSeq ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
succ₂ : drop j (cs.rightInvSeq ω) = drop (j + 1) ((cs.wordProd ω)⁻¹ * cs.simple k * cs.wordProd ω :: cs.rightInvSeq ω)
succ₃ succ₄ : drop j (cs.rightInvSeq ω) = drop j (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))

Tactic:
rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

Premises used: List.drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
succ : cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])
succ₁ :
  ∀ (k : B) (ω : List B),
    cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω) →
      cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)

Tactic:
induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

Premises used: List.cons, List.drop_succ_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
j : ℕ
zero : ∀ (ω : List B), cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)
succ :
  ∀ (j : ℕ) (ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)) (ω : List B),
    cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)

Tactic:
induction j generalizing ω with
  | zero => simp
  | succ j ih₁ =>
    induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

Premises used: List.cons, List.drop_succ_cons, CoxeterSystem.rightInvSeq, Matrix.zero, 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
j : ℕ
simp : (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (take j ω) = take j (cs.leftInvSeq ω)

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Premises used: _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
j : ℕ
rw :
  (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse

Tactic:
rw [List.take_reverse]

Premises used: List.take_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
j : ℕ
nth_rw :
  (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
nth_rw 1 [← List.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
j : ℕ
rw :
  (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
⊢ (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
rw [List.take_reverse]

Premises used: List.take_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
j : ℕ
⊢ (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
simp [rightInvSeq_drop]

Premises used: CoxeterSystem.rightInvSeq_drop
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
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
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
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 : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
cons :
  ∀
    (ih :
      ∀ (ht : (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 ω)
cons₁ : ∀ (mem : Mem t (cs.rightInvSeq ω)), cs.IsReflection t
⊢ cs.IsReflection t

Tactic:
rcases ht with _ | ⟨_, mem⟩
-- 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 :
  ∀ (ht : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω),
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
h : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

Tactic:
use (π ω)⁻¹, i
-- 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 :
  ∀ (ht : (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
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
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 : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
ih mem
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
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 : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
exact ih mem
-- 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 ω
nil : ∀ (ht : t ∈ cs.rightInvSeq []), cs.IsReflection t
cons :
  ∀ (i : B) (ω : List B) (ih : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t) (ht : t ∈ cs.rightInvSeq (i :: ω)),
    cs.IsReflection t
⊢ cs.IsReflection t

Tactic:
induction ω with
  | nil => simp at ht
  | cons i ω ih =>
    dsimp [rightInvSeq] at ht
    rcases ht with _ | ⟨_, mem⟩
    · use (π ω)⁻¹, i
      group
    · exact ih mem

Premises used: 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
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ t ∈ cs.rightInvSeq ω.reverse

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, mem_reverse] at ht

Premises used: List.mem_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
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ cs.IsReflection t

Tactic:
cs.isReflection_of_mem_rightInvSeq ω.reverse ht

Premises used: CoxeterSystem.isReflection_of_mem_rightInvSeq, List.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
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ cs.IsReflection t

Tactic:
exact cs.isReflection_of_mem_rightInvSeq ω.reverse ht

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

Tactic:
rw [getD_rightInvSeq, eraseIdx_eq_take_drop_succ]

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

Tactic:
nth_rw 1 [← take_append_drop (j + 1) ω]

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

Tactic:
rw [getD_leftInvSeq, eraseIdx_eq_take_drop_succ]

Premises used: CoxeterSystem.getD_leftInvSeq, List.eraseIdx_eq_take_drop_succ
-- 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 : ℕ
nth_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 + 1) ω ++ 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 ω =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
nth_rw 4 [← take_append_drop (j + 1) ω]

Premises used: List.take_append_drop, HAdd.hAdd, OfNat.ofNat