-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_mul_simple_self (i : B) : s i * s i = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
⊢ cs.simple i * cs.simple i = 1

Tactic:
have : (PresentedGroup.mk _ (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
  (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.simple i * cs.simple i = 1

Proof state:
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 = 1

Tactic:
have : (FreeGroup.of i) * (FreeGroup.of i) ∈ M.relationsSet := ⟨(i, i), by simp [relation]⟩

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
⊢ cs.simple i * cs.simple i = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i) = 1

Tactic:
rw [← map_mul, PresentedGroup.of, map_mul]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.mk M.relationsSet) (FreeGroup.of i)) *
      cs.mulEquiv.symm ((PresentedGroup.mk M.relationsSet) (FreeGroup.of i)) =
    1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.mk M.relationsSet) (FreeGroup.of i)) *
      cs.mulEquiv.symm ((PresentedGroup.mk M.relationsSet) (FreeGroup.of i)) =
    1

Tactic:
exact map_mul_eq_one cs.mulEquiv.symm this

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ uncurry M.relation (i, i) = FreeGroup.of i * FreeGroup.of i

Tactic:
simp [relation]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.simple i * cs.simple i = 1

Tactic:
unfold simple

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i) = 1