diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
index f4e518fcf3..3a5f075ecb 100644
--- a/theories/Algebra/AbGroups/AbPushout.v
+++ b/theories/Algebra/AbGroups/AbPushout.v
@@ -123,7 +123,7 @@ Definition path_ab_pushout `{Univalence} {A B C : AbGroup} (f : A $-> B) (g : A
   : @in_cosetL (ab_biprod B C) (ab_pushout_subgroup f g) bc0 bc1
                <~> (grp_quotient_map bc0 = grp_quotient_map bc1 :> ab_pushout f g).
 Proof.
-  rapply path_quotient.
+  nrapply path_quotient; exact _.
 Defined.
 
 (** The pushout of an embedding is an embedding. *)
diff --git a/theories/Algebra/Groups/Commutator.v b/theories/Algebra/Groups/Commutator.v
index 7e5ae6afcf..f44b791f73 100644
--- a/theories/Algebra/Groups/Commutator.v
+++ b/theories/Algebra/Groups/Commutator.v
@@ -1,8 +1,9 @@
-Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
-Require Import Types.Sigma.
+Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
+  Basics.Iff Basics.Equivalences.
+Require Import Types.Sigma Types.Paths.
 Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
   Groups.QuotientGroup.
-Require Import WildCat.Core WildCat.EquivGpd.
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd.
 Require Import Truncations.Core.
 
 Local Open Scope mc_scope.
@@ -156,7 +157,7 @@ Proof.
   apply grp_inv_r.
 Defined.
 
-(** This variant of the Hall-Witt identity is useful later for proving the three subgroups lemma. *)  
+(** This variant of the Hall-Witt identity is useful later for proving the three subgroups lemma. *)
 Definition grp_hall_witt' {G : Group} (x y z : G)
   : grp_conj x [[x^, y], z] * grp_conj z [[z^, x], y] * grp_conj y [[y^, z], x] = 1.
 Proof.
@@ -167,7 +168,7 @@ Defined.
 
 (** ** Precomposing normal subgroups with commutators *)
 
-Global Instance issubgroup_precomp_commutator {G : Group} (H : Subgroup G)
+Global Instance issubgroup_precomp_commutator_l {G : Group} (H : Subgroup G)
   `{!IsNormalSubgroup H} (y : G)
   : IsSubgroup (fun x => H [x, y]).
 Proof.
@@ -187,11 +188,28 @@ Proof.
     by apply subgroup_in_inv.
 Defined.
 
-Definition subgroup_precomp_commutator {G : Group} (H : Subgroup G) (y : G)
+Global Instance issubgroup_precomp_commutator_r {G : Group} (H : Subgroup G)
+  `{!IsNormalSubgroup H} (x : G)
+  : IsSubgroup (fun y => H [x, y]).
+Proof.
+  snrapply issubgroup_equiv.
+  - exact (fun y => H [y, x]^).
+  - intros y; cbn beta.
+    by rewrite grp_commutator_inv.
+  - exact (issubgroup_precomp_commutator_l
+      (subgroup_preimage (grp_op_iso_inv G) (subgroup_grp_op H)) x).
+Defined.
+
+Definition subgroup_precomp_commutator_l {G : Group} (H : Subgroup G) (y : G)
   `{!IsNormalSubgroup H}
   : Subgroup G
   := Build_Subgroup _ (fun x => H [x, y]) _.
 
+Definition subgroup_precomp_commutator_r {G : Group} (H : Subgroup G) (x : G)
+  `{!IsNormalSubgroup H}
+  : Subgroup G
+  := Build_Subgroup _ (fun y => H [x, y]) _.
+
 (** ** Commutator subgroups *)
 
 Definition subgroup_commutator {G : Group@{i}} (H K : Subgroup@{i i} G)
@@ -220,11 +238,76 @@ Definition subgroup_commutator_2_rec {G : Group} {H J K : Subgroup G}
 Proof.
   snrapply subgroup_commutator_rec.
   intros x z HJx Kz; revert x HJx.
-  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator N z x).
+  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator_l N z x).
   rapply subgroup_commutator_rec.
   by intros; apply i.
 Defined.
 
+(** A commutator of elements from each respective subgroup is in the commutator subgroup. *)
+Definition subgroup_commutator_in {G : Group} {H J : Subgroup G} {x y : G}
+  (Hx : H x) (Jy : J y)
+  : subgroup_commutator H J (grp_commutator x y).
+Proof.
+  apply tr, sgt_in.
+  by exists (x; Hx), (y; Jy).
+Defined.
+
+(** Commutator subgroups are functorial. *)
+Definition functor_subgroup_commutator {G : Group} {H J K L : Subgroup G}
+  (f : forall x, H x -> K x) (g : forall x, J x -> L x)
+  : forall x, [H, J] x -> [K, L] x.
+Proof.
+  snrapply subgroup_commutator_rec.
+  intros x y Hx Jx.
+  apply subgroup_commutator_in.
+  - by apply f.
+  - by apply g.
+Defined.
+
+Definition subgroup_eq_commutator {G : Group} {H J K L : Subgroup G}
+  (f : forall x, H x <-> K x) (g : forall x, J x <-> L x)
+  : forall x, [H, J] x <-> [K, L] x.
+Proof.
+  intros x; split; revert x; apply functor_subgroup_commutator.
+  1,3: apply f.
+  1,2: apply g.
+Defined.
+
+(** Commutator subgroups are symmetric in their arguments. *)
+Definition subgroup_commutator_symm {G : Group} (H J : Subgroup G)
+  : forall x, [H, J] x <-> [J, H] x.
+Proof.
+  intros x; split; revert x; snrapply subgroup_commutator_rec.
+  - intros x y Hx Jy.
+    nrapply subgroup_in_inv'.
+    rewrite grp_commutator_inv.
+    by apply subgroup_commutator_in.
+  - intros x y Jy Hx.
+    nrapply subgroup_in_inv'.
+    rewrite grp_commutator_inv.
+    by apply subgroup_commutator_in.
+Defined.
+
+(** The opposite subgroup of a commutator subgroup is the commutator subgroup of the opposite subgroups. *)
+Definition subgroup_eq_commutator_grp_op {G : Group} (H J : Subgroup G)
+  : forall (x : grp_op G), subgroup_grp_op [H, J] x
+    <-> [subgroup_grp_op H, subgroup_grp_op J] x.
+Proof.
+  intros x.
+  nrapply (iff_compose
+    (subgroup_eq_functor_subgroup_generated _ _ (grp_op_iso_inv G) _ x)
+    (equiv_subgroup_inv _ _)^-1%equiv).
+  clear x; intros x.
+  do 2 (snrapply (equiv_functor_sigma'
+    (grp_iso_subgroup_group (grp_op_iso_inv G)
+      (equiv_subgroup_inv (G:=grp_op G) (subgroup_grp_op _)))); intro).
+  simpl.
+  refine (equiv_moveL_equiv_M _ _ oE _).
+  apply equiv_concat_l.
+  apply moveR_equiv_V; symmetry.
+  nrapply (grp_homo_commutator (grp_op_iso_inv _)).
+Defined.
+
 (** A commutator subgroup of an abelian group is always trivial. *)
 Definition istrivial_commutator_subgroup_ab {A : AbGroup} (H K : Subgroup A)
   : IsTrivialGroup [H, K].
@@ -233,28 +316,80 @@ Proof.
   rapply ab_commutator.
 Defined.
 
-(** ** Derived subgroup *)
-
-(** The commutator subgroup of the maximal subgroup with itself is called the derived subgroup. It is the subgroup generated by all commutators. *)
-
-(** The derived subgroup is a normal subgroup. *)
-Global Instance isnormal_subgroup_derived {G : Group}
-  : IsNormalSubgroup [G, G].
+(** A commutator of normal subgroups is normal. *)
+Global Instance isnormal_subgroup_commutator {G : Group} (H J : Subgroup G)
+  `{!IsNormalSubgroup H, !IsNormalSubgroup J}
+  : IsNormalSubgroup [H, J].
 Proof.
   snrapply Build_IsNormalSubgroup'.
   intros x y; revert x.
   apply (functor_subgroup_generated _ _ (grp_conj y)).
-  intros g.
-  snrapply (functor_sigma (functor_sigma (grp_conj y) (fun _ => idmap)));
-    cbn beta; intros [x []].
-  snrapply (functor_sigma (functor_sigma (grp_conj y) (fun _ => idmap)));
-    cbn beta; intros [z []].
-  intros p; simpl.
+  intros x.
+  do 2 (rapply (functor_sigma (grp_iso_normal_conj _ y)); intro).
+  intros p.
   lhs_V nrapply (grp_homo_commutator (grp_conj y)).
-  snrapply (ap (grp_conj y)).
-  exact p.
+  exact (ap (grp_conj y) p).
 Defined.
 
+(** Commutator subgroups distribute over products of normal subgroups on the left. *)
+Definition subgroup_commutator_normal_prod_l {G : Group}
+  (H K L : NormalSubgroup G)
+  : forall x, [subgroup_product H K, L] x <-> subgroup_product [H, L] [K, L] x.
+Proof.
+  intros x; split.
+  - revert x; snrapply subgroup_commutator_rec.
+    intros x y HKx Ly; revert x HKx.
+    change (subgroup_product ?H ?J (grp_commutator ?x y))
+      with (subgroup_precomp_commutator_l (subgroup_product H J) y x).
+    snrapply subgroup_generated_rec.
+    intros x [Hx | Kx].
+    + apply subgroup_product_incl_l.
+      by apply subgroup_commutator_in.
+    + apply subgroup_product_incl_r.
+      by apply subgroup_commutator_in.
+  - revert x; snrapply subgroup_generated_rec.
+    intros x [HLx | KLx].
+    + revert x HLx.
+      apply functor_subgroup_commutator; trivial.
+      apply subgroup_product_incl_l.
+    + revert x KLx.
+      apply functor_subgroup_commutator; trivial.
+      apply subgroup_product_incl_r.
+Defined.
+
+(** Commutator subgroups distribute over products of normal subgroups on the right. *)
+Definition subgroup_commutator_normal_prod_r {G : Group}
+  (H K L : NormalSubgroup G)
+  : forall x, [H, subgroup_product K L] x <-> subgroup_product [H, K] [H, L] x.
+Proof.
+  intros x.
+  etransitivity.
+  1: symmetry; apply subgroup_commutator_symm.
+  etransitivity.
+  2: nrapply (subgroup_eq_functor_subgroup_product grp_iso_id
+    (subgroup_commutator_symm _ _) (subgroup_commutator_symm _ _)).
+  exact (subgroup_commutator_normal_prod_l K L H x).
+Defined.
+
+(** The subgroup image of a commutator is included in the commutator of the subgroup images. The converse only generally holds for a normal [J] and [K] and a surjective [f]. *)
+Definition subgroup_image_commutator_incl {G H : Group}
+  (f : G $-> H) (J K : Subgroup G)
+  : forall x, subgroup_image f [J, K] x
+    -> [subgroup_image f J, subgroup_image f K] x.
+Proof.
+  snrapply subgroup_image_rec.
+  change ([?G, ?H] (f ?x)) with (subgroup_preimage f [G, H] x).
+  snrapply subgroup_commutator_rec.
+  intros x y Jx Ky.
+  change (subgroup_preimage f [?G, ?H] ?x) with ([G, H] (f x)).
+  rewrite grp_homo_commutator.
+  apply subgroup_commutator_in;
+    by apply subgroup_image_in.
+Defined.
+
+(** ** Derived subgroup *)
+
+(** The commutator subgroup of the maximal subgroup with itself is called the derived subgroup. It is the subgroup generated by all commutators. *)
 Definition normalsubgroup_derived G : NormalSubgroup G
   := Build_NormalSubgroup G [G, G] _.
 
@@ -279,7 +414,7 @@ Definition abgroup_derived_quotient (G : Group) : AbGroup
   := Build_AbGroup (grp_derived_quotient G) _.
 
 (** We get a recursion principle into abelian groups. *)
-Definition abgroup_derived_quotient_rec {G : Group} {A : AbGroup} (f : G $-> A) 
+Definition abgroup_derived_quotient_rec {G : Group} {A : AbGroup} (f : G $-> A)
   : abgroup_derived_quotient G $-> A.
 Proof.
   snrapply (grp_quotient_rec _ _ f).
@@ -329,8 +464,8 @@ Proof.
     apply tr, sgt_in.
     unshelve eexists.
     + exists [x^, y].
-      apply tr, sgt_in.
-      by exists (x^; subgroup_in_inv _ _ Hx), (y; Jy). 
+      apply subgroup_commutator_in; trivial.
+      by apply subgroup_in_inv.
     + by exists (z^; subgroup_in_inv _ _ Kz).
   - apply subgroup_in_inv.
     rapply isnormal_conj.
@@ -338,8 +473,8 @@ Proof.
     apply tr, sgt_in.
     unshelve eexists.
     + exists [y^, z^].
-      apply tr, sgt_in.
-      by exists (y^; subgroup_in_inv _ _ Jy), (z^; subgroup_in_inv _ _ Kz). 
+      apply subgroup_commutator_in;
+        by apply subgroup_in_inv.
     + by exists (x; Hx).
   Local Open Scope group_scope.
 Defined.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 3281b94a9e..7cea0351c5 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -892,6 +892,39 @@ Defined.
 Definition grp_homo_const {G H : Group} : GroupHomomorphism G H
   := zero_morphism.
 
+(** ** Opposite Group *)
+
+(** The opposite group of a group is the group with the same elements but with the group operation reversed. *)
+Definition grp_op : Group -> Group.
+Proof.
+  intros G.
+  snrapply Build_Group'.
+  - exact G.
+  - exact _.
+  - exact (flip (.*.)).
+  - exact 1.
+  - exact (^).
+  - intros x y z.
+    symmetry.
+    exact (grp_assoc z y x).
+  - intro x.
+    exact (grp_unit_r x).
+  - intro x.
+    exact (grp_inv_r x).
+Defined.
+
+(** Taking the inverse is an isomorphism from the group to the opposite group. *)
+Definition grp_op_iso_inv (G : Group)
+  : G $<~> (grp_op G).
+Proof.
+  snrapply Build_GroupIsomorphism.
+  - snrapply Build_GroupHomomorphism.
+    + exact inv.
+    + intros x y.
+      rapply grp_inv_op.
+  - simpl; exact _.
+Defined.
+
 (** ** The direct product of groups *)
 
 (** The cartesian product of the underlying sets of two groups has a natural group structure. We call this the direct product of groups. *)
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index f65f1c4555..7409262fa4 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -22,6 +22,9 @@ Class IsSubgroup {G : Group} (H : G -> Type) := {
 
 Global Existing Instance issubgroup_predicate.
 
+Definition issig_issubgroup {G : Group} (H : G -> Type) : _ <~> IsSubgroup H
+  := ltac:(issig).
+
 (** Basic properties of subgroups *)
 
 (** Smart constructor for subgroups.  *)
@@ -96,9 +99,6 @@ Section IsSubgroupElements.
 
 End IsSubgroupElements.
 
-Definition issig_issubgroup {G : Group} (H : G -> Type) : _ <~> IsSubgroup H
-  := ltac:(issig).
-
 (** Given a predicate H on a group G, being a subgroup is a property. *)
 Global Instance ishprop_issubgroup `{F : Funext} {G : Group} {H : G -> Type}
   : IsHProp (IsSubgroup H).
@@ -106,6 +106,27 @@ Proof.
   exact (istrunc_equiv_istrunc _ (issig_issubgroup H)).
 Defined.
 
+(** Transporting being a subgroup across a pointwise equivalence. *)
+Definition issubgroup_equiv {G : Group} {H K : G -> Type}
+  (p : forall g, H g <~> K g)
+  : IsSubgroup H -> IsSubgroup K.
+Proof.
+  intros H1.
+  snrapply Build_IsSubgroup.
+  - intros x.
+    snrapply (istrunc_equiv_istrunc (H x)).
+    1: apply p.
+    exact _.
+  - apply p, issubgroup_in_unit.
+  - intros x y.
+    equiv_intro (p x) Hx.
+    equiv_intro (p y) Hy.
+    exact (p _ (issubgroup_in_op x y Hx Hy)).
+  - intros x.
+    equiv_intro (p x) Hx.
+    exact (p _ (issubgroup_in_inv x Hx)).
+Defined.
+
 (** ** Definition of subgroup *) 
 
 (** The type (set) of subgroups of a group G. *)
@@ -269,7 +290,7 @@ Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H
   := subgroup_corec (grp_homo_restr f J) (sig_ind _ g).
 
 Definition grp_iso_subgroup_group {G H : Group@{i}}
-  {J : Subgroup@{i i} G} (K : Subgroup@{i i} H)
+  {J : Subgroup@{i i} G} {K : Subgroup@{i i} H}
   (e : G $<~> H) (f : forall x, J x <-> K (e x))
   : subgroup_group J $<~> subgroup_group K.
 Proof.
@@ -486,6 +507,17 @@ Proof.
     by snrapply Build_IsNormalSubgroup'.
 Defined.
 
+(** Inner automorphisms of a group [G] restrict to automorphisms of normal subgroups. *)
+Definition grp_iso_normal_conj {G : Group} (N : Subgroup G)
+  `{!IsNormalSubgroup N} (x : G)
+  : subgroup_group N $<~> subgroup_group N.
+Proof.
+  snrapply grp_iso_subgroup_group.
+  - exact (grp_iso_conj x).
+  - intros y.
+    rapply isnormal_conj.
+Defined.
+
 (** Left and right cosets are equivalent in normal subgroups. *)
 Definition equiv_in_cosetL_in_cosetR_normalsubgroup {G : Group}
   (N : NormalSubgroup G) (x y : G)
@@ -654,24 +686,62 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group}
   : IsMaximalSubgroup (maximal_subgroup G)
   := fun g => tt.
 
+(** ** Subgroups in opposite group *)
+
+Global Instance issubgroup_grp_op {G : Group} (H : G -> Type)
+  : IsSubgroup H -> IsSubgroup (G:=grp_op G) H.
+Proof.
+  intros H1.
+  snrapply Build_IsSubgroup'.
+  - exact _.
+  - cbn; rapply issubgroup_in_unit.
+  - intros x y Hx Hy; cbn.
+    by apply issubgroup_in_inv_op.
+Defined.
+
+Definition subgroup_grp_op {G : Group} (H : Subgroup G)
+  : Subgroup (grp_op G)
+  := Build_Subgroup (grp_op G) H _.
+
+Global Instance isnormal_subgroup_grp_op {G : Group} (H : Subgroup G)
+  : IsNormalSubgroup H -> IsNormalSubgroup (subgroup_grp_op H).
+Proof.
+  intros n x y; cbn.
+  apply isnormal.
+Defined.
+
+Definition normalsubgroup_grp_op {G : Group}
+  : NormalSubgroup G -> NormalSubgroup (grp_op G)
+  := fun N => Build_NormalSubgroup (grp_op G) (subgroup_grp_op N) _.
+
+Definition subgroup_eq_grp_op_op {G : Group} (H : Subgroup G)
+  : forall x, subgroup_grp_op (subgroup_grp_op H) x <-> H x.
+Proof.
+  reflexivity.
+Defined.
+
 (** ** Preimage subgroup *)
 
 (** The preimage of a subgroup under a group homomorphism is a subgroup. *)
-Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
-  : Subgroup G.
+Global Instance issubgroup_preimage {G H : Group} (f : G $-> H) (S : H -> Type)
+  : IsSubgroup S -> IsSubgroup (S o f).
 Proof.
-  snrapply Build_Subgroup'.
-  - exact (S o f).
+  intros H1.
+  snrapply Build_IsSubgroup'.
   - hnf; exact _.
   - nrefine (transport S (grp_homo_unit f)^ _).
-    apply subgroup_in_unit.
+    apply issubgroup_in_unit.
   - hnf; intros x y Sfx Sfy.
     nrefine (transport S (grp_homo_op f _ _)^ _).
-    nrapply subgroup_in_op; only 1: assumption.
+    rapply issubgroup_in_op; only 1: assumption.
     nrefine (transport S (grp_homo_inv f _)^ _).
-    by apply subgroup_in_inv.
+    by apply issubgroup_in_inv.
 Defined.
 
+Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
+  : Subgroup G
+  := Build_Subgroup G (S o f) _.
+
 (** The preimage of a normal subgroup is again normal. *)
 Global Instance isnormal_subgroup_preimage {G H : Group} (f : G $-> H)
   (N : Subgroup H) `{!IsNormalSubgroup N}
@@ -789,6 +859,23 @@ Proof.
   by apply preserves.
 Defined.
 
+Definition subgroup_eq_functor_subgroup_generated {G H : Group}
+  (X : G -> Type) (Y : H -> Type) (f : G $<~> H) (preserves : forall g, X g <-> Y (f g))
+  : forall g, subgroup_generated X g <-> subgroup_generated Y (f g).
+Proof.
+  intros x; split; revert x.
+  - apply functor_subgroup_generated.
+    apply preserves.
+  - equiv_intro f^-1$ x.
+    rewrite eisretr.
+    apply functor_subgroup_generated; clear x.
+    equiv_intro f x; intros y.
+    simpl; rewrite (eissect f).
+    by apply preserves.
+Defined.
+
+(** ** Product of subgroups *)
+
 (** The product of two subgroups. *)
 Definition subgroup_product {G : Group} (H K : Subgroup G) : Subgroup G
   := subgroup_generated (fun x => (H x + K x)%type).
@@ -837,6 +924,37 @@ Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G)
   : NormalSubgroup G
   := Build_NormalSubgroup G (subgroup_product H K) _.
 
+Definition functor_subgroup_product {G H : Group}
+  {J K : Subgroup G} {L M : Subgroup H}
+  (f : G $-> H) (l : forall x, J x -> L (f x)) (r : forall x, K x -> M (f x))
+  : forall x, subgroup_product J K x -> subgroup_product L M (f x).
+Proof.
+  snrapply functor_subgroup_generated.
+  exact (fun x => functor_sum (l x) (r x)).
+Defined.
+
+Definition subgroup_eq_functor_subgroup_product {G H : Group}
+  {J K : Subgroup G} {L M : Subgroup H}
+  (f : G $<~> H) (l : forall x, J x <-> L (f x)) (r : forall x, K x <-> M (f x))
+  : forall x, subgroup_product J K x <-> subgroup_product L M (f x).
+Proof.
+  snrapply subgroup_eq_functor_subgroup_generated.
+  exact (fun x => iff_functor_sum (l x) (r x)).
+Defined.
+
+Definition subgroup_eq_product_grp_op {G : Group} (H K : Subgroup G)
+  : forall x, subgroup_grp_op (subgroup_product H K) x
+    <-> subgroup_product (subgroup_grp_op H) (subgroup_grp_op K) x.
+Proof.
+  intros x.
+  nrapply (iff_compose
+    (subgroup_eq_functor_subgroup_generated _ _ (grp_op_iso_inv G) _ x)
+    (equiv_subgroup_inv _ _)^-1%equiv).
+  clear x; intros x.
+  snrapply equiv_functor_sum';
+    nrapply equiv_subgroup_inv.
+Defined.
+
 (** *** Paths between generated subgroups *)
 
 (** This gets used twice in [path_subgroup_generated], so we factor it out here. *)