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
t : W
ht : cs.IsReflection t
w : W
suffices :
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * t) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, 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
t : W
ht : cs.IsReflection t
w : W
rcases :
  ∀ (w_1 : W) (i : B),
    Ne (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * (w_1 * cs.simple i * w_1⁻¹)) :
        Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * t) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: 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
w_1 w : W
i : B
⊢ Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w_1 * (w * cs.simple i * w⁻¹)) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w_1 : Multiplicative (ZMod 2))

Tactic:
simp [lengthParity_simple]

Premises used: CoxeterSystem.lengthParity_simple
-- 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 : cs.IsReflection t
w : W
this :
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
contrapose :
  ∀ (this : cs.length (t * w) = cs.length w),
    Eq (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
contrapose 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
t : W
ht : cs.IsReflection t
w : W
this : cs.length (t * w) = cs.length w
⊢ Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))

Tactic:
simp only [lengthParity_eq_ofAdd_length, this]

Premises used: CoxeterSystem.lengthParity_eq_ofAdd_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
t : W
ht : cs.IsReflection t
w : W
suffices :
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
suffices cs.lengthParity (t * w) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, 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
t : W
ht : cs.IsReflection t
w : W
rcases :
  ∀ (w_1 : W) (i : B),
    Ne (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w_1 * cs.simple i * w_1⁻¹ * w) : Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: 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
w_1 w : W
i : B
⊢ Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * cs.simple i * w⁻¹ * w_1) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w_1 : Multiplicative (ZMod 2))

Tactic:
simp [lengthParity_simple]

Premises used: CoxeterSystem.lengthParity_simple
-- 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 : cs.IsReflection t
w : W
obtain : ∀ (u : W) (i : B), cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)
⊢ cs.IsReflection (w * t * w⁻¹)

Tactic:
obtain ⟨u, i, rfl⟩ := ht

Premises used: 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
w u : W
i : B
h : w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹
⊢ cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)

Tactic:
use w * u, 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
w u : W
i : B
⊢ w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹

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
w t : W
mp : cs.IsReflection (w * t * w⁻¹) → cs.IsReflection t
mpr : cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection 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
w t : W
h : cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection t

Tactic:
simpa [← mul_assoc] using h.conj w⁻¹

Premises used: mul_assoc, CoxeterSystem.IsReflection.conj, Inv.inv
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)

Tactic:
IsReflection.conj (w := w)

Premises used: CoxeterSystem.IsReflection.conj
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)

Tactic:
exact IsReflection.conj (w := w)

Premises used: CoxeterSystem.IsReflection.conj
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
h : cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)
⊢ cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

Tactic:
apply and_congr_right

Premises used: and_congr_right
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₁ : cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₂ : cs.length (t⁻¹ * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₃ : cs.length (t * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₄ h₅ : cs.length (t * w) < cs.length w ↔ cs.length (t * w) < cs.length w
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w

Tactic:
rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]

Premises used: CoxeterSystem.IsReflection.inv, inv_inv, mul_inv_rev, CoxeterSystem.length_inv
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w⁻¹⁻¹ t

Tactic:
cs.isRightInversion_inv_iff.symm

Premises used: CoxeterSystem.isRightInversion_inv_iff, Iff.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
w t : W
h : w = w⁻¹⁻¹
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

Tactic:
convert! cs.isRightInversion_inv_iff.symm

Premises used: CoxeterSystem.isRightInversion_inv_iff, Iff.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
w t : W
⊢ w = w⁻¹⁻¹

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
t : W
ht : cs.IsReflection t
w : W
simp : cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)
⊢ cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)

Tactic:
simp only [mul_assoc, ht.mul_self, mul_one, ht, true_and, not_lt]

Premises used: mul_assoc, CoxeterSystem.IsReflection.mul_self, not_lt, mul_one, true_and
-- 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 : cs.IsReflection t
w : W
mp : cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)
mpr : cs.length w ≤ cs.length (w * t) → cs.length w < cs.length (w * t)
⊢ cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * 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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)

Tactic:
le_of_lt

Premises used: le_of_lt
-- 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 : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)

Tactic:
exact le_of_lt

Premises used: le_of_lt
-- 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 : cs.IsReflection t
w : W
⊢ cs.length w ≤ cs.length (w * t) → cs.length w < cs.length (w * t)

Tactic:
(lt_of_le_of_ne' · (ht.length_mul_left_ne w))

Premises used: CoxeterSystem.IsReflection.length_mul_left_ne, lt_of_le_of_ne'
-- 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 : cs.IsReflection t
w : W
⊢ cs.length w ≤ cs.length (w * t) → cs.length w < cs.length (w * t)

Tactic:
exact (lt_of_le_of_ne' · (ht.length_mul_left_ne w))

Premises used: CoxeterSystem.IsReflection.length_mul_left_ne, lt_of_le_of_ne'
-- 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 : cs.IsReflection t
w : W
⊢ ¬cs.IsRightInversion (w * t) t ↔ cs.IsRightInversion w t

Tactic:
ht.isRightInversion_mul_left_iff.not_left

Premises used: Iff.not_left, CoxeterSystem.IsReflection.isRightInversion_mul_left_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
t : W
ht : cs.IsReflection t
w : W
rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
rw₁ : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₂ : cs.IsRightInversion (w⁻¹ * t⁻¹) t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₃ : cs.IsRightInversion (w⁻¹ * t) t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₄ rw₅ : ¬cs.IsRightInversion w⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

Tactic:
rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]

Premises used: CoxeterSystem.IsReflection.inv, CoxeterSystem.IsReflection.isRightInversion_mul_left_iff, mul_inv_rev, CoxeterSystem.isRightInversion_inv_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
t : W
ht : cs.IsReflection t
w : W
⊢ ¬cs.IsLeftInversion (t * w) t ↔ cs.IsLeftInversion w t

Tactic:
ht.isLeftInversion_mul_right_iff.not_left

Premises used: CoxeterSystem.IsReflection.isLeftInversion_mul_right_iff, Iff.not_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
w : W
i : B
⊢ cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

Tactic:
simp [IsRightInversion, IsRightDescent, cs.isReflection_simple i]

Premises used: CoxeterSystem.IsRightInversion, CoxeterSystem.isReflection_simple, CoxeterSystem.IsRightDescent
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i

Tactic:
simp [IsLeftInversion, IsLeftDescent, cs.isReflection_simple i]

Premises used: CoxeterSystem.IsLeftInversion, CoxeterSystem.IsLeftDescent, CoxeterSystem.isReflection_simple
-- 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 [] = []

Tactic:
rfl

Premises used: CoxeterSystem.rightInvSeq, 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
⊢ cs.leftInvSeq [] = []

Tactic:
rfl

Premises used: CoxeterSystem.leftInvSeq, 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
i : B
⊢ cs.rightInvSeq [i] = [cs.simple i]

Tactic:
simp [rightInvSeq]

Premises used: 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
i : B
⊢ cs.leftInvSeq [i] = [cs.simple i]

Tactic:
rfl

Premises used: List.map, CoxeterSystem.leftInvSeq, 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
i : B
⊢ cs.rightInvSeq (concat [] i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq []))
      (cs.simple i)

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
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
cons :
  (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)
⊢ cs.rightInvSeq ((j :: ω).concat i) =
    concat
      (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq (j :: ω)))
      (cs.simple i)

Tactic:
dsimp [rightInvSeq, concat]

Premises used: List.concat, 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
i j : B
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
cons :
  (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)

Tactic:
rw [ih]
-- 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
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
cons :
  cs.simple i * (cs.wordProd ω)⁻¹ * cs.simple j * (cs.wordProd ω * cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * cs.simple i
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)

Tactic:
simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, cons.injEq, and_true]

Premises used: CoxeterSystem.inv_simple, and_true, CoxeterSystem.wordProd_cons, List.concat_eq_append, List.cons.injEq, CoxeterSystem.wordProd_nil, mul_inv_rev, mul_one, 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
i j : B
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
⊢ cs.simple i * (cs.wordProd ω)⁻¹ * cs.simple j * (cs.wordProd ω * cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * cs.simple i

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
i : B
nil :
  cs.rightInvSeq (concat [] i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq []))
      (cs.simple i)
cons :
  ∀ (j : B) (ω : List B)
    (ih :
      cs.rightInvSeq (ω.concat i) =
        concat
          (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
          (cs.simple i)),
    cs.rightInvSeq ((j :: ω).concat i) =
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
          (cs.rightInvSeq (j :: ω)))
        (cs.simple i)
⊢ cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)

Tactic:
induction ω with
  | nil => simp
  | cons j ω ih =>
    dsimp [rightInvSeq, concat]
    rw [ih]
    simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, cons.injEq, and_true]
    group

Premises used: CoxeterSystem.inv_simple, and_true, List.concat, CoxeterSystem.wordProd_cons, List.concat_eq_append, List.cons, List.cons.injEq, CoxeterSystem.wordProd_nil, CoxeterSystem.rightInvSeq, mul_inv_rev, mul_one, CoxeterSystem.wordProd_append, 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
⊢ cs.leftInvSeq [] = (cs.rightInvSeq (reverse [])).reverse

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.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
cons :
  cs.simple i ::
      List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq ω.reverse).reverse =
    (concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
          (cs.rightInvSeq ω.reverse))
        (cs.simple i)).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Tactic:
rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]

Premises used: CoxeterSystem.rightInvSeq_concat, List.concat_eq_append, List.reverse_cons, CoxeterSystem.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
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i ::
      List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq ω.reverse).reverse =
    (concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
          (cs.rightInvSeq ω.reverse))
        (cs.simple i)).reverse

Tactic:
simp [map_reverse]

Premises used: List.map_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
nil : cs.leftInvSeq [] = (cs.rightInvSeq (reverse [])).reverse
cons :
  ∀ (i : B) (ω : List B) (ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse),
    cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse
⊢ cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse

Tactic:
induction ω with
  | nil => simp
  | cons i ω ih =>
    rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]
    simp [map_reverse]

Premises used: CoxeterSystem.rightInvSeq_concat, List.concat_eq_append, List.cons, List.reverse_cons, List.map_reverse, CoxeterSystem.leftInvSeq, 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
i : B
⊢ cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse, rightInvSeq]

Premises used: _private.0.CoxeterSystem.leftInvSeq_eq_reverse_rightInvSeq_reverse, 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
⊢ cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse

Tactic:
simp [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
⊢ cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse

Tactic:
simp [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
⊢ (cs.rightInvSeq []).length = List.length.{u_1} (α := B) []

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 ω).length = ω.length
⊢ (cs.rightInvSeq (i :: ω)).length = (i :: ω).length

Tactic:
simpa [rightInvSeq]

Premises used: CoxeterSystem.rightInvSeq