diff --git a/.gitignore b/.gitignore
index 0c8c123..3a19649 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@ GPATH
 GRTAGS
 GSYMS
 GTAGS
+TAGS
 Makefile
 *.cmake
 CMakeFiles/
diff --git a/TAGS b/TAGS
deleted file mode 100644
index f016d47..0000000
--- a/TAGS
+++ /dev/null
@@ -1,692 +0,0 @@
-
-homotopy/spherical_fibrations.hlean,1152
-  definition pointed_BFspherical_fibrations.pointed_BF50,1310
-  definition pBGspherical_fibrations.pBG15,414
-  definition BF_of_BG_mulspherical_fibrations.BF_of_BG_mul95,2692
-  definition BFspherical_fibrations.BF47,1244
-    definition thom_spacespherical_fibrations.thom.thom_space109,3059
-  definition mirrorspherical_fibrations.mirror23,605
-  definition Gspherical_fibrations.G17,484
-  definition G_charspherical_fibrations.G_char20,537
-  definition BG_mulspherical_fibrations.BG_mul78,2096
-  definition BF_succspherical_fibrations.BF_succ55,1496
-  definition BG_of_BFspherical_fibrations.BG_of_BF71,1919
-  definition BF_of_BGspherical_fibrations.BF_of_BG62,1681
-    protected definition secspherical_fibrations.thom.sec104,2964
-    definition tauspherical_fibrations.two_sphere.tau144,4263
-  definition BG_succspherical_fibrations.BG_succ39,1009
-  definition pBFspherical_fibrations.pBF53,1426
-  definition pointed_BGspherical_fibrations.pointed_BG12,301
-  definition BF_mulspherical_fibrations.BF_mul87,2401
-  definition BGspherical_fibrations.BG9,233
-  definition S_of_BGspherical_fibrations.S_of_BG36,936
-
-homotopy/homotopy_groups.hlean,743
-    definition group_equiv_onemy.group_equiv_one44,1189
-    theorem group_equiv_mul_assocmy.group_equiv_mul_assoc52,1423
-    theorem group_equiv_mul_onemy.group_equiv_mul_one58,1710
-    definition group_equiv_invmy.group_equiv_inv46,1234
-  theorem ap1_conmy.ap1_con25,626
-    theorem group_equiv_mul_left_invmy.group_equiv_mul_left_inv61,1852
-    definition group_equiv_closedmy.group_equiv_closed65,2030
-    theorem group_equiv_one_mulmy.group_equiv_one_mul55,1568
-    definition group_equiv_mulmy.group_equiv_mul42,1118
-  definition apn_composemy.apn_compose18,411
-  definition apn_conmy.apn_con30,784
-  definition homotopy_group_homomorphismeq.homotopy_group_homomorphism83,2503
-  definition tr_mulmy.tr_mul34,931
-
-homotopy/sample.hlean,1236
-    definition is_conn_of_map_from_unithomotopy.is_conn_of_map_from_unit97,3227
-  definition is_connhomotopy.is_conn12,308
-    definition elimhomotopy.is_conn_fun.elim51,1665
-  definition is_conn_homotopyhomotopy.is_conn_homotopy154,4935
-    definition introhomotopy.is_conn_fun.intro70,2280
-  definition is_conn_funhomotopy.is_conn_fun24,636
-    definition rechomotopy.is_conn_fun.rec39,1224
-    definition is_conn_of_map_to_unithomotopy.is_conn_of_map_to_unit88,2969
-  definition merely_of_minus_one_connhomotopy.merely_of_minus_one_conn131,4268
-  definition minus_one_conn_of_merelyhomotopy.minus_one_conn_of_merely134,4364
-  definition is_conn_susphomotopy.is_conn_susp165,5320
-  definition minus_one_conn_of_surjectivehomotopy.minus_one_conn_of_surjective117,3839
-    definition is_conn_fun_from_unithomotopy.is_conn_fun_from_unit106,3534
-  definition is_surjection_of_minus_one_connhomotopy.is_surjection_of_minus_one_conn124,4078
-  definition is_conn_equiv_closedhomotopy.is_conn_equiv_closed15,404
-  definition minus_two_connhomotopy.minus_two_conn159,5215
-    definition elim_βhomotopy.is_conn_fun.elim_β54,1767
-    definition retract_of_conn_is_connhomotopy.retract_of_conn_is_conn143,4572
-
-homotopy/LES_applications.hlean,701
-    definition add_plus_one_minus_oneis_conn.add_plus_one_minus_one110,4328
-    definition add_plus_one_succis_conn.add_plus_one_succ111,4398
-  definition eq_even_or_eq_oddnat.eq_even_or_eq_odd7,278
-  definition join_empty_rightis_conn.join_empty_right87,3633
-    definition succ_add_plus_oneis_conn.succ_add_plus_one114,4613
-  definition rec_on_even_oddnat.rec_on_even_odd16,554
-  theorem is_surjective_π_of_is_connectedis_conn.is_surjective_π_of_is_connected69,2838
-    definition minus_one_add_plus_oneis_conn.minus_one_add_plus_one112,4480
-  definition natural_square2is_conn.natural_square2102,4049
-  theorem is_equiv_π_of_is_connectedis_conn.is_equiv_π_of_is_connected32,921
-
-homotopy/LES_of_homotopy_groups.hlean,8241
-  definition LES_of_homotopy_groups3_1chain_complex.LES_of_homotopy_groups3_1882,34115
-  definition is_exact_LES_of_homotopy_groups3chain_complex.is_exact_LES_of_homotopy_groups3857,32991
-  definition LES_of_homotopy_groups3_4chain_complex.LES_of_homotopy_groups3_4888,34446
-  definition homotopy_groups_fun2chain_complex.homotopy_groups_fun2544,20051
-  definition LES_of_homotopy_groups_mul3add2'chain_complex.LES_of_homotopy_groups_mul3add2'477,17839
-  definition LES_of_homotopy_groups3_3chain_complex.LES_of_homotopy_groups3_3886,34336
-  definition tr_mul_trchain_complex.tr_mul_tr500,18472
-  definition is_exact_fiber_sequencechain_complex.is_exact_fiber_sequence80,2506
-  definition boundary_mapchain_complex.boundary_map225,8385
-  theorem fiber_sequence_fun_phomotopychain_complex.fiber_sequence_fun_phomotopy216,8057
-  definition is_exact_LES_of_homotopy_groupschain_complex.is_exact_LES_of_homotopy_groups410,15146
-  definition LES_of_homotopy_groups3_2chain_complex.LES_of_homotopy_groups3_2884,34221
-  definition homotopy_groups_mul3add2chain_complex.homotopy_groups_mul3add2254,9279
-  definition type_LES_of_homotopy_groupschain_complex.type_LES_of_homotopy_groups386,14323
-  definition homotopy_groups_fun2_add1_5chain_complex.homotopy_groups_fun2_add1_5592,22238
-  definition homotopy_groups_fun'chain_complex.homotopy_groups_fun'276,10198
-  definition fin_prod_nat_equiv_natchain_complex.fin_prod_nat_equiv_nat620,23461
-  definition fiber_sequence_helpernchain_complex.fiber_sequence_helpern54,1759
-  theorem fiber_sequence_carrier_pequiv_eq_point_eq_idpchain_complex.fiber_sequence_carrier_pequiv_eq_point_eq_idp177,6559
-  definition homotopy_groups_funchain_complex.homotopy_groups_fun260,9523
-  definition fiber_sequence_carrierchain_complex.fiber_sequence_carrier62,1987
-  definition homotopy_groups_fun_add3chain_complex.homotopy_groups_fun_add3312,11532
-  definition comm_group_LES_of_homotopy_groupschain_complex.comm_group_LES_of_homotopy_groups486,18179
-  definition LES_of_homotopy_groups2chain_complex.LES_of_homotopy_groups2779,30007
-  definition LES_of_homotopy_groups_mul3add1chain_complex.LES_of_homotopy_groups_mul3add1451,17024
-  definition homotopy_groups_add3chain_complex.homotopy_groups_add3240,8787
-  definition LES_of_homotopy_groups3_0chain_complex.LES_of_homotopy_groups3_0880,34009
-  definition homotopy_groups3eq2chain_complex.homotopy_groups3eq2794,30462
-  definition fiber_sequence_helperchain_complex.fiber_sequence_helper50,1612
-  definition homotopy_groups2_pequiv'chain_complex.homotopy_groups2_pequiv'641,24217
-  definition fiber_sequence_carrier_equiv_inv_eqchain_complex.fiber_sequence_carrier_equiv_inv_eq125,4437
-  definition homotopy_groups2chain_complex.homotopy_groups2526,19349
-  definition fiber_sequence_pequiv_homotopy_groupschain_complex.fiber_sequence_pequiv_homotopy_groups319,11794
-  definition is_homomorphism_cast_loop_space_succ_eq_inchain_complex.is_homomorphism_cast_loop_space_succ_eq_in504,18597
-  definition fiber_sequence_funchain_complex.fiber_sequence_fun65,2078
-  definition LES_of_homotopy_groups_mul3add1'chain_complex.LES_of_homotopy_groups_mul3add1'471,17652
-  definition nat_of_str_6Schain_complex.nat_of_str_6S610,23009
-  definition homotopy_groups_mul3chain_complex.homotopy_groups_mul3244,8912
-  definition LES_of_homotopy_groupschain_complex.LES_of_homotopy_groups401,14827
-  definition homotopy_groups_fun2_add1_4chain_complex.homotopy_groups_fun2_add1_4583,21862
-  definition homotopy_groups3chain_complex.homotopy_groups3786,30178
-  definition fiber_sequence_pequiv_homotopy_groups_3_phomotopychain_complex.fiber_sequence_pequiv_homotopy_groups_3_phomotopy336,12382
-  definition homotopy_groupschain_complex.homotopy_groups234,8658
-  definition homotopy_groups_fun2_add1_2chain_complex.homotopy_groups_fun2_add1_2565,21099
-  definition homotopy_groups_fun2_phomotopychain_complex.homotopy_groups_fun2_phomotopy689,26060
-  definition LES_of_homotopy_groups3_5chain_complex.LES_of_homotopy_groups3_5890,34556
-  definition LES_of_homotopy_groups_fun3_1chain_complex.LES_of_homotopy_groups_fun3_1899,34906
-  definition group_LES_of_homotopy_groups3_0chain_complex.group_LES_of_homotopy_groups3_0916,35755
-  definition CommGroup_LES_of_homotopy_groups3chain_complex.CommGroup_LES_of_homotopy_groups3933,36775
-  definition is_exact_type_LES_of_homotopy_groups2chain_complex.is_exact_type_LES_of_homotopy_groups2772,29801
-  theorem homotopy_groups_fun_eqchain_complex.homotopy_groups_fun_eq287,10605
-  definition LES_of_homotopy_groups_mul3'chain_complex.LES_of_homotopy_groups_mul3'465,17477
-  definition LES_of_homotopy_groups_fun3_0chain_complex.LES_of_homotopy_groups_fun3_0896,34780
-  definition comm_group_LES_of_homotopy_groups3chain_complex.comm_group_LES_of_homotopy_groups3923,36148
-  definition homotopy_groups_fun2_add1_1chain_complex.homotopy_groups_fun2_add1_1560,20890
-  definition fiber_sequence_pequiv_homotopy_groups_add3chain_complex.fiber_sequence_pequiv_homotopy_groups_add3331,12158
-  definition homotopy_groups_fun'_add3chain_complex.homotopy_groups_fun'_add3283,10455
-  definition is_homomorphism_inversechain_complex.is_homomorphism_inverse514,19037
-  theorem fiber_sequence_fun_phomotopy_helperchain_complex.fiber_sequence_fun_phomotopy_helper194,7170
-  definition homotopy_groups_fun_add6chain_complex.homotopy_groups_fun_add6270,9919
-  definition LES_of_homotopy_groups_fun3_5chain_complex.LES_of_homotopy_groups_fun3_5911,35532
-  theorem fiber_sequence_phomotopy_homotopy_groups'chain_complex.fiber_sequence_phomotopy_homotopy_groups'344,12670
-  definition LES_of_homotopy_groups_fun3_4chain_complex.LES_of_homotopy_groups_fun3_4908,35381
-  definition is_exact_type_LES_of_homotopy_groupschain_complex.is_exact_type_LES_of_homotopy_groups393,14582
-  definition fiber_sequence_carrier_equiv_eqchain_complex.fiber_sequence_carrier_equiv_eq110,3830
-  definition LES_of_homotopy_groups_mul3chain_complex.LES_of_homotopy_groups_mul3444,16814
-  definition LES_of_homotopy_groups3chain_complex.LES_of_homotopy_groups3850,32786
-  theorem fiber_sequence_phomotopy_homotopy_groupschain_complex.fiber_sequence_phomotopy_homotopy_groups377,13934
-  definition LES_of_homotopy_groups_mul3add2chain_complex.LES_of_homotopy_groups_mul3add2458,17246
-  definition homotopy_groups_fun3chain_complex.homotopy_groups_fun3804,30894
-  definition homotopy_groups_mul3add1chain_complex.homotopy_groups_mul3add1249,9089
-  definition fiber_sequence_carrier_pequiv_inv_eqchain_complex.fiber_sequence_carrier_pequiv_inv_eq149,5360
-  definition fiber_sequence_carrier_pequivchain_complex.fiber_sequence_carrier_pequiv134,4778
-  theorem fiber_sequence_fun_eqchain_complex.fiber_sequence_fun_eq208,7685
-  definition fiber_sequence_carrier_equivchain_complex.fiber_sequence_carrier_equiv84,2664
-  definition nat_of_strchain_complex.nat_of_str604,22800
-  definition fiber_sequencechain_complex.fiber_sequence70,2251
-  definition str_of_natchain_complex.str_of_nat607,22917
-  definition homomorphism_LES_of_homotopy_groups_fun3chain_complex.homomorphism_LES_of_homotopy_groups_fun3937,36984
-  definition homotopy_groups_fun3eq2chain_complex.homotopy_groups_fun3eq2816,31572
-  definition homotopy_groups_fun2_add1_0chain_complex.homotopy_groups_fun2_add1_0555,20681
-  definition fiber_sequence_fun_eq_helperchain_complex.fiber_sequence_fun_eq_helper157,5693
-  definition homotopy_groups2_add1chain_complex.homotopy_groups2_add1534,19628
-  definition homotopy_groups_fun2_add1_3chain_complex.homotopy_groups_fun2_add1_3574,21486
-  definition LES_of_homotopy_groups_fun3_3chain_complex.LES_of_homotopy_groups_fun3_3905,35239
-  definition LES_of_homotopy_groups_fun3_2chain_complex.LES_of_homotopy_groups_fun3_2902,35041
-  definition type_LES_of_homotopy_groups2chain_complex.type_LES_of_homotopy_groups2758,29331
-  definition homotopy_groups2_pequivchain_complex.homotopy_groups2_pequiv684,25855
-  definition group_LES_of_homotopy_groupschain_complex.group_LES_of_homotopy_groups483,18035
-  definition fiber_sequence_carrier_pequiv_eqchain_complex.fiber_sequence_carrier_pequiv_eq142,5004
-
-group_theory/constructions.hlean,10223
-  definition normal_subgroup_kernelgroup.normal_subgroup_kernel721,26462
-  structure Rinvgroup.normal_subgroup_rel.Rinv23,565
-    | rinvgroup.generating_relation'.rinv614,22880
-  | rreflgroup.free_comm_group.fcg_rel.rrefl435,16260
-  definition fcg_mulgroup.free_comm_group.fcg_mul492,18417
-  theorem subgroup_one_mulgroup.subgroup_one_mul82,3290
-  structure rec_ongroup.normal_subgroup_rel.rec_on23,565
-    definition quotient_comm_group_gengroup.quotient_comm_group_gen633,23558
-  structure Rgroup.subgroup_rel.R17,410
-  theorem kernel_mulgroup.kernel_mul680,25173
-  definition sggroup.sg65,2698
-  theorem subgroup_mul_assocgroup.subgroup_mul_assoc79,3183
-    | rmulgroup.generating_relation'.rmul613,22779
-  definition subgroup_onegroup.subgroup_one68,2786
-  definition is_reflexive_Rgroup.free_group.is_reflexive_R290,10899
-  inductive cases_ongroup.free_group.free_group_rel.cases_on274,10175
-  abbreviation subgroup_has_onegroup.subgroup_has_one28,791
-  definition free_group_onegroup.free_group.free_group_one315,11815
-  theorem quotient_rel_symmgroup.quotient_rel_symm120,4459
-  | resp_appendgroup.free_group.free_group_rel.resp_append278,10373
-  definition fcg_carriergroup.free_comm_group.fcg_carrier449,16786
-  definition group_qggroup.group_qg210,7984
-  theorem product_one_mulgroup.product_one_mul240,9105
-  definition free_group_inclusiongroup.free_group_inclusion376,13925
-  structure destructgroup.subgroup_rel.destruct17,410
-  definition free_comm_group_inclusiongroup.free_comm_group_inclusion560,20652
-  theorem free_group_mul_left_invgroup.free_group.free_group_mul_left_inv348,12968
-  definition group_prodgroup.group_prod255,9511
-  | rtransgroup.free_group.free_group_rel.rtrans280,10519
-  definition free_comm_group_homgroup.free_comm_group_hom575,21250
-    definition normal_generating_relationgroup.normal_generating_relation625,23357
-  definition free_comm_groupgroup.free_comm_group555,20471
-  structure to_subgroup_relgroup.normal_subgroup_rel.to_subgroup_rel23,565
-  definition free_group_invgroup.free_group.free_group_inv316,11879
-  structure Rmulgroup.normal_subgroup_rel.Rmul23,565
-  theorem rel_respect_reversegroup.free_comm_group.rel_respect_reverse468,17493
-  theorem free_group_mul_assocgroup.free_group.free_group_mul_assoc327,12349
-  structure normal_subgroup_relgroup.normal_subgroup_rel23,565
-    definition gr_mulgroup.gr_mul622,23272
-  theorem product_mul_assocgroup.product_mul_assoc237,8989
-  definition quotient_comm_groupgroup.quotient_comm_group221,8428
-  theorem fcg_one_mulgroup.free_comm_group.fcg_one_mul509,18950
-  abbreviation subgroup_respect_mulgroup.subgroup_respect_mul29,860
-  definition comm_group_prodgroup.comm_group_prod262,9779
-  inductive fcg_relgroup.free_comm_group.fcg_rel.rec434,16208
-  definition quotient_relgroup.quotient_rel115,4268
-    inductive dirsum_relgroup.dirsum_rel643,23866
-  theorem quotient_mul_assocgroup.quotient_mul_assoc172,6919
-  theorem product_mul_commgroup.product_mul_comm249,9371
-  definition subgroupgroup.subgroup102,3873
-  theorem fgh_helper_respect_comm_relgroup.fgh_helper_respect_comm_rel563,20753
-  theorem quotient_rel_transgroup.quotient_rel_trans123,4623
-  definition kernelgroup.kernel678,25082
-  definition qggroup.qg157,6375
-  definition comm_subgroupgroup.comm_subgroup109,4111
-    definition direct_sumgroup.direct_sum646,23998
-  structure normal_subgroup_relgroup.normal_subgroup_rel.rec23,565
-    definition gr_invgroup.gr_inv620,23198
-  theorem rel_cons_concatgroup.free_comm_group.rel_cons_concat479,17905
-  theorem fgh_helper_mulgroup.fgh_helper_mul393,14566
-  definition comm_group_sggroup.comm_group_sg105,3947
-  | resp_appendgroup.free_comm_group.fcg_rel.resp_append439,16420
-  definition fn_of_free_group_homgroup.fn_of_free_group_hom413,15391
-  theorem fcg_mul_assocgroup.free_comm_group.fcg_mul_assoc500,18669
-  theorem product_mul_left_invgroup.product_mul_left_inv246,9271
-  definition comm_group_qggroup.comm_group_qg217,8257
-  definition normal_subgroup_rel_commgroup.normal_subgroup_rel_comm39,1314
-  | cancel1group.free_comm_group.fcg_rel.cancel1436,16290
-  definition fgh_helpergroup.fgh_helper379,14019
-  definition product_onegroup.product_one226,8642
-    mkgroup.normal_subgroup_rel.mk24,627
-    definition generating_relationgroup.generating_relation617,23026
-  | cancel2group.free_group.free_group_rel.cancel2277,10322
-    | rmkgroup.dirsum_rel.rmk644,23910
-  structure no_confusiongroup.subgroup_rel.no_confusion17,410
-  inductive rec_ongroup.free_comm_group.fcg_rel.rec_on434,16208
-  theorem is_normal_subgroup_kernelgroup.is_normal_subgroup_kernel707,25917
-  theorem fgh_helper_respect_relgroup.fgh_helper_respect_rel382,14131
-  abbreviation is_normal_subgroupgroup.is_normal_subgroup31,998
-    | rinclgroup.generating_relation'.rincl612,22730
-  definition free_group_carriergroup.free_group.free_group_carrier287,10767
-  theorem quotient_mul_onegroup.quotient_mul_one187,7357
-  | rtransgroup.free_comm_group.fcg_rel.rtrans441,16545
-  structure Rinvgroup.subgroup_rel.Rinv17,410
-  definition fn_of_free_comm_group_homgroup.fn_of_free_comm_group_hom586,21759
-    mkgroup.subgroup_rel.mk18,442
-    definition gr_onegroup.gr_one619,23155
-  theorem is_normal_subgroup_rev'group.is_normal_subgroup_rev'52,1969
-  structure subgroup_relgroup.subgroup_rel.rec17,410
-  structure Rgroup.normal_subgroup_rel.R23,565
-  inductive fcg_relgroup.free_comm_group.fcg_rel434,16208
-  definition quotient_onegroup.quotient_one161,6480
-  theorem quotient_rel_reflgroup.quotient_rel_refl118,4339
-  theorem product_mul_onegroup.product_mul_one243,9188
-  definition free_comm_group_hom_equiv_fngroup.free_comm_group_hom_equiv_fn590,21903
-  definition subgroup_kernelgroup.subgroup_kernel699,25721
-  | cancel1group.free_group.free_group_rel.cancel1276,10271
-  definition product_mulgroup.product_mul229,8782
-  theorem quotient_rel_resp_mulgroup.quotient_rel_resp_mul140,5543
-  definition free_groupgroup.free_group371,13774
-  theorem is_normal_subgroup'group.is_normal_subgroup'36,1200
-  definition productgroup.product259,9701
-  definition free_group_homgroup.free_group_hom402,14897
-  theorem normal_subgroup_insertgroup.normal_subgroup_insert55,2094
-  theorem quotient_mul_left_invgroup.quotient_mul_left_inv193,7512
-  structure Rmulgroup.subgroup_rel.Rmul17,410
-  theorem quotient_rel_resp_invgroup.quotient_rel_resp_inv131,5061
-  theorem fcg_mul_commgroup.free_comm_group.fcg_mul_comm536,19740
-  definition group_free_comm_groupgroup.group_free_comm_group551,20268
-    inductive cases_ongroup.dirsum_rel.cases_on643,23866
-  structure Ronegroup.normal_subgroup_rel.Rone23,565
-  structure is_normalgroup.normal_subgroup_rel.is_normal23,565
-  abbreviation subgroup_to_relgroup.subgroup_to_rel27,725
-  definition is_reflexive_Rgroup.free_comm_group.is_reflexive_R452,16904
-  structure cases_ongroup.normal_subgroup_rel.cases_on23,565
-  | rflipgroup.free_comm_group.fcg_rel.rflip438,16378
-  definition product_invgroup.product_inv227,8704
-  structure Ronegroup.subgroup_rel.Rone17,410
-  | cancel2group.free_comm_group.fcg_rel.cancel2437,16334
-  inductive free_group_relgroup.free_group.free_group_rel274,10175
-  definition group_sggroup.group_sg98,3680
-  definition subgroup_invgroup.subgroup_inv69,2861
-  theorem rel_respect_reversegroup.free_group.rel_respect_reverse305,11444
-    inductive dirsum_relgroup.dirsum_rel.rec643,23866
-  definition quotient_groupgroup.quotient_group214,8177
-  definition free_group_mulgroup.free_group.free_group_mul319,12069
-    definition dirsum_carriergroup.dirsum_carrier641,23724
-    inductive rec_ongroup.generating_relation'.rec_on611,22688
-  structure destructgroup.normal_subgroup_rel.destruct23,565
-    inductive generating_relation'group.generating_relation'611,22688
-  theorem quotient_mul_commgroup.quotient_mul_comm199,7679
-  theorem kernel_invgroup.kernel_inv690,25493
-  inductive rec_ongroup.free_group.free_group_rel.rec_on274,10175
-  theorem free_group_one_mulgroup.free_group.free_group_one_mul336,12637
-  theorem rel_respect_flipgroup.free_comm_group.rel_respect_flip457,17078
-  inductive free_group_relgroup.free_group.free_group_rel.rec274,10175
-    inductive cases_ongroup.generating_relation'.cases_on611,22688
-  definition fcg_invgroup.free_comm_group.fcg_inv489,18234
-  theorem subgroup_mul_commgroup.subgroup_mul_comm91,3530
-    inductive rec_ongroup.dirsum_rel.rec_on643,23866
-  definition fcg_onegroup.free_comm_group.fcg_one488,18177
-  structure rec_ongroup.subgroup_rel.rec_on17,410
-  theorem subgroup_mul_left_invgroup.subgroup_mul_left_inv88,3442
-  theorem fcg_mul_left_invgroup.free_comm_group.fcg_mul_left_inv521,19267
-  theorem rel_respect_flipgroup.free_group.rel_respect_flip295,11073
-  | rreflgroup.free_group.free_group_rel.rrefl275,10234
-    inductive generating_relation'group.generating_relation'.rec611,22688
-  theorem quotient_one_mulgroup.quotient_one_mul181,7202
-  definition quotient_invgroup.quotient_inv162,6543
-  theorem is_equivalence_quotient_relgroup.is_equivalence_quotient_rel150,6091
-  theorem free_group_mul_onegroup.free_group.free_group_mul_one342,12802
-  theorem is_normal_subgroup_revgroup.is_normal_subgroup_rev45,1563
-  structure no_confusiongroup.normal_subgroup_rel.no_confusion23,565
-  structure subgroup_relgroup.subgroup_rel17,410
-  definition group_free_groupgroup.group_free_group367,13543
-    | ronegroup.generating_relation'.rone615,22950
-  theorem fcg_mul_onegroup.free_comm_group.fcg_mul_one515,19108
-  abbreviation subgroup_respect_invgroup.subgroup_respect_inv30,929
-  definition free_group_hom_equiv_fngroup.free_group_hom_equiv_fn417,15520
-  inductive cases_ongroup.free_comm_group.fcg_rel.cases_on434,16208
-  theorem subgroup_mul_onegroup.subgroup_mul_one85,3366
-  definition comm_productgroup.comm_product265,9929
-  definition subgroup_mulgroup.subgroup_mul71,2957
-  structure cases_ongroup.subgroup_rel.cases_on17,410
-  definition quotient_mulgroup.quotient_mul164,6665
-
-homotopy/fin.hlean,557
-  definition my_succfin.my_succ30,720
-inductive is_succis_succ.rec13,236
-  definition has_one_finfin.has_one_fin46,1254
-  protected definition addfin.add40,1035
-  definition has_add_finfin.has_add_fin49,1401
-definition is_succ_bit0is_succ_bit024,585
-inductive rec_onis_succ.rec_on13,236
-inductive is_succis_succ13,236
-| mkis_succ.mk14,268
-definition is_succ_add_rightis_succ_add_right18,339
-inductive cases_onis_succ.cases_on13,236
-  definition has_zero_finfin.has_zero_fin43,1114
-definition is_succ_add_leftis_succ_add_left21,460
-
-group_theory/basic.hlean,2779
-  definition to_respect_mulgroup.to_respect_mul94,3090
-  definition structgroup.homomorphism.struct88,2858
-    mkgroup.homomorphism.mk82,2703
-  definition comm_group_Group_of_CommGroupgroup.comm_group_Group_of_CommGroup30,953
-  definition is_homomorphism_idgroup.is_homomorphism_id76,2559
-  theorem to_respect_invgroup.to_respect_inv100,3245
-  definition to_ginvgroup.to_ginv151,5068
-  definition Set_of_Groupgroup.Set_of_Group25,788
-  theorem respect_onegroup.respect_one51,1730
-  definition pointed_Groupgroup.pointed_Group23,631
-  definition precategory_groupgroup.precategory_group183,6085
-  definition Group_of_CommGroupgroup.Group_of_CommGroup27,853
-  structure destructgroup.homomorphism.destruct81,2660
-  structure no_confusiongroup.homomorphism.no_confusion81,2660
-  definition reflgroup.isomorphism.refl158,5270
-  definition is_set_homomorphismgroup.is_set_homomorphism106,3462
-  structure to_homgroup.isomorphism.to_hom140,4744
-    mkgroup.isomorphism.mk141,4777
-  theorem to_respect_onegroup.to_respect_one97,3182
-  structure isomorphismgroup.isomorphism.rec140,4744
-  definition transgroup.isomorphism.trans164,5502
-  definition is_embedding_homomorphismgroup.is_embedding_homomorphism61,2062
-  structure homomorphismgroup.homomorphism81,2660
-  definition pmap_of_homomorphismgroup.pmap_of_homomorphism120,3991
-  definition homomorphism_composegroup.homomorphism_compose131,4395
-  theorem respect_invgroup.respect_inv58,1922
-  definition group_fungroup.group_fun87,2794
-  structure rec_ongroup.homomorphism.rec_on81,2660
-  structure φgroup.homomorphism.φ81,2660
-  definition homomorphism_eqgroup.homomorphism_eq123,4120
-  definition to_is_embedding_homomorphismgroup.to_is_embedding_homomorphism103,3330
-  definition equiv_of_isomorphismgroup.equiv_of_isomorphism148,4976
-  structure no_confusiongroup.isomorphism.no_confusion140,4744
-  definition symmgroup.isomorphism.symm161,5378
-  structure destructgroup.isomorphism.destruct140,4744
-  definition is_homomorphismgroup.is_homomorphism39,1242
-  structure rec_ongroup.isomorphism.rec_on140,4744
-  structure is_equiv_to_homgroup.isomorphism.is_equiv_to_hom140,4744
-  structure isomorphismgroup.isomorphism140,4744
-  definition homomorphism_idgroup.homomorphism_id134,4544
-  structure homomorphismgroup.homomorphism.rec81,2660
-  definition group_pType_of_Groupgroup.group_pType_of_Group34,1108
-  definition respect_mulgroup.respect_mul48,1643
-  definition pType_of_Groupgroup.pType_of_Group24,711
-  structure cases_ongroup.homomorphism.cases_on81,2660
-  definition is_homomorphism_composegroup.is_homomorphism_compose72,2369
-  structure pgroup.homomorphism.p81,2660
-  structure cases_ongroup.isomorphism.cases_on140,4744
-
-homotopy/join_theorem.hlean,366
-    protected definition introis_conn.intro51,1299
-  definition is_retraction_composeretraction.is_retraction_compose11,231
-  definition is_retraction_compose_equiv_leftretraction.is_retraction_compose_equiv_left27,703
-theorem is_conn_joinis_conn_join70,1667
-  definition is_retraction_compose_equiv_rightretraction.is_retraction_compose_equiv_right32,871
-
-homotopy/sec86.hlean,1825
-definition freudenthal_pequivfreudenthal_pequiv223,8078
-  definition encode'freudenthal.encode'121,4379
-  definition code_merid_inv_ptfreudenthal.code_merid_inv_pt92,3441
-  definition upfreudenthal.up58,2252
-  definition decodefreudenthal.decode174,6391
-  definition decode_north_ptfreudenthal.decode_north_pt115,4165
-  definition decode_coh_gfreudenthal.decode_coh_g148,5307
-  definition psphere_succpsphere_succ47,1992
-  theorem elim_type_merid_invelim_type_merid_inv36,1519
-  definition decode_northfreudenthal.decode_north112,4042
-  theorem decode_cohfreudenthal.decode_coh160,5802
-  definition code_merid_cohfreudenthal.code_merid_coh76,2843
-  definition equiv'freudenthal.equiv'188,6798
-  definition decode_coh_lemfreudenthal.decode_coh_lem156,5625
-definition freudenthal_equivfreudenthal_equiv229,8371
-  definition is_trunc_codefreudenthal.is_trunc_code103,3823
-  definition code_meridfreudenthal.code_merid61,2360
-  theorem encode_decode_northfreudenthal.encode_decode_north130,4628
-  definition is_equiv_code_meridfreudenthal.is_equiv_code_merid81,3004
-  definition is_conn_truncis_conn_trunc40,1776
-  definition pequiv'freudenthal.pequiv'191,6935
-  definition decode_southfreudenthal.decode_south118,4253
-  definition encodefreudenthal.encode124,4469
-  definition decode_coh_ffreudenthal.decode_coh_f139,4992
-  definition code_merid_β_leftfreudenthal.code_merid_β_left70,2625
-  definition stability_pequivsphere.stability_pequiv236,8573
-  definition code_merid_equivfreudenthal.code_merid_equiv89,3312
-  definition codefreudenthal.code100,3704
-  theorem decode_encodefreudenthal.decode_encode182,6599
-  definition code_merid_β_rightfreudenthal.code_merid_β_right73,2727
-  definition iterated_loop_ptrunc_pequiv_coniterated_loop_ptrunc_pequiv_con23,1032
-
-homotopy/chain_complex.hlean,5324
-definition sintsint36,1114
-structure carriersucc_str.carrier24,757
-  structure mul_left_inv_ptchain_complex.pgroup.mul_left_inv_pt478,19042
-  structure type_chain_complexchain_complex.type_chain_complex88,3028
-  definition transfer_chain_complex2'chain_complex.transfer_chain_complex2'336,12565
-  structure invchain_complex.pgroup.inv478,19042
-structure no_confusionsucc_str.no_confusion24,757
-  definition cc_to_fnchain_complex.cc_to_fn248,9540
-  definition transfer_chain_complexchain_complex.transfer_chain_complex280,10737
-definition stratifiedstratified57,1945
-  structure cases_onchain_complex.chain_complex.cases_on239,9213
-  definition is_exact_at_tchain_complex.is_exact_at_t103,3692
-  definition whisker_left_idp_con_eq_assoceq.whisker_left_idp_con_eq_assoc17,554
-  structure pgroupchain_complex.pgroup478,19042
-definition stratified_succstratified_succ53,1777
-definition snatsnat34,955
-  definition cast_inv_castchain_complex.cast_inv_cast178,6596
-  definition cast_cast_invchain_complex.cast_cast_inv174,6433
-  definition is_surjective_of_trivialchain_complex.is_surjective_of_trivial516,20301
-structure succ_strsucc_str.rec24,757
-  structure destructchain_complex.type_chain_complex.destruct88,3028
-  theorem is_exact_at_transferchain_complex.is_exact_at_transfer292,11186
-  structure is_set_carrierchain_complex.pgroup.is_set_carrier478,19042
-  structure to_has_invchain_complex.pgroup.to_has_inv478,19042
-  definition inv_commute1'chain_complex.inv_commute1'162,5796
-  mksucc_str.mk25,778
-  definition is_exact_tchain_complex.is_exact_t106,3821
-  structure cases_onchain_complex.type_chain_complex.cases_on88,3028
-  definition tcc_to_carchain_complex.tcc_to_car96,3299
-structure succsucc_str.succ24,757
-  structure fnchain_complex.chain_complex.fn239,9213
-    mkchain_complex.chain_complex.mk240,9256
-  structure mul_assocchain_complex.pgroup.mul_assoc478,19042
-  definition is_exact_at_truncchain_complex.is_exact_at_trunc324,12208
-  definition is_embedding_of_trivialchain_complex.is_embedding_of_trivial501,19848
-  definition cc_to_carchain_complex.cc_to_car247,9473
-  definition inv_commute1chain_complex.inv_commute1166,6045
-  definition is_equiv_of_trivialchain_complex.is_equiv_of_trivial524,20541
-  definition is_exact_at_transfer2chain_complex.is_exact_at_transfer2201,7632
-  definition transfer_type_chain_complexchain_complex.transfer_type_chain_complex130,4624
-  structure rec_onchain_complex.pgroup.rec_on478,19042
-  definition fn_cast_eq_cast_fnchain_complex.fn_cast_eq_cast_fn170,6235
-  definition is_exact_atchain_complex.is_exact_at254,9852
-  structure carchain_complex.type_chain_complex.car88,3028
-definition stratified_typestratified_type44,1365
-  structure cases_onchain_complex.pgroup.cases_on478,19042
-  structure destructchain_complex.pgroup.destruct478,19042
-  definition is_exact_at_transfer2'chain_complex.is_exact_at_transfer2'357,13539
-    mkchain_complex.type_chain_complex.mk89,3076
-  definition trunc_chain_complexchain_complex.trunc_chain_complex312,11842
-  definition is_exactchain_complex.is_exact257,9977
-  definition tcc_is_chain_complexchain_complex.tcc_is_chain_complex98,3453
-definition sint'sint'37,1193
-  structure is_chain_complexchain_complex.chain_complex.is_chain_complex239,9213
-  definition group_of_pgroupchain_complex.group_of_pgroup483,19228
-  structure chain_complexchain_complex.chain_complex239,9213
-  structure chain_complexchain_complex.chain_complex.rec239,9213
-  definition cc_is_chain_complexchain_complex.cc_is_chain_complex249,9618
-  structure type_chain_complexchain_complex.type_chain_complex.rec88,3028
-  structure no_confusionchain_complex.type_chain_complex.no_confusion88,3028
-definition snat'snat'35,1034
-  structure destructchain_complex.chain_complex.destruct239,9213
-  structure mul_ptchain_complex.pgroup.mul_pt478,19042
-  structure pgroupchain_complex.pgroup.rec478,19042
-  structure carchain_complex.chain_complex.car239,9213
-  structure fnchain_complex.type_chain_complex.fn88,3028
-definition Ssucc_str.S30,875
-  structure is_chain_complexchain_complex.type_chain_complex.is_chain_complex88,3028
-  structure mulchain_complex.pgroup.mul478,19042
-structure cases_onsucc_str.cases_on24,757
-  definition transfer_type_chain_complex2chain_complex.transfer_type_chain_complex2183,6842
-    mkchain_complex.pgroup.mk479,19107
-  definition pgroup_of_groupchain_complex.pgroup_of_group491,19482
-structure rec_onsucc_str.rec_on24,757
-  definition tcc_to_fnchain_complex.tcc_to_fn97,3372
-  structure rec_onchain_complex.type_chain_complex.rec_on88,3028
-  structure no_confusionchain_complex.pgroup.no_confusion478,19042
-  theorem is_exact_at_t_transferchain_complex.is_exact_at_t_transfer142,5091
-  structure rec_onchain_complex.chain_complex.rec_on239,9213
-structure succ_strsucc_str24,757
-  definition is_trunc_ptrunctypechain_complex.is_trunc_ptrunctype473,18817
-  structure to_semigroupchain_complex.pgroup.to_semigroup478,19042
-structure destructsucc_str.destruct24,757
-  definition transport_eq_Fl_idp_lefteq.transport_eq_Fl_idp_left13,386
-  structure no_confusionchain_complex.chain_complex.no_confusion239,9213
-  structure pt_mulchain_complex.pgroup.pt_mul478,19042
-
-homotopy/spectrum.hlean,5800
-structure is_spectrumis_spectrum.rec187,9094
-structure destructgen_spectrum.destruct192,9275
-  definition pequiv_postcomposepointed.pequiv_postcompose137,7133
-structure no_confusiongen_prespectrum.no_confusion181,8929
-structure gluegen_prespectrum.glue181,8929
-  structure cases_onspectrum.sp_chain_complex.cases_on386,18262
-  structure no_confusionspectrum.sp_chain_complex.no_confusion386,18262
-  definition pequiv_precomposepointed.pequiv_precompose145,7584
-  definition loop_pmap_commutepointed.loop_pmap_commute73,2970
-abbreviation mkspectrum.mk203,9684
-  definition psp_of_gen_indexedspectrum.psp_of_gen_indexed248,11436
-  structure shomotopyspectrum.shomotopy317,15315
-  structure shomotopyspectrum.shomotopy.rec317,15315
-structure destructgen_prespectrum.destruct181,8929
-  structure fnspectrum.sp_chain_complex.fn386,18262
-    definition scc_to_carspectrum.scc_to_car394,18517
-  structure sp_chain_complexspectrum.sp_chain_complex386,18262
-  structure carspectrum.sp_chain_complex.car386,18262
-  protected definition of_gen_indexedspectrum.of_gen_indexed257,11975
-  definition shomotopy_groupspectrum.shomotopy_group356,16961
-structure cases_onis_spectrum.cases_on187,9094
-structure cases_ongen_spectrum.cases_on192,9275
-  structure rec_onspectrum.sp_chain_complex.rec_on386,18262
-  mkgen_prespectrum.mk182,8965
-  definition ppcompose_leftpointed.ppcompose_left82,3567
-structure no_confusionis_spectrum.no_confusion187,9094
-  definition scomposespectrum.scompose299,14044
-structure to_prespectrumgen_spectrum.to_prespectrum192,9275
-  structure no_confusionspectrum.smap.no_confusion278,13041
-  definition szerospectrum.szero311,14839
-  structure cases_onspectrum.smap.cases_on278,13041
-structure gen_prespectrumgen_prespectrum.rec181,8929
-  structure no_confusionspectrum.shomotopy.no_confusion317,15315
-abbreviation spectrumspectrum202,9643
-  structure cases_onspectrum.shomotopy.cases_on317,15315
-    definition scc_is_chain_complexspectrum.scc_is_chain_complex396,18670
-  definition struncspectrum.strunc343,16403
-  structure glue_squarespectrum.smap.glue_square278,13041
-structure destructis_spectrum.destruct187,9094
-  structure smapspectrum.smap.rec278,13041
-  definition pfiber_loop_spacepointed.pfiber_loop_space110,5185
-  definition pequiv_composepointed.pequiv_compose35,1119
-  definition psuspnspectrum.psuspn330,15866
-  definition pmap_eq_equivpointed.pmap_eq_equiv58,1870
-structure deloopgen_prespectrum.deloop181,8929
-  structure rec_onspectrum.shomotopy.rec_on317,15315
-  definition transport_fiber_equivpointed.transport_fiber_equiv132,6798
-  definition pcompose_pconstpointed.pcompose_pconst101,4763
-  mkis_spectrum.mk188,9158
-  definition sglue_squarespectrum.sglue_square288,13371
-  definition equiv_ppcompose_leftpointed.equiv_ppcompose_left98,4631
-  definition ap1_pconstpointed.ap1_pconst107,5048
-  definition ppipointed.ppi160,8279
-  structure glue_homotopyspectrum.shomotopy.glue_homotopy317,15315
-structure rec_ongen_spectrum.rec_on192,9275
-  definition sigma_equiv_sigma_left'sigma.sigma_equiv_sigma_left'20,711
-  definition is_spectrum_of_gen_indexedspectrum.is_spectrum_of_gen_indexed251,11679
-  structure to_funspectrum.smap.to_fun278,13041
-  definition pfiber_equiv_of_phomotopypointed.pfiber_equiv_of_phomotopy121,6291
-  structure destructspectrum.sp_chain_complex.destruct386,18262
-structure gen_spectrumgen_spectrum.rec192,9275
-  protected definition of_nat_indexedspectrum.of_nat_indexed237,10937
-  protected definition MKspectrum.MK262,12282
-  definition equiv_ppi_rightpointed.equiv_ppi_right166,8498
-    definition scc_to_fnspectrum.scc_to_fn395,18590
-structure rec_onis_spectrum.rec_on187,9094
-  structure destructspectrum.shomotopy.destruct317,15315
-structure gen_prespectrumgen_prespectrum181,8929
-  definition is_spectrum_of_nat_indexedspectrum.is_spectrum_of_nat_indexed230,10636
-  protected definition Mkspectrum.Mk270,12731
-  definition equiv_gluespectrum.equiv_glue209,9865
-    mkspectrum.smap.mk279,13094
-  mkgen_spectrum.mk193,9308
-structure is_equiv_glueis_spectrum.is_equiv_glue187,9094
-  definition gluespectrum.glue207,9753
-  definition sigma_charpointed.phomotopy.sigma_char49,1559
-  structure sp_chain_complexspectrum.sp_chain_complex.rec386,18262
-  structure smapspectrum.smap278,13041
-    mkspectrum.shomotopy.mk318,15388
-structure gen_spectrumgen_spectrum192,9275
-  definition psp_suspspectrum.psp_susp335,16065
-structure is_spectrumis_spectrum187,9094
-  structure is_chain_complexspectrum.sp_chain_complex.is_chain_complex386,18262
-structure cases_ongen_prespectrum.cases_on181,8929
-  definition sfiberspectrum.sfiber382,18050
-  definition of_natspectrum.succ_str.of_nat244,11289
-  definition pathover_eq_Fl'eq.pathover_eq_Fl'28,913
-structure rec_ongen_prespectrum.rec_on181,8929
-  definition pconst_pcomposepointed.pconst_pcompose104,4907
-structure no_confusiongen_spectrum.no_confusion192,9275
-  structure rec_onspectrum.smap.rec_on278,13041
-    mkspectrum.sp_chain_complex.mk387,18308
-  definition sp_cotensorspectrum.sp_cotensor366,17352
-  definition pfiber_equiv_of_squarepointed.pfiber_equiv_of_square154,7944
-  structure destructspectrum.smap.destruct278,13041
-  definition loop_ppi_commutepointed.loop_ppi_commute163,8361
-  definition sidspectrum.sid293,13688
-  structure to_phomotopyspectrum.shomotopy.to_phomotopy317,15315
-structure to_is_spectrumgen_spectrum.to_is_spectrum192,9275
-  definition psp_of_nat_indexedspectrum.psp_of_nat_indexed216,10207
-  definition spispectrum.spi374,17699
-  definition sigma_charpointed.pmap.sigma_char40,1292
-  definition is_equiv_ppcompose_leftpointed.is_equiv_ppcompose_left85,3741
-
-algebra/module.hlean,3083
-mkleft_module.mk22,563
-structure destructleft_module.destruct20,467
-structure cases_onvector_space.cases_on72,2518
-  proposition smul_zerosmul_zero50,1651
-structure rec_onleft_module.rec_on20,467
-structure mul_smulleft_module.mul_smul20,467
-  proposition neg_one_smulneg_one_smul57,1961
-structure has_scalarhas_scalar13,339
-structure smul_left_distribvector_space.smul_left_distrib72,2518
-structure add_zerovector_space.add_zero72,2518
-structure cases_onhas_scalar.cases_on13,339
-  proposition one_smulone_smul44,1413
-structure zero_addleft_module.zero_add20,467
-structure rec_onhas_scalar.rec_on13,339
-structure smulvector_space.smul72,2518
-structure addvector_space.add72,2518
-structure smul_left_distribleft_module.smul_left_distrib20,467
-structure left_moduleleft_module.rec20,467
-  proposition mul_smulmul_smul41,1310
-  proposition smul_left_distribsmul_left_distrib35,1074
-structure destructhas_scalar.destruct13,339
-structure smulleft_module.smul20,467
-structure negleft_module.neg20,467
-structure vector_spacevector_space72,2518
-  proposition smul_negsmul_neg60,2054
-structure one_smulleft_module.one_smul20,467
-structure is_set_carrierleft_module.is_set_carrier20,467
-structure left_moduleleft_module20,467
-structure no_confusionleft_module.no_confusion20,467
-  proposition neg_smulneg_smul54,1811
-structure no_confusionhas_scalar.no_confusion13,339
-structure destructvector_space.destruct72,2518
-structure add_commvector_space.add_comm72,2518
-structure mkvector_space.mk72,2518
-structure zero_addvector_space.zero_add72,2518
-structure zerovector_space.zero72,2518
-structure add_zeroleft_module.add_zero20,467
-structure smul_right_distribvector_space.smul_right_distrib72,2518
-  proposition zero_smulzero_smul46,1488
-structure vector_spacevector_space.rec72,2518
-structure negvector_space.neg72,2518
-structure has_scalarhas_scalar.rec13,339
-structure add_assocvector_space.add_assoc72,2518
-structure one_smulvector_space.one_smul72,2518
-structure add_assocleft_module.add_assoc20,467
-  proposition sub_smul_right_distribsub_smul_right_distrib66,2336
-structure zeroleft_module.zero20,467
-structure smul_right_distribleft_module.smul_right_distrib20,467
-  proposition smul_right_distribsmul_right_distrib38,1191
-structure add_commleft_module.add_comm20,467
-structure is_set_carriervector_space.is_set_carrier72,2518
-structure add_left_invvector_space.add_left_inv72,2518
-structure cases_onleft_module.cases_on20,467
-structure rec_onvector_space.rec_on72,2518
-structure no_confusionvector_space.no_confusion72,2518
-  proposition smul_sub_left_distribsmul_sub_left_distrib63,2189
-structure smulhas_scalar.smul13,339
-structure to_add_comm_groupleft_module.to_add_comm_group20,467
-structure mul_smulvector_space.mul_smul72,2518
-structure add_left_invleft_module.add_left_inv20,467
-mkhas_scalar.mk14,374
-structure addleft_module.add20,467
-structure to_left_modulevector_space.to_left_module72,2518
-structure to_has_scalarleft_module.to_has_scalar20,467
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index b2ae55b..5d514f0 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -123,11 +123,12 @@ namespace group
     (is_normal_subgroup : is_normal R)
 
   attribute subgroup_rel.R [coercion]
-  abbreviation subgroup_to_rel      [unfold 2] := @subgroup_rel.R
-  abbreviation subgroup_has_one     [unfold 2] := @subgroup_rel.Rone
-  abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul
-  abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv
-  abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
+  abbreviation subgroup_to_rel      [parsing_only] [unfold 2] := @subgroup_rel.R
+  abbreviation subgroup_has_one     [parsing_only] [unfold 2] := @subgroup_rel.Rone
+  abbreviation subgroup_respect_mul [parsing_only] [unfold 2] := @subgroup_rel.Rmul
+  abbreviation subgroup_respect_inv [parsing_only] [unfold 2] := @subgroup_rel.Rinv
+  abbreviation is_normal_subgroup   [parsing_only] [unfold 2] :=
+  @normal_subgroup_rel.is_normal_subgroup
 
   variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
             {A B : CommGroup}
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index c7cc0e3..7d6e2fc 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -6,9 +6,9 @@
   However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B.
 -/
 
-import homotopy.circle homotopy.join types.pointed ..move_to_lib
+import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib
 
-open bool pointed eq equiv is_equiv sum bool prod unit circle
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber
 
 namespace smash
 
@@ -181,6 +181,38 @@ namespace smash
 
   /- To prove: commutative, associative -/
 
+  /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
+
+  definition prod_of_pwedge [unfold 3] (v : pwedge A B) : A × B :=
+  begin
+    induction v with a b ,
+    { exact (a, pt) },
+    { exact (pt, b) },
+    { reflexivity }
+  end
+
+  definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
+  begin
+    fconstructor,
+    { intro v, induction v with a b ,
+      { exact (a, pt) },
+      { exact (pt, b) },
+      { reflexivity }},
+    { reflexivity }
+  end
+
+  attribute pcofiber [constructor]
+  definition pcofiber_of_smash (x : smash A B) : pcofiber (@pprod_of_pwedge A B) :=
+  begin
+    induction x,
+    { exact pushout.inr (a, b) },
+    { exact pushout.inl ⋆ },
+    { exact pushout.inl ⋆ },
+    { symmetry, },
+    { }
+  end
+
+
   /- smash A S¹ = susp A -/
   open susp
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 4243431..6de864b 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -7,7 +7,7 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 
 attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose
           fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in
-          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv
+          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ
           [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
 attribute isomorphism._trans_of_to_hom [unfold 3]
@@ -25,6 +25,21 @@ open sigma
 namespace group
   open is_trunc
 
+  -- some extra instances for type class inference
+  definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G))
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' _
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ :=
+  homomorphism.struct φ
+
   theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 :=
   iff.mpr (inv_eq_one_iff_eq_one a) H
 
