awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i i' : B
this_1 : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1
have unfold : HMul.hMul (α := W) (β := W) ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i') : W) ^
    M.M i i' =
  1
Tactic: unfold 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
cs : CoxeterSystem M W
i i' : B
this_1 : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
⊢ HMul.hMul (α := W) (β := W)
        ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W)
        ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i') : W) ^
      M.M i i' =
    1
have rw : Eq.{u_3 + 1} (α := W)
  ((cs.mulEquiv.symm : (a : M.Group) → W)
      (HMul.hMul (α := M.Group) (PresentedGroup.of (rels := M.relationsSet) i)
          (PresentedGroup.of (rels := M.relationsSet) i') ^
        M.M i i') :
    W)
  (1 : W)
Tactic: rw [← map_mul, ← map_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Eq (α := Subgroup W) (Subgroup.closure (Set.range cs.simple)) ⊤
have this : cs.simple = comp (β := M.Group) (⇑cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet))
Tactic: have : cs.simple = cs.mulEquiv.symm ∘ PresentedGroup.of := rfl
-- 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
this :
  cs.simple = comp (β := M.Group) (⇑cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet))
⊢ Eq (α := Subgroup W) (Subgroup.closure (Set.range cs.simple)) ⊤
have rw : cs.mulEquiv.symm.toMonoidHom.range = ⊤
Tactic: rw [this, Set.range_comp, ← MulEquiv.coe_toMonoidHom, ← MonoidHom.map_closure,
    PresentedGroup.closure_range_of, ← MonoidHom.range_eq_map]
-- 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
⊢ Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
have simp_rw : Set.range cs.simple = Set.range cs.simple ∪ Set.range fun (i : B) ↦ (cs.simple i)⁻¹
Tactic: simp_rw [inv_range, inv_simple, union_self]
-- 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
simp_rw : Set.range cs.simple = Set.range cs.simple ∪ Set.range fun (i : B) ↦ (cs.simple i)⁻¹
⊢ Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
have simp_rw₁ : Set.range cs.simple = Set.range cs.simple ∪ Set.range fun (i : B) ↦ cs.simple i
Tactic: simp_rw [inv_range, inv_simple, union_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤
have this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
Tactic: have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
    simp_rw [inv_range, inv_simple, union_self]
-- 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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤
have rw : Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple ∪ (Set.range cs.simple)⁻¹)) ⊤
Tactic: rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]
-- 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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
rw : Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple ∪ (Set.range cs.simple)⁻¹)) ⊤
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤
have rw₁ : Eq (α := Submonoid W) (Subgroup.toSubmonoid (Subgroup.closure (Set.range cs.simple))) ⊤
Tactic: rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]
-- 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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
rw : Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple ∪ (Set.range cs.simple)⁻¹)) ⊤
rw₁ : Eq (α := Submonoid W) (Subgroup.toSubmonoid (Subgroup.closure (Set.range cs.simple))) ⊤
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤
have rw₂ : Eq.{u_3 + 1} (α := Submonoid W) (Subgroup.toSubmonoid ⊤) ⊤
Tactic: rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]
-- 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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
rw : Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple ∪ (Set.range cs.simple)⁻¹)) ⊤
rw₁ : Eq (α := Submonoid W) (Subgroup.toSubmonoid (Subgroup.closure (Set.range cs.simple))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submonoid W) (Subgroup.toSubmonoid ⊤) ⊤
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤
have rw₃ : Eq.{u_3 + 1} (α := Submonoid W) ⊤ ⊤
Tactic: rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]
-- 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
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
⊢ p w
have have : ∀ (this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w), p w
Tactic: have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
⊢ p w
have this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
Tactic: have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top 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
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
i : W
mi : i ∈ Set.range cs.simple
y : W
my : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) y
ih : p y
⊢ p (i * y)
have mul_left : ∀ (mi : ∃ (y : B), cs.simple y = i) (y : W)
  (my : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) y) (ih : p y), p (i * y)
Tactic: rw [Set.mem_range] at mi
Cleared hypotheses: mi, y, my, ih
-- 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
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
one₁ : p 1
⊢ p w
have mul_left : ∀ (i : W) (mi : i ∈ Set.range cs.simple) (y : W)
  (my : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) y) (ih : p y), p (i * y)
Tactic: induction this using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left i mi y my ih =>
    rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_left _ _ ih
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
⊢ p w
have this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
Tactic: have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top 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
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
y : W
my : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) y
i : W
mi : i ∈ Set.range cs.simple
ih : p y
⊢ p (y * i)
have mul_right : ∀ (mi : ∃ (y : B), cs.simple y = i) (ih : p y), p (y * i)
Tactic: rw [Set.mem_range] at mi
Cleared hypotheses: mi, ih
-- 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
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w → Prop :=
  fun (w : W) (x : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w) ↦ p w
this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
one₁ : p 1
⊢ p w
have mul_right : ∀ (y : W) (my : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) y) (i : W)
  (mi : i ∈ Set.range cs.simple) (ih : p y), p (y * i)
Tactic: induction this using Submonoid.closure_induction_right with
  | one => exact one
  | mul_right y my i mi ih =>
    rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_right _ _ ih
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst : Group G
f : B → G
hf : M.IsLiftable f
r : FreeGroup B
hr : r ∈ M.relationsSet
⊢ Eq.{u_5 + 1} (α := G)
    ((((FreeGroup.lift : (a : B → G) → FreeGroup B →* G) f : MonoidHom.{u_1, u_5} (FreeGroup B) G) :
          (a : FreeGroup B) → G)
        r :
      G)
    (1 : G)
have rcases : ∀ (i i' : B),
  Eq.{u_5 + 1} (α := G)
    ((((FreeGroup.lift : (a : B → G) → FreeGroup B →* G) f : MonoidHom.{u_1, u_5} (FreeGroup B) G) :
          (a : FreeGroup B) → G)
        (uncurry M.relation (i, i')) :
      G)
    (1 : G)
Tactic: rcases hr with ⟨⟨i, i'⟩, rfl⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ Eq.{u_5 + 1} (α := G)
    ((((FreeGroup.lift : (a : B → G) → FreeGroup B →* G) f : MonoidHom.{u_1, u_5} (FreeGroup B) G) :
          (a : FreeGroup B) → G)
        (uncurry M.relation (i, i')) :
      G)
    (1 : G)
have rw : (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1
Tactic: rw [uncurry, relation, map_pow, map_mul, FreeGroup.lift_apply_of, FreeGroup.lift_apply_of]
-- 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
a : PresentedGroup M.relationsSet
⊢ (cs.mulEquiv : (a : W) → M.Group) ((cs.mulEquiv.symm : (a : M.Group) → W) a) = a
have rw : a = a
Tactic: rw [MulEquiv.apply_symm_apply]
-- 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 i' : B
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw : HMul.hMul (α := G) (β := G) ((ι : (a : W) → G) (cs.simple i) : G) (((⇑ι : (a : W) → G) ∘ cs.simple) i' : G) ^ M.M i i' =
  1
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 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
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw₁ : HMul.hMul (α := G) (β := G) ((ι : (a : W) → G) (cs.simple i) : G) ((ι : (a : W) → G) (cs.simple i') : G) ^ M.M i i' = 1
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 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
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw₂ : HPow.hPow (α := G) ((ι : (a : W) → G) (cs.simple i * cs.simple i') : G) (M.M i i') = 1
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 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
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw₃ : Eq.{u_5 + 1} (α := G) ((ι : (a : W) → G) ((cs.simple i * cs.simple i') ^ M.M i i') : G) (1 : G)
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 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)
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw₄ : Eq.{u_5 + 1} (α := G) ((ι : (a : W) → G) 1 : G) (1 : G)
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 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)
⊢ HMul.hMul (α := G) (((⇑ι : (a : W) → G) ∘ cs.simple) i) (((⇑ι : (a : W) → G) ∘ cs.simple) i') ^ M.M i i' = 1
have rw₅ : Eq.{u_5 + 1} (α := G) 1 1
Tactic: rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]
-- 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 }
⊢ (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
have a : ∀ (i : B),
  (↑((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 }))
            ((fun (f : { f : B → G // M.IsLiftable f }) ↦
                (MonoidHom.comp (Units.coeHom G) (cs.groupLift (f := restrictUnit sorry) sorry) : W →* G))
              f)) :
        B → G)
      i =
    (↑f : B → G) i
Tactic: ext i
-- 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
⊢ (↑((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
have a : (Units.coeHom G : (a : Gˣ) → G)
    ((PresentedGroup.toGroup (f := restrictUnit sorry) (rels := M.relationsSet) sorry :
          (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: simp only [MonoidHom.comp_apply, comp_apply, groupLift, 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
f : { f : B → G // M.IsLiftable f }
i : B
⊢ (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 (M := Gˣ) (↑(Units.coeHom G) : OneHom Gˣ G)
    ((PresentedGroup.toGroup (f := restrictUnit sorry) (rels := M.relationsSet) sorry :
        (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
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
⊢ (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 (M := Gˣ) (↑(Units.coeHom G) : OneHom Gˣ G)
    ((PresentedGroup.toGroup (f := restrictUnit sorry) (rels := M.relationsSet) sorry :
        (a : PresentedGroup M.relationsSet) → Gˣ)
      (PresentedGroup.of (rels := M.relationsSet) 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]