Theoremsinjective_lift_of_ping_pong, append_head, append_last, append_prod, inv_head, inv_last, inv_prod, mulHead_head, mulHead_prod, of_word, prod_singleton, replaceHead_head, singleton_head, singleton_last, toList_getLast?, toList_head?, toList_ne_nil, ext, ext_iff, fstIdx_ne, chain_ne, consRecOn_cons, consRecOn_empty, cons_eq_smul, cons_toList, empty_toList, equivPair_eq_of_fstIdx_ne, equivPair_head, equivPair_head_smul_equivPair_tail, equivPair_smul_same, equivPair_symm, equivPair_tail, equivPair_tail_eq_inv_smul, ext, ext_iff, fstIdx_cons, fstIdx_ne_iff, mem_equivPair_tail_iff, mem_of_mem_equivPair_tail, mem_rcons_iff, mem_smul_iff, mem_smul_iff_of_ne, ne_one, of_smul_def, prod_cons, prod_empty, prod_rcons, prod_smul, rcons_eq_smul, rcons_inj, smul_def, smul_eq_of_smul, smul_induction, empty_of_word_prod_eq_one, ext_hom, ext_hom_iff, iSup_mrange_of, induction_left, induction_on, instIsFreeGroup, inv_def, lift_comp_of, lift_comp_of', lift_injective_of_ping_pong, lift_mrange_le, lift_of, lift_of', lift_range_le, lift_symm_apply, lift_word_ping_pong, lift_word_prod_nontrivial_of_head_card, lift_word_prod_nontrivial_of_head_eq_last, lift_word_prod_nontrivial_of_not_empty, lift_word_prod_nontrivial_of_other_i, mclosure_iUnion_range_of, mrange_eq_iSup, of_apply, of_injective, of_leftInverse, range_eq_iSup, freeGroupEquivCoprodI_apply, freeGroupEquivCoprodI_symm_apply | 82 |