fact: Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G) : H1 = H2 -> GroupIsomorphism H1 H2 := ltac:(intros []; exact grp_iso_id).
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType