awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
a : PresentedGroup M.relationsSet
⊢ Eq.{u_1 + 1} (α := M.Group)
    ((cs.mulEquiv.toMonoidHom : (a : W) → PresentedGroup M.relationsSet) ((cs.mulEquiv.symm : (a : M.Group) → W) a) :
      PresentedGroup M.relationsSet)
    ((cs.mulEquiv : (a : W) → M.Group) ((cs.mulEquiv.symm : (a : M.Group) → W) a) : M.Group)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
a : PresentedGroup M.relationsSet
rw rw₁ : a = a
⊢ (cs.mulEquiv : (a : W) → M.Group) ((cs.mulEquiv.symm : (a : M.Group) → W) a) = a

Tactic:
rw [MulEquiv.apply_symm_apply]

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
ι : W →* G
i i' : B
rw :
  HMul.hMul (α := G) (β := G) ((ι : (a : W) → G) (cs.simple i) : G) (((⇑ι : (a : W) → G) ∘ cs.simple) i' : G) ^
      M.M i i' =
    1
rw₁ :
  HMul.hMul (α := G) (β := G) ((ι : (a : W) → G) (cs.simple i) : G) ((ι : (a : W) → G) (cs.simple i') : G) ^ M.M i i' =
    1
rw₂ : HPow.hPow (α := G) ((ι : (a : W) → G) (cs.simple i * cs.simple i') : G) (M.M i i') = 1
rw₃ : Eq.{u_5 + 1} (α := G) ((ι : (a : W) → G) ((cs.simple i * cs.simple i') ^ M.M i i') : G) (1 : G)
rw₄ : Eq.{u_5 + 1} (α := G) ((ι : (a : W) → G) 1 : G) (1 : G)
rw₅ rw₆ : Eq.{u_5 + 1} (α := G) 1 1
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1

Tactic:
rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]

Premises used: CoxeterSystem.simple_mul_simple_pow, map_pow, map_mul, map_one, Function.comp_apply
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
f : { f : B → G // M.IsLiftable f }
a :
  ∀ (i : B),
    (↑((fun (ι : W →* G) ↦
                (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
                  { f : B → G // M.IsLiftable f }))
              ((fun (f : { f : B → G // M.IsLiftable f }) ↦
                  (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
                f)) :
          B → G)
        i =
      (↑f : B → G) i
⊢ (fun (ι : W →* G) ↦
        (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
          { f : B → G // M.IsLiftable f }))
      ((fun (f : { f : B → G // M.IsLiftable f }) ↦
          (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
        f) =
    f

Tactic:
ext i
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
f : { f : B → G // M.IsLiftable f }
i : B
a :
  (Units.coeHom G : (a : Gˣ) → G)
      ((PresentedGroup.toGroup (f := restrictUnit ⋯) (rels := M.relationsSet) ⋯ :
            (a : PresentedGroup M.relationsSet) → Gˣ)
          ((cs.mulEquiv.toMonoidHom : (a : W) → PresentedGroup M.relationsSet)
            ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i))) :
        Gˣ) =
    (↑f : B → G) i
⊢ (↑((fun (ι : W →* G) ↦
              (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
                { f : B → G // M.IsLiftable f }))
            ((fun (f : { f : B → G // M.IsLiftable f }) ↦
                (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
              f)) :
        B → G)
      i =
    (↑f : B → G) i

Tactic:
simp only [MonoidHom.comp_apply, comp_apply, groupLift, simple]

Premises used: CoxeterSystem.simple, _private.0.CoxeterSystem.groupLift, Function.comp_apply, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
f : { f : B → G // M.IsLiftable f }
i : B
a :
  OneHom.toFun (M := Gˣ) (↑(Units.coeHom G) : OneHom Gˣ G)
      ((PresentedGroup.toGroup (f := restrictUnit ⋯) (rels := M.relationsSet) ⋯ :
          (a : PresentedGroup M.relationsSet) → Gˣ)
        ((cs.mulEquiv.toMonoidHom : (a : W) → PresentedGroup M.relationsSet)
          ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i)))) =
    (↑f : B → G) i
a₁ :
  OneHom.toFun (M := Gˣ) (↑(Units.coeHom G) : OneHom Gˣ G)
      ((PresentedGroup.toGroup (f := restrictUnit ⋯) (rels := M.relationsSet) ⋯ :
          (a : PresentedGroup M.relationsSet) → Gˣ)
        (PresentedGroup.of (rels := M.relationsSet) i)) =
    (↑f : B → G) i
a₂ : OneHom.toFun (↑(Units.coeHom G) : OneHom Gˣ G) (restrictUnit ⋯ i) = (↑f : B → G) i
a₃ : ((↑(Units.coeHom G) : OneHom Gˣ G) : (a : Gˣ) → G) (restrictUnit ⋯ i) = (↑f : B → G) i
a₄ : (Units.coeHom G : (a : Gˣ) → G) (restrictUnit ⋯ i) = (↑f : B → G) i
a₅ : (↑(restrictUnit ⋯ i) : G) = (↑f : B → G) i
a₆ a₇ : (↑{ val := (↑f : B → G) i, inv := (↑f : B → G) i, val_inv := ⋯, inv_val := ⋯ : Gˣ } : G) = (↑f : B → G) i
⊢ (Units.coeHom G : (a : Gˣ) → G)
      ((PresentedGroup.toGroup (f := restrictUnit ⋯) (rels := M.relationsSet) ⋯ :
            (a : PresentedGroup M.relationsSet) → Gˣ)
          ((cs.mulEquiv.toMonoidHom : (a : W) → PresentedGroup M.relationsSet)
            ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i))) :
        Gˣ) =
    (↑f : B → G) i

Tactic:
rw [← MonoidHom.toFun_eq_coe, toMonoidHom_apply_symm_apply, PresentedGroup.toGroup.of,
      OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, Units.coeHom_apply, restrictUnit]

Premises used: MonoidHom.toOneHom_coe, MonoidHom.toFun_eq_coe, _private.0.CoxeterSystem.restrictUnit, PresentedGroup.toGroup.of, Units.coeHom_apply, _private.0.CoxeterSystem.toMonoidHom_apply_symm_apply, OneHom.toFun_eq_coe
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
ι : W →* G
apply :
  ∀ (i : B),
    Eq.{u_5 + 1} (α := G)
      (((fun (f : { f : B → G // M.IsLiftable f }) ↦
                (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
              ((fun (ι : W →* G) ↦
                  (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
                    { f : B → G // M.IsLiftable f }))
                ι) :
            (a : W) → G)
          (cs.simple i) :
        G)
      ((ι : (a : W) → G) (cs.simple i) : G)
⊢ (fun (f : { f : B → G // M.IsLiftable f }) ↦
        (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
      ((fun (ι : W →* G) ↦
          (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
            { f : B → G // M.IsLiftable f }))
        ι) =
    ι

Tactic:
apply cs.ext_simple

Premises used: CoxeterSystem.ext_simple
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
ι : W →* G
i : B
dsimp :
  Eq.{u_5 + 1} (α := G)
    ((MonoidHom.comp (Units.coeHom G)
            (cs.groupLift (f := restrictUnit (M := M) (f := (⇑ι : (a : W) → G) ∘ cs.simple) ⋯) ⋯) :
          (a : W) → G)
        (cs.simple i) :
      G)
    ((ι : (a : W) → G) (cs.simple i) : G)
⊢ Eq.{u_5 + 1} (α := G)
    (((fun (f : { f : B → G // M.IsLiftable f }) ↦
              (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit ⋯) ⋯) : W →* G))
            ((fun (ι : W →* G) ↦
                (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) ⋯ :
                  { f : B → G // M.IsLiftable f }))
              ι) :
          (a : W) → G)
        (cs.simple i) :
      G)
    ((ι : (a : W) → G) (cs.simple i) : G)

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
ι : W →* G
i : B
rw :
  Eq.{u_5 + 1} (α := G)
    ((↑{ val := ((⇑ι : (a : W) → G) ∘ cs.simple) i, inv := ((⇑ι : (a : W) → G) ∘ cs.simple) i, val_inv := ⋯,
            inv_val := ⋯ } :
        G) :
      G)
    ((ι : (a : W) → G) ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) : G)
⊢ Eq.{u_5 + 1} (α := G)
    ((MonoidHom.comp (Units.coeHom G)
            (cs.groupLift (f := restrictUnit (M := M) (f := (⇑ι : (a : W) → G) ∘ cs.simple) ⋯) ⋯) :
          (a : W) → G)
        (cs.simple i) :
      G)
    ((ι : (a : W) → G) (cs.simple i) : G)

Tactic:
rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
      PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]

Premises used: CoxeterSystem.simple, _private.0.CoxeterSystem.restrictUnit, PresentedGroup.toGroup.of, Units.coeHom_apply, _private.0.CoxeterSystem.groupLift, _private.0.CoxeterSystem.toMonoidHom_apply_symm_apply, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_2 : Monoid G
ι : W →* G
i : B
⊢ Eq.{u_5 + 1} (α := G)
    ((↑{ val := ((⇑ι : (a : W) → G) ∘ cs.simple) i, inv := ((⇑ι : (a : W) → G) ∘ cs.simple) i, val_inv := ⋯,
            inv_val := ⋯ } :
        G) :
      G)
    ((ι : (a : W) → G) ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) : G)

Tactic:
simp only [comp_apply, simple]

Premises used: CoxeterSystem.simple, Function.comp_apply
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst_1 : Monoid G
f : B → G
hf : M.IsLiftable f
i : B
⊢ (((cs.lift : (a : { f : B → G // M.IsLiftable f }) → W →* G)
            (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) f hf) :
          W →* G) :
        (a : W) → G)
      (cs.simple i) =
    f i

Tactic:
congrFun (congrArg Subtype.val (cs.lift.left_inv ⟨f, hf⟩)) i

Premises used: congrArg, Subtype.mk, CoxeterSystem.lift, congrFun, Subtype.val, Equiv.left_inv
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
mulEquiv : cs1.mulEquiv = cs2.mulEquiv
⊢ cs1 = cs2

Tactic:
apply CoxeterSystem.ext

Premises used: CoxeterSystem.ext
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
mulEquiv : cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom
⊢ cs1.mulEquiv = cs2.mulEquiv

Tactic:
apply MulEquiv.toMonoidHom_injective

Premises used: MulEquiv.toMonoidHom_injective
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
mulEquiv :
  ∀ (i : B),
    Eq.{u_1 + 1} (α := M.Group) ((cs1.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)
      ((cs2.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)
⊢ cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom

Tactic:
apply cs1.ext_simple

Premises used: CoxeterSystem.ext_simple
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
mulEquiv :
  ∀ (i : B),
    Eq.{u_1 + 1} (α := M.Group) ((cs1.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)
      ((cs2.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs2.simple i) : M.Group)
⊢ ∀ (i : B),
    Eq.{u_1 + 1} (α := M.Group) ((cs1.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)
      ((cs2.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ ∀ (i : B),
    Eq.{u_1 + 1} (α := M.Group) ((cs1.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs1.simple i) : M.Group)
      ((cs2.mulEquiv.toMonoidHom : (a : W) → M.Group) (cs2.simple i) : M.Group)

Tactic:
simp [simple]

Premises used: CoxeterSystem.simple
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd [] = 1

Tactic:
simp [wordProd]

Premises used: CoxeterSystem.wordProd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
simp [wordProd]

Premises used: CoxeterSystem.wordProd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.wordProd [i] = cs.simple i

Tactic:
simp [wordProd]

Premises used: CoxeterSystem.wordProd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
⊢ cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i

Tactic:
simp [wordProd]

Premises used: CoxeterSystem.wordProd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω ω' : List B
⊢ cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'

Tactic:
simp [wordProd]

Premises used: CoxeterSystem.wordProd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd (reverse []) = (cs.wordProd [])⁻¹

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Tactic:
simpa [wordProd_cons, wordProd_append] using ih

Premises used: CoxeterSystem.wordProd_cons, CoxeterSystem.wordProd_append
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
nil : cs.wordProd (reverse []) = (cs.wordProd [])⁻¹
cons :
  ∀ (x : B) (ω' : List B) (ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹),
    cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹

Tactic:
induction ω with
  | nil => simp
  | cons x ω' ih => simpa [wordProd_cons, wordProd_append] using ih

Premises used: CoxeterSystem.wordProd_cons, List.cons, CoxeterSystem.wordProd_append, List.nil
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
one : ∃ (a : List B), cs.wordProd a = 1
mul_simple_left :
  ∀ (w : W) (i : B), (∃ (a : List B), cs.wordProd a = w) → ∃ (a : List B), cs.wordProd a = cs.simple i * w
⊢ ∃ (a : List B), cs.wordProd a = w

Tactic:
apply cs.simple_induction_left w

Premises used: CoxeterSystem.simple_induction_left
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.wordProd [] = 1
⊢ ∃ (a : List B), cs.wordProd a = 1

Tactic:
use []
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h h₁ : Eq.{u_3 + 1} (α := W) 1 1
⊢ cs.wordProd [] = 1

Tactic:
rw [wordProd_nil]

Premises used: CoxeterSystem.wordProd_nil
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
h : cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
⊢ ∃ (a : List B), cs.wordProd a = cs.simple i * cs.wordProd ω

Tactic:
use i :: ω
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
h h₁ : cs.simple i * cs.wordProd ω = cs.simple i * cs.wordProd ω
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
rw [wordProd_cons]

Premises used: CoxeterSystem.wordProd_cons
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i i' : B
m : ℕ
⊢ alternatingWord i i' (m + 1) = (alternatingWord i' i m).concat i'

Tactic:
rfl

Premises used: CoxeterSystem.alternatingWord, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i i' : B
⊢ alternatingWord i i' (HAdd.hAdd (α := ℕ) 0 1) = (if Even (α := ℕ) 0 then i' else i) :: alternatingWord i i' 0

Tactic:
simp [alternatingWord]

Premises used: CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
succ :
  ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
nth_rw 1 [ih i' i]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: (alternatingWord i' i m).concat i'

Tactic:
simp [Nat.even_add_one, -Nat.not_even_iff_odd]

Premises used: Nat.even_add_one, Nat.not_even_iff_odd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i i' : B
m : ℕ
zero :
  ∀ (i i' : B),
    alternatingWord i i' (HAdd.hAdd (α := ℕ) 0 1) = (if Even (α := ℕ) 0 then i' else i) :: alternatingWord i i' 0
succ :
  ∀ (m : ℕ) (ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m)
    (i i' : B), alternatingWord i i' (m + 1 + 1) = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m

Tactic:
induction m generalizing i i' with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord]
    nth_rw 1 [ih i' i]
    rw [alternatingWord]
    simp [Nat.even_add_one, -Nat.not_even_iff_odd]

Premises used: Nat.even_add_one, Nat.not_even_iff_odd, CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i i' : B
⊢ (alternatingWord i i' 0).length = 0

Tactic:
dsimp [alternatingWord]

Premises used: CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), (alternatingWord i i' m).length = m
i i' : B
⊢ (alternatingWord i i' (m + 1)).length = m + 1

Tactic:
simpa [alternatingWord] using ih i' i

Premises used: CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i i' : B
m : ℕ
zero : ∀ (i i' : B), (alternatingWord i i' 0).length = 0
succ :
  ∀ (m : ℕ) (ih : ∀ (i i' : B), (alternatingWord i i' m).length = m) (i i' : B),
    (alternatingWord i i' (m + 1)).length = m + 1
⊢ (alternatingWord i i' m).length = m

Tactic:
induction m generalizing i i' with
  | zero => dsimp [alternatingWord]
  | succ m ih => simpa [alternatingWord] using ih i' i

Premises used: CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
hk : k < p
⊢ k < (alternatingWord i j p).length

Tactic:
simp [hk]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
hk : k < p
revert :
  ∀ (k : ℕ) (hk : k < p),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j p) k ⋯ =
      if Even (p + k) then i else j
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j p) k ⋯ =
    if Even (p + k) then i else j

Tactic:
revert k
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
⊢ ∀ (k : ℕ) (hk : k < 0),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j 0) k ⋯ =
      if Even (0 + k) then i else j

Tactic:
grind
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
n : ℕ
h :
  ∀ (k : ℕ) (hk : k < n),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j n) k ⋯ =
      if Even (n + k) then i else j
⊢ ∀ (k : ℕ) (hk : k < n + 1),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (n + 1)) k ⋯ =
      if Even (n + 1 + k) then i else j

Tactic:
grind [CoxeterSystem.alternatingWord_succ']

Premises used: CoxeterSystem.alternatingWord_succ'
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p : ℕ
zero :
  ∀ (k : ℕ) (hk : k < 0),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j 0) k ⋯ =
      if Even (0 + k) then i else j
succ :
  ∀ (n : ℕ)
    (h :
      ∀ (k : ℕ) (hk : k < n),
        getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j n) k ⋯ =
          if Even (n + k) then i else j)
    (k : ℕ) (hk : k < n + 1),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (n + 1)) k ⋯ =
      if Even (n + 1 + k) then i else j
⊢ ∀ (k : ℕ) (hk : k < p),
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j p) k ⋯ =
      if Even (p + k) then i else j

Tactic:
induction p with
  | zero => grind
  | succ n h => grind [CoxeterSystem.alternatingWord_succ']

Premises used: CoxeterSystem.alternatingWord_succ'
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < p
⊢ k + 1 < (alternatingWord i j p).length

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < p
simp : k < p
⊢ k < (alternatingWord j i p).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < p
⊢ k < p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ k + 1 < p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ k < p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
rw : (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j p) (k + 1) ⋯ =
    getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i p) k ⋯

Tactic:
rw [getElem_alternatingWord i j p (k + 1) (by lia),
    getElem_alternatingWord j i p k (by lia)]

Premises used: CoxeterSystem.getElem_alternatingWord, HAdd.hAdd, OfNat.ofNat