awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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
have a₂ : OneHom.toFun (↑(Units.coeHom G) : OneHom Gˣ G) (restrictUnit sorry i) = (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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
have a₃ : ((↑(Units.coeHom G) : OneHom Gˣ G) : (a : Gˣ) → G) (restrictUnit sorry i) = (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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
have a₄ : (Units.coeHom G : (a : Gˣ) → G) (restrictUnit sorry i) = (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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
have a₅ : (↑(restrictUnit sorry 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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
have a₆ : (↑{ val := (↑f : B → G) i, inv := (↑f : B → G) i, val_inv := sorry, inv_val := sorry : Gˣ } : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (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 }))
        ι) =
    ι
have 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 sorry) sorry) : W →* G))
            ((fun (ι : W →* G) ↦
                (Subtype.mk (p := fun (f : B → G) ↦ M.IsLiftable f) ((⇑ι : (a : W) → G) ∘ cs.simple) sorry :
                  { f : B → G // M.IsLiftable f }))
              ι) :
          (a : W) → G)
        (cs.simple i) :
      G)
    ((ι : (a : W) → G) (cs.simple i) : G)
Tactic: apply cs.ext_simple
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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)
    ((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)
have rw : Eq.{u_5 + 1} (α := G)
  ((↑{ val := ((⇑ι : (a : W) → G) ∘ cs.simple) i, inv := ((⇑ι : (a : W) → G) ∘ cs.simple) i, val_inv := sorry,
          inv_val := sorry } :
      G) :
    G)
  ((ι : (a : W) → G) ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) : G)
Tactic: rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
      PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ cs1 = cs2
have mulEquiv : cs1.mulEquiv = cs2.mulEquiv
Tactic: apply CoxeterSystem.ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ cs1.mulEquiv = cs2.mulEquiv
have mulEquiv : cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom
Tactic: apply MulEquiv.toMonoidHom_injective
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom
have 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)
Tactic: apply cs1.ext_simple
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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) (cs1.simple i) : M.Group)
have 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)
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹
have nil : cs.wordProd (reverse []) = (cs.wordProd [])⁻¹
Tactic: induction ω with
  | nil => simp
  | cons x ω' ih => simpa [wordProd_cons, wordProd_append] using ih
Cleared hypotheses: ω
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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 [])⁻¹
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹
have cons : ∀ (x : B) (ω' : List B) (ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹),
  cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹
Tactic: induction ω with
  | nil => simp
  | cons x ω' ih => simpa [wordProd_cons, wordProd_append] using ih
Cleared hypotheses: ω
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ (a : List B), cs.wordProd a = w
have one : ∃ (a : List B), cs.wordProd a = 1
Tactic: apply cs.simple_induction_left w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ ∃ (a : List B), cs.wordProd a = w
have mul_simple_left : ∀ (w : W) (i : B), (∃ (a : List B), cs.wordProd a = w) → ∃ (a : List B), cs.wordProd a = cs.simple i * w
Tactic: apply cs.simple_induction_left w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ (a : List B), cs.wordProd a = 1
have h : cs.wordProd [] = 1
Tactic: use []
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.wordProd [] = 1
have h : Eq.{u_3 + 1} (α := W) 1 1
Tactic: rw [wordProd_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ ∃ (a : List B), cs.wordProd a = cs.simple i * cs.wordProd ω
have h : cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
Tactic: use i :: ω
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
have h : cs.simple i * cs.wordProd ω = cs.simple i * cs.wordProd ω
Tactic: rw [wordProd_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
have 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)
Tactic: nth_rw 1 [ih i' i]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i i' : B
m : ℕ
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
have zero : ∀ (i i' : B),
  alternatingWord i i' (HAdd.hAdd (α := ℕ) 0 1) = (if Even (α := ℕ) 0 then i' else i) :: alternatingWord i i' 0
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]
Cleared hypotheses: i, i', m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
have 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)
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]
Cleared hypotheses: i, i', m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i i' : B
m : ℕ
⊢ (alternatingWord i i' m).length = m
have zero : ∀ (i i' : B), (alternatingWord i i' 0).length = 0
Tactic: induction m generalizing i i' with
  | zero => dsimp [alternatingWord]
  | succ m ih => simpa [alternatingWord] using ih i' i
Cleared hypotheses: i, i', m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i i' : B
m : ℕ
zero : ∀ (i i' : B), (alternatingWord i i' 0).length = 0
⊢ (alternatingWord i i' m).length = m
have succ : ∀ (m : ℕ) (ih : ∀ (i i' : B), (alternatingWord i i' m).length = m) (i i' : B),
  (alternatingWord i i' (m + 1)).length = m + 1
Tactic: induction m generalizing i i' with
  | zero => dsimp [alternatingWord]
  | succ m ih => simpa [alternatingWord] using ih i' i
Cleared hypotheses: i, i', m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p 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
have revert : ∀ (k : ℕ) (hk : k < p),
  getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j p) k sorry =
    if Even (p + k) then i else j
Tactic: revert k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p : ℕ
⊢ ∀ (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
have zero : ∀ (k : ℕ) (hk : k < 0),
  getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j 0) k sorry =
    if Even (0 + k) then i else j
Tactic: induction p with
  | zero => grind
  | succ n h => grind [CoxeterSystem.alternatingWord_succ']
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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
⊢ ∀ (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
have succ : ∀ (n : ℕ)
  (h :
    ∀ (k : ℕ) (hk : k < n),
      getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j n) k sorry =
        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 sorry =
    if Even (n + 1 + k) then i else j
Tactic: induction p with
  | zero => grind
  | succ n h => grind [CoxeterSystem.alternatingWord_succ']
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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 < (alternatingWord j i p).length
have simp : k < p
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ 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 ⋯
have rw : (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
Tactic: rw [getElem_alternatingWord i j p (k + 1) (by lia),
    getElem_alternatingWord j i p k (by lia)]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
have pos : ∀ (h_even : Even (p + k)), (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
Tactic: by_cases h_even : Even (p + k)
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
pos : ∀ (h_even : Even (p + k)), (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
have neg : ∀ (h_even : ¬Even (p + k)), (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
Tactic: by_cases h_even : Even (p + k)
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
have pos : (if Even (p + k + 1) then i else j) = j
Tactic: rw [if_pos h_even, ← add_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
have neg : (if Even (p + k + 1) then i else j) = i
Tactic: rw [if_neg h_even, ← add_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (h : k < 2 * p),
    take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
have hk : k < 2 * p
Tactic: have hk : k < 2 * p := by lia
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (h : k < 2 * p),
    take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : k < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
have hk₁ : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
Tactic: apply h' at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (h : k < 2 * p),
    take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
have pos : ∀ (h_even : Even k),
  take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
Tactic: by_cases h_even : Even k