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
i : B
this_1 : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        (FreeGroup.of i * FreeGroup.of i) :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
⊢ HMul.hMul (α := W) (β := W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W) =
    1

Tactic:
exact map_mul_eq_one cs.mulEquiv.symm this

Premises used: CoxeterSystem.mulEquiv, map_mul_eq_one, MulEquiv.symm
-- 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
⊢ w * cs.simple i * cs.simple i = w

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
⊢ cs.simple i * (cs.simple i * w) = w

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- 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
⊢ HPow.hPow (β := ℕ) (cs.simple i) 2 = 1

Tactic:
pow_two (s i) ▸ cs.simple_mul_simple_self i

Premises used: pow_two, Eq.rec, CoxeterSystem.simple, CoxeterSystem.simple_mul_simple_self, Eq.symm
-- 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.simple i)⁻¹ = cs.simple i

Tactic:
(eq_inv_of_mul_eq_one_right (cs.simple_mul_simple_self i)).symm

Premises used: CoxeterSystem.simple_mul_simple_self, Eq.symm, eq_inv_of_mul_eq_one_right
-- 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 i' : B
⊢ (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet

Tactic:
have : (FreeGroup.of i * FreeGroup.of i') ^ M i i' ∈ M.relationsSet := ⟨(i, i'), 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
i i' : B
this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
⊢ 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)

Tactic:
have : (PresentedGroup.mk _ ((FreeGroup.of i * FreeGroup.of i') ^ M i i') : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
-- 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 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)
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
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Tactic:
unfold 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
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)
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)
⊢ 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:
rw [← map_mul, ← map_pow]

Premises used: map_pow, map_mul
-- 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 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)
⊢ 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:
(MulEquiv.map_eq_one_iff cs.mulEquiv.symm).mpr this

Premises used: Iff.mpr, MulEquiv.map_eq_one_iff, CoxeterSystem.mulEquiv, MulEquiv.symm
-- 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 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)
⊢ 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:
exact (MulEquiv.map_eq_one_iff cs.mulEquiv.symm).mpr this

Premises used: Iff.mpr, MulEquiv.map_eq_one_iff, CoxeterSystem.mulEquiv, MulEquiv.symm
-- 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 i' : B
⊢ (cs.simple i' * cs.simple i) ^ M.M i i' = 1

Tactic:
M.symmetric i' i ▸ cs.simple_mul_simple_pow i' i

Premises used: CoxeterSystem.simple_mul_simple_pow, Eq.rec, CoxeterMatrix.symmetric
-- 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.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
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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))
rw : cs.mulEquiv.symm.toMonoidHom.range = ⊤
⊢ Eq (α := Subgroup W) (Subgroup.closure (Set.range cs.simple)) ⊤

Tactic:
rw [this, Set.range_comp, ← MulEquiv.coe_toMonoidHom, ← MonoidHom.map_closure,
    PresentedGroup.closure_range_of, ← MonoidHom.range_eq_map]

Premises used: Set.range_comp, MonoidHom.range_eq_map, MulEquiv.coe_toMonoidHom, MonoidHom.map_closure, PresentedGroup.closure_range_of
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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))
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Tactic:
MonoidHom.range_eq_top.2 (MulEquiv.surjective _)

Premises used: Iff.mpr, MulEquiv.surjective, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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))
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Tactic:
exact MonoidHom.range_eq_top.2 (MulEquiv.surjective _)

Premises used: Iff.mpr, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)⁻¹
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)⁻¹

Tactic:
simp_rw [inv_range, inv_simple, union_self]

Premises used: CoxeterSystem.inv_simple, Set.inv_range, Set.union_self
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)⁻¹

Tactic:
have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
    simp_rw [inv_range, inv_simple, union_self]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 ⊤) ⊤
rw₃ rw₄ : Eq.{u_3 + 1} (α := Submonoid W) ⊤ ⊤
⊢ Eq (α := Submonoid W) (Submonoid.closure (Set.range cs.simple)) ⊤

Tactic:
rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]

Premises used: Subgroup.closure_toSubmonoid, Subgroup.top_toSubmonoid, CoxeterSystem.subgroup_closure_range_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
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')
have : ∀ (this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w), p w
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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')
this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
⊢ p w

Tactic:
Submonoid.closure_induction (fun x ⟨i, hi⟩ ↦ hi ▸ simple i) one (fun _ _ _ _ ↦ mul _ _)
    this

Premises used: Submonoid.closure_induction
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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')
this : Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w
⊢ p w

Tactic:
exact Submonoid.closure_induction (fun x ⟨i, hi⟩ ↦ hi ▸ simple i) one (fun _ _ _ _ ↦ mul _ _)
    this
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
let : p w
⊢ p w

Tactic:
let p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop :=
    fun w _ ↦ p w
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 1

Tactic:
one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 1

Tactic:
exact one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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)
⊢ p (i * y)

Tactic:
rw [Set.mem_range] at mi

Premises used: Set.mem_range
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 : ∃ (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:
mi.choose_spec ▸ mul_simple_left _ _ ih

Premises used: Exists.choose_spec, Eq.rec
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 : ∃ (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:
exact mi.choose_spec ▸ mul_simple_left _ _ ih
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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)
⊢ p w

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

Premises used: Set.mem_range
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
let : p w
⊢ p w

Tactic:
let p' : ((w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop) :=
    fun w _ ↦ p w
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ Membership.mem (γ := Submonoid W) (Submonoid.closure (Set.range cs.simple)) w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 1

Tactic:
one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 1

Tactic:
exact one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
mul_right : ∀ (mi : ∃ (y : B), cs.simple y = i) (ih : p y), p (y * i)
⊢ p (y * i)

Tactic:
rw [Set.mem_range] at mi

Premises used: Set.mem_range
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 : ∃ (y : B), cs.simple y = i
ih : p y
⊢ p (y * i)

Tactic:
mi.choose_spec ▸ mul_simple_right _ _ ih

Premises used: Exists.choose_spec, Eq.rec
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 : ∃ (y : B), cs.simple y = i
ih : p y
⊢ p (y * i)

Tactic:
exact mi.choose_spec ▸ mul_simple_right _ _ ih
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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)
⊢ p w

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

Premises used: Set.mem_range
-- 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 : MulOneClass G
φ₁ φ₂ : W →* G
h : ∀ (i : B), Eq.{u_5 + 1} (α := G) ((φ₁ : (a : W) → G) (cs.simple i) : G) ((φ₂ : (a : W) → G) (cs.simple i) : G)
⊢ φ₁ = φ₂

Tactic:
MonoidHom.eq_of_eqOn_denseM cs.submonoid_closure_range_simple (fun _ ⟨i, hi⟩ ↦ hi ▸ h i)

Premises used: Eq.rec, MonoidHom.eq_of_eqOn_denseM, CoxeterSystem.submonoid_closure_range_simple, _private.0.CoxeterSystem.simple_induction.match_1, Eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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)
⊢ 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)

Tactic:
rcases hr with ⟨⟨i, i'⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
rw : (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1
⊢ 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:
rw [uncurry, relation, map_pow, map_mul, FreeGroup.lift_apply_of, FreeGroup.lift_apply_of]

Premises used: FreeGroup.lift_apply_of, map_pow, map_mul, Function.uncurry, CoxeterMatrix.relation
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1

Tactic:
hf i i'
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1

Tactic:
exact hf i i'