∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_2}
  [inst_1 : Monoid G] (f : { f // M.IsLiftable f }),
  (fun ι => ⟨⇑ι ∘ cs.simple, ⋯⟩) ((fun f => (Units.coeHom G).comp (CoxeterSystem.groupLift✝ cs ⋯)) f) = f