Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
  Basics.Iff Basics.Equivalences.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma Types.Paths.
Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
  Groups.QuotientGroup.
Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd.
Require Import Truncations.Core.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

Set Universe Minimization ToSet.

(** Commutators in groups *)

(** ** Commutators of group elements *)

(** Note that this convention is chosen due to the convention we chose for group conjugation elsewhere. *)
Definition grp_commutator {G : Group} (x y : G) : G := x * y * x^ * y^.

Notation "[ x , y ]" := (grp_commutator x y) : mc_mult_scope.

Arguments grp_commutator {G} x y : simpl never.

(** ** Easy properties of commutators *)

(** Commuting elements of a group have trivial commutator. *)
Definition grp_commutator_commutes {G : Group} (x y : G) (p : x * y = y * x)
  : [x, y] = 1.
G: Group
x, y: G
p: x * y = y * x
[x, y] = 1
Proof.
G: Group
x, y: G
p: x * y = y * x
[x, y] = 1
  unfold grp_commutator.
G: Group
x, y: G
p: x * y = y * x
x * y * x^ * y^ = 1
  rewrite p, grp_inv_gg_V.
G: Group
x, y: G
p: x * y = y * x
y * y^ = 1
  apply grp_inv_r.
Defined.

(** A commutator of an element with itself is the unit. *)
Definition grp_commutator_cancel {G : Group} (x y : G)
  : [x, x] = 1.
G: Group
x, y: G
[x, x] = 1
Proof.
G: Group
x, y: G
[x, x] = 1
  by apply grp_commutator_commutes.
Defined.

(** A commutator of a group element with unit on the left is the unit. *)
Definition grp_commutator_unit_l {G : Group} (x : G)
  : [1, x] = 1.
G: Group
x: G
[1, x] = 1
Proof.
G: Group
x: G
[1, x] = 1
  by apply grp_commutator_commutes, grp_1g_g1.
Defined.

(** A commutator of a group element with unit on the right is the unit. *)
Definition grp_commutator_unit_r {G : Group} (x : G)
  : [x, 1] = 1.
G: Group
x: G
[x, 1] = 1
Proof.
G: Group
x: G
[x, 1] = 1
  by apply grp_commutator_commutes, grp_g1_1g.
Defined.

(** Commutators in abelian groups are trivial. *)
Definition ab_commutator (A : AbGroup) (x y : A)
  : [x, y] = 1.
A: AbGroup
x, y: A
[x, y] = 1
Proof.
A: AbGroup
x, y: A
[x, y] = 1
  apply grp_commutator_commutes, commutativity.
Defined.

(** The commutator can be thought of as the "error" in the commutativity of two elements of a group. *)
Definition grp_commutator_swap_op {G : Group} (x y : G)
  : x * y = [x, y] * y * x.
G: Group
x, y: G
x * y = [x, y] * y * x
Proof.
G: Group
x, y: G
x * y = [x, y] * y * x
  unfold grp_commutator.
G: Group
x, y: G
x * y = x * y * x^ * y^ * y * x
  by rewrite !grp_inv_gV_g.
Defined.

(** Inverting a commutator reverses the order. *)
Definition grp_commutator_inv {G : Group} (x y : G)
  : [x, y]^ = [y, x].
G: Group
x, y: G
[x, y]^ = [y, x]
Proof.
G: Group
x, y: G
[x, y]^ = [y, x]
  unfold grp_commutator.
G: Group
x, y: G
(x * y * x^ * y^)^ = y * x * y^ * x^
  by rewrite 3 grp_inv_op, 2 grp_inv_inv, 2 grp_assoc.
Defined.

(** Group homomorphisms commute with commutators. *)
Definition grp_homo_commutator {G H : Group} (f : G $-> H) (x y : G)
  : f [x, y] = [f x, f y].
G, H: Group
f: G $-> H
x, y: G
f [x, y] = [f x, f y]
Proof.
G, H: Group
f: G $-> H
x, y: G
f [x, y] = [f x, f y]
  unfold grp_commutator.
G, H: Group
f: G $-> H
x, y: G
f (x * y * x^ * y^) = f x * f y * (f x)^ * (f y)^
  by rewrite !grp_homo_op, !grp_homo_inv.
Defined.

(** A commutator with a product on the left side can be expanded as the product of a conjugated commutator and another commutator. *)
Definition grp_commutator_op_l {G : Group} (x y z : G)
  : [x * y, z] = grp_conj x [y, z] * [x, z].
G: Group
x, y, z: G
[x * y, z] = grp_conj x [y, z] * [x, z]
Proof.
G: Group
x, y, z: G
[x * y, z] = grp_conj x [y, z] * [x, z]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y, z: G
x * y * z * (x * y)^ * z^ =
x * (y * z * y^ * z^) * x^ * (x * z * x^ * z^)
  by rewrite grp_inv_op, !grp_assoc, !grp_inv_gV_g.
Defined.

(** A commutator with a product on the right side can be expanded as the product of a conjugated commutator and another commutator. *)
Definition grp_commutator_op_r {G : Group} (x y z : G)
  : [x, y * z] = [x, y] * grp_conj y [x, z].
G: Group
x, y, z: G
[x, y * z] = [x, y] * grp_conj y [x, z]
Proof.
G: Group
x, y, z: G
[x, y * z] = [x, y] * grp_conj y [x, z]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y, z: G
x * (y * z) * x^ * (y * z)^ =
x * y * x^ * y^ * (y * (x * z * x^ * z^) * y^)
  by rewrite grp_inv_op, !grp_assoc, !grp_inv_gV_g.
Defined.

(** A commutator with the element on the right being multiplied on the right gives a conjugation. *)
Definition grp_op_l_commutator {G : Group} (x y : G)
  : [x, y] * y = grp_conj x y.
G: Group
x, y: G
[x, y] * y = grp_conj x y
Proof.
G: Group
x, y: G
[x, y] * y = grp_conj x y
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
x * y * x^ * y^ * y = x * y * x^
  by rewrite grp_inv_gV_g.
Defined.

(** A commutator with the inverse element on the left being multiplied on the left gives a conjugation. *)
Definition grp_op_r_commutator {G : Group} (x y : G)
  : x^ * [x, y] = grp_conj y x^.
G: Group
x, y: G
x^ * [x, y] = grp_conj y x^
Proof.
G: Group
x, y: G
x^ * [x, y] = grp_conj y x^
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
x^ * (x * y * x^ * y^) = y * x^ * y^
  by rewrite <- !grp_assoc, grp_inv_V_gg.
Defined.

(** Commutators with inverted left sides are conjugated commutators. *)
Definition grp_commutator_inv_l {G : Group} (x y : G)
  : [x^, y] = grp_conj x^ [y, x].
G: Group
x, y: G
[x^, y] = grp_conj x^ [y, x]
Proof.
G: Group
x, y: G
[x^, y] = grp_conj x^ [y, x]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
x^ * y * (x^)^ * y^ = x^ * (y * x * y^ * x^) * (x^)^
  by rewrite !grp_assoc, grp_inv_inv, grp_inv_gV_g.
Defined.

(** Commutators with inverted right sides are conjugated commutators. *)
Definition grp_commutator_inv_r {G : Group} (x y : G)
  : [x, y^] = grp_conj y^ [y, x].
G: Group
x, y: G
[x, y^] = grp_conj y^ [y, x]
Proof.
G: Group
x, y: G
[x, y^] = grp_conj y^ [y, x]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
x * y^ * x^ * (y^)^ = y^ * (y * x * y^ * x^) * (y^)^
  by rewrite <- !grp_assoc, grp_inv_inv, grp_inv_V_gg.
Defined.

Definition grp_conj_commutator_inv_l {G : Group} (x y : G)
  : grp_conj x [x^, y] = [y, x].
G: Group
x, y: G
grp_conj x [x^, y] = [y, x]
Proof.
G: Group
x, y: G
grp_conj x [x^, y] = [y, x]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
x * (x^ * y * (x^)^ * y^) * x^ = y * x * y^ * x^
  by rewrite !grp_inv_inv, <- !grp_assoc, grp_inv_g_Vg.
Defined.

Definition grp_conj_commutator_inv_r {G : Group} (x y : G)
  : grp_conj y [x, y^] = [y, x].
G: Group
x, y: G
grp_conj y [x, y^] = [y, x]
Proof.
G: Group
x, y: G
grp_conj y [x, y^] = [y, x]
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y: G
y * (x * y^ * x^ * (y^)^) * y^ = y * x * y^ * x^
  by rewrite grp_inv_inv, !grp_assoc, grp_inv_gg_V.
Defined.

(** ** Hall-Witt identity *)

(** The Hall-Witt identity is a Jacobi-like identity for groups. It states that the different commutators of 3 elements (with one conjugated) assemble into an identity. The proof is purely mechanical and simply cancels all the terms. This is a rare instance where a mechanized proof is much shorter than an on-paper proof. *)
Definition grp_hall_witt {G : Group} (x y z : G)
  : [[x, y], grp_conj y z] * [[y, z], grp_conj z x] * [[z, x], grp_conj x y] = 1.
G: Group
x, y, z: G
[[x, y], grp_conj y z] * [[y, z], grp_conj z x] *
[[z, x], grp_conj x y] = 1
Proof.
G: Group
x, y, z: G
[[x, y], grp_conj y z] * [[y, z], grp_conj z x] *
[[z, x], grp_conj x y] = 1
  unfold grp_commutator, grp_conj, grp_homo_map.
G: Group
x, y, z: G
x * y * x^ * y^ * (y * z * y^) * (x * y * x^ * y^)^ *
(y * z * y^)^ *
(y * z * y^ * z^ * (z * x * z^) * (y * z * y^ * z^)^ *
 (z * x * z^)^) *
(z * x * z^ * x^ * (x * y * x^) * (z * x * z^ * x^)^ *
 (x * y * x^)^) = 1
  rewrite !grp_inv_op, !grp_inv_inv, !grp_assoc.
G: Group
x, y, z: G
... * y^ * z^ * z * x * z^ * z * y * z^ * y^ * z * x^ *
z^ * z * x * z^ * x^ * x * y * x^ * x * z * x^ * z^ *
x * y^ * x^ = 1
  do 3 rewrite !grp_inv_gV_g, !grp_inv_gg_V.
G: Group
x, y, z: G
x * x^ = 1
  apply grp_inv_r.
Defined.

(** 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.
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.
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
  rewrite 3 (grp_homo_commutator _ [_^, _]).
G: Group
x, y, z: G
[grp_conj x [x^, y], grp_conj x z] *
[grp_conj z [z^, x], grp_conj z y] *
[grp_conj y [y^, z], grp_conj y x] = 1
  rewrite 3 grp_conj_commutator_inv_l.
G: Group
x, y, z: G
[[y, x], grp_conj x z] * [[x, z], grp_conj z y] *
[[z, y], grp_conj y x] = 1
  apply grp_hall_witt.
Defined.

(** ** Precomposing normal subgroups with commutators *)

Instance issubgroup_precomp_commutator_l {G : Group} (H : Subgroup G)
  `{!IsNormalSubgroup H} (y : G)
  : IsSubgroup (fun x => H [x, y]).
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
IsSubgroup (fun x : G => H [x, y])
Proof.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
IsSubgroup (fun x : G => H [x, y])
  snapply Build_IsSubgroup; cbn beta.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x : G, IsHProp (H [x, y])
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
H [1, y]
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x y0 : G,
H [x, y] -> H [y0, y] -> H [x * y0, y]
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x : G, H [x, y] -> H [x^, y]
  -
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x : G, IsHProp (H [x, y]) exact _.
  -
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
H [1, y] rewrite grp_commutator_unit_l.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
H 1
    apply subgroup_in_unit.
  -
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x y0 : G,
H [x, y] -> H [y0, y] -> H [x * y0, y] intros x z Hxy Hzy.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H [x * z, y]
    rewrite grp_commutator_op_l.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H (grp_conj x [z, y] * [x, y])
    apply subgroup_in_op.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H (grp_conj x [z, y])
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H [x, y]
    +
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H (grp_conj x [z, y]) by rapply isnormal_conj.
    +
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x, z: G
Hxy: H [x, y]
Hzy: H [z, y]
H [x, y] assumption.
  -
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y: G
forall x : G, H [x, y] -> H [x^, y] intros x Hxy.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x: G
Hxy: H [x, y]
H [x^, y]
    rewrite grp_commutator_inv_l.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x: G
Hxy: H [x, y]
H (grp_conj x^ [y, x])
    rapply isnormal_conj.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x: G
Hxy: H [x, y]
H [y, x]
    rewrite <- grp_commutator_inv.
G: Group
H: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
y, x: G
Hxy: H [x, y]
H [x, y]^
    by apply subgroup_in_inv.
Defined.

(** The condition [H [x, y]] is equivalent to the condition [H [y, x]]. *)
Definition issubgroup_precomp_commutator_agree {G : Group} (H : Subgroup G)
  (x y : G)
  : H [x, y] <~> H [y, x].
G: Group
H: Subgroup G
x, y: G
H [x, y] <~> H [y, x]
Proof.
G: Group
H: Subgroup G
x, y: G
H [x, y] <~> H [y, x]
  refine (_ oE equiv_subgroup_inv _ _).
G: Group
H: Subgroup G
x, y: G
H [x, y]^ <~> H [y, x]
  by rewrite grp_commutator_inv.
Defined.

(** So we get this symmetrical version as well. *)
Instance issubgroup_precomp_commutator_r {G : Group} (H : Subgroup G)
  `{!IsNormalSubgroup H} (x : G)
  : IsSubgroup (fun y => H [x, y])
  := issubgroup_equiv (fun y => issubgroup_precomp_commutator_agree H y x) _.

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)
  : Subgroup@{i i} G
  := subgroup_generated (fun g => exists (x : H) (y : K), [x.1, y.1] = g).

Notation "[ H , K ]" := (subgroup_commutator H K) : group_scope.

Local Open Scope group_scope.

(** [subgroup_commutator H K] is the smallest subgroup containing the commutators of elements of [H] with elements of [K]. *)
Definition subgroup_commutator_rec {G : Group} {H K : Subgroup G} (J : Subgroup G)
  (i : forall x y, H x -> K y -> J (grp_commutator x y))
  : forall x, [H, K] x -> J x.
G: Group
H, K, J: Subgroup G
i: forall x y : G,
H x -> K y -> J (grp_commutator x y)
forall x : G, [H, K] x -> J x
Proof.
G: Group
H, K, J: Subgroup G
i: forall x y : G,
H x -> K y -> J (grp_commutator x y)
forall x : G, [H, K] x -> J x
  rapply subgroup_generated_rec; intros x [[y Hy] [[z Kz] p]];
    destruct p; simpl.
G: Group
H, K, J: Subgroup G
i: forall x y : G,
H x -> K y -> J (grp_commutator x y)
y: G
Hy: H y
z: G
Kz: K z
J (grp_commutator y z)
  by apply i.
Defined.

(** Doubly iterated [subgroup_commutator]s of [H], [J] and [K] are the smallest of the normal subgroups containing the doubly iterated commutators of elements of [H], [J] and [K]. *)
Definition subgroup_commutator_2_rec {G : Group} {H J K : Subgroup G}
  (N : Subgroup G) `{!IsNormalSubgroup N}
  (i : forall x y z, H x -> J y -> K z -> N (grp_commutator (grp_commutator x y) z))
  : forall x, [[H, J], K] x -> N x.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
forall x : G, [[H, J], K] x -> N x
Proof.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
forall x : G, [[H, J], K] x -> N x
  snapply subgroup_commutator_rec.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
forall x y : G,
[H, J] x -> K y -> N (grp_commutator x y)
  intros x z HJx Kz; revert x HJx.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
z: G
Kz: K z
forall x : G, [H, J] x -> N (grp_commutator x z)
  change (N (grp_commutator ?x z)) with (subgroup_precomp_commutator_l N z x).
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
z: G
Kz: K z
forall x : G,
[H, J] x -> subgroup_precomp_commutator_l N z x
  rapply subgroup_commutator_rec.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
i: forall x y z : G,
H x ->
J y ->
K z -> N (grp_commutator (grp_commutator x y) z)
z: G
Kz: K z
forall x y : G,
H x ->
J y ->
subgroup_precomp_commutator_l N z (grp_commutator x y)
  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).
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
[H, J] (grp_commutator x y)
Proof.
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
[H, J] (grp_commutator x y)
  apply tr, sgt_in.
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
{x0 : H &
{y0 : J &
grp_commutator x0.1 y0.1 = grp_commutator x y}}
  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.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
forall x : G, [H, J] x -> [K, L] x
Proof.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
forall x : G, [H, J] x -> [K, L] x
  snapply subgroup_commutator_rec.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
forall x y : G,
H x -> J y -> [K, L] (grp_commutator x y)
  intros x y Hx Jx.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
x, y: G
Hx: H x
Jx: J y
[K, L] (grp_commutator x y)
  apply subgroup_commutator_in.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
x, y: G
Hx: H x
Jx: J y
K x
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
x, y: G
Hx: H x
Jx: J y
L y
  -
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
x, y: G
Hx: H x
Jx: J y
K x by apply f.
  -
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x -> K x
g: forall x : G, J x -> L x
x, y: G
Hx: H x
Jx: J y
L y 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.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, [H, J] x <-> [K, L] x
Proof.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, [H, J] x <-> [K, L] x
  intros x; split; revert x; apply functor_subgroup_commutator.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, H x -> K x
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, J x -> L x
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, K x -> H x
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, L x -> J x
  1,3: apply f.
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, J x -> L x
G: Group
H, J, K, L: Subgroup G
f: forall x : G, H x <-> K x
g: forall x : G, J x <-> L x
forall x : G, L x -> J x
  1,2: apply g.
Defined.

Definition subgroup_incl_commutator_symm {G : Group} (H J : Subgroup G)
  : forall x, [H, J] x -> [J, H] x.
G: Group
H, J: Subgroup G
forall x : G, [H, J] x -> [J, H] x
Proof.
G: Group
H, J: Subgroup G
forall x : G, [H, J] x -> [J, H] x
  snapply subgroup_commutator_rec.
G: Group
H, J: Subgroup G
forall x y : G,
H x -> J y -> [J, H] (grp_commutator x y)
  intros x y Hx Jy.
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
[J, H] (grp_commutator x y)
  napply subgroup_in_inv'.
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
[J, H] (grp_commutator x y)^
  rewrite grp_commutator_inv.
G: Group
H, J: Subgroup G
x, y: G
Hx: H x
Jy: J y
[J, H] (grp_commutator y x)
  by apply subgroup_commutator_in.
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.
G: Group
H, J: Subgroup G
forall x : G, [H, J] x <-> [J, H] x
Proof.
G: Group
H, J: Subgroup G
forall x : G, [H, J] x <-> [J, H] x
  intros x; split; snapply subgroup_incl_commutator_symm.
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), [H, J] x
    <-> [subgroup_grp_op J, subgroup_grp_op H] x.
G: Group
H, J: Subgroup G
forall x : grp_op G,
[H, J] x <-> [subgroup_grp_op J, subgroup_grp_op H] x
Proof.
G: Group
H, J: Subgroup G
forall x : grp_op G,
[H, J] x <-> [subgroup_grp_op J, subgroup_grp_op H] x
  napply (subgroup_eq_subgroup_generated_op (G:=G)).
G: Group
H, J: Subgroup G
forall g : G,
{x : H & {y : J & grp_commutator x.1 y.1 = g}} <->
{x : subgroup_grp_op J &
{y : subgroup_grp_op H & grp_commutator x.1 y.1 = g}}
  intro x.
G: Group
H, J: Subgroup G
x: G
{x0 : H & {y : J & grp_commutator x0.1 y.1 = x}} <->
{x0 : subgroup_grp_op J &
{y : subgroup_grp_op H & grp_commutator x0.1 y.1 = x}}
  refine (iff_compose _ (equiv_sigma_symm _)).
G: Group
H, J: Subgroup G
x: G
{x0 : H & {y : J & grp_commutator x0.1 y.1 = x}} <->
{a : subgroup_grp_op H &
{b : subgroup_grp_op J & grp_commutator b.1 a.1 = x}}
  do 2 (snapply (equiv_functor_sigma'
    (grp_iso_subgroup_group (grp_op_iso_inv G)
      (equiv_subgroup_inv (G:=grp_op G) (subgroup_grp_op _)))); intro).
G: Group
H, J: Subgroup G
x: G
a: H
a0: J
(fun y : J => grp_commutator a.1 y.1 = x) a0 <~>
(fun b : subgroup_grp_op J =>
 grp_commutator b.1
   (grp_iso_subgroup_group (grp_op_iso_inv G)
      (fun x : G =>
       equiv_subgroup_inv (subgroup_grp_op H) x) a).1 =
 x)
  (grp_iso_subgroup_group (grp_op_iso_inv G)
     (fun x : G =>
      equiv_subgroup_inv (subgroup_grp_op J) x) a0)
  simpl.
G: Group
H, J: Subgroup G
x: G
a: H
a0: J
grp_commutator a.1 a0.1 = x <~>
grp_commutator (a0.1)^ (a.1)^ = x
  apply equiv_concat_l; symmetry.
G: Group
H, J: Subgroup G
x: G
a: H
a0: J
grp_commutator a.1 a0.1 =
grp_commutator (a0.1)^ (a.1)^
  lhs_V napply grp_commutator_inv.
G: Group
H, J: Subgroup G
x: G
a: H
a0: J
(grp_commutator a0.1 a.1)^ =
grp_commutator (a0.1)^ (a.1)^
  exact (grp_homo_commutator (grp_op_iso_inv _) a0.1 a.1).
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].
A: AbGroup
H, K: Subgroup A
IsTrivialGroup [H, K]
Proof.
A: AbGroup
H, K: Subgroup A
IsTrivialGroup [H, K]
  rapply subgroup_commutator_rec; intros.
A: AbGroup
H, K: Subgroup A
x, y: A
X: H x
X0: K y
trivial_subgroup A (grp_commutator x y)
  rapply ab_commutator.
Defined.

(** A commutator of normal subgroups is normal. *)
Instance isnormal_subgroup_commutator {G : Group} (H J : Subgroup G)
  `{!IsNormalSubgroup H, !IsNormalSubgroup J}
  : IsNormalSubgroup [H, J].
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
IsNormalSubgroup [H, J]
Proof.
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
IsNormalSubgroup [H, J]
  snapply Build_IsNormalSubgroup'.
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
forall x y : G, [H, J] x -> [H, J] (y * x * y^)
  intros x y; revert x.
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y: G
forall x : G, [H, J] x -> [H, J] (y * x * y^)
  apply (functor_subgroup_generated _ _ (grp_conj y)).
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y: G
forall g : G,
{x : H & {y : J & grp_commutator x.1 y.1 = g}} ->
{x : H &
{y0 : J & grp_commutator x.1 y0.1 = grp_conj y g}}
  intros x.
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y, x: G
{x0 : H & {y : J & grp_commutator x0.1 y.1 = x}} ->
{x0 : H &
{y0 : J & grp_commutator x0.1 y0.1 = grp_conj y x}}
  do 2 (rapply (functor_sigma (grp_iso_normal_conj _ y)); intro).
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y, x: G
a: H
a0: J
grp_commutator a.1 a0.1 = x ->
grp_commutator (grp_iso_normal_conj H y a).1
  (grp_iso_normal_conj J y a0).1 = grp_conj y x
  intros p.
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y, x: G
a: H
a0: J
p: grp_commutator a.1 a0.1 = x
grp_commutator (grp_iso_normal_conj H y a).1
  (grp_iso_normal_conj J y a0).1 = grp_conj y x
  lhs_V napply (grp_homo_commutator (grp_conj y)).
G: Group
H, J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup J
y, x: G
a: H
a0: J
p: grp_commutator a.1 a0.1 = x
grp_conj y
  (grp_commutator (subgroup_incl H a)
     (subgroup_incl J a0)) = grp_conj y x
  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.
G: Group
H, K, L: NormalSubgroup G
forall x : G,
[subgroup_product H K, L] x <->
subgroup_product [H, L] [K, L] x
Proof.
G: Group
H, K, L: NormalSubgroup G
forall x : G,
[subgroup_product H K, L] x <->
subgroup_product [H, L] [K, L] x
  intros x; split.
G: Group
H, K, L: NormalSubgroup G
x: G
[subgroup_product H K, L] x ->
subgroup_product [H, L] [K, L] x
G: Group
H, K, L: NormalSubgroup G
x: G
subgroup_product [H, L] [K, L] x ->
[subgroup_product H K, L] x
  -
G: Group
H, K, L: NormalSubgroup G
x: G
[subgroup_product H K, L] x ->
subgroup_product [H, L] [K, L] x revert x; snapply subgroup_commutator_rec.
G: Group
H, K, L: NormalSubgroup G
forall x y : G,
subgroup_product H K x ->
L y ->
subgroup_product [H, L] [K, L] (grp_commutator x y)
    intros x y HKx Ly; revert x HKx.
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
forall x : G,
subgroup_product H K x ->
subgroup_product [H, L] [K, L] (grp_commutator x y)
    change (subgroup_product ?H ?J (grp_commutator ?x y))
      with (subgroup_precomp_commutator_l (subgroup_product H J) y x).
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
forall x : G,
subgroup_product H K x ->
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y x
    snapply subgroup_generated_rec.
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
forall g : G,
(fun x : G => (H x + K x)%type) g ->
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y g
    intros x [Hx | Kx].
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Hx: H x
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y x
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Kx: K x
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y x
    +
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Hx: H x
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y x apply subgroup_product_incl_l.
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Hx: H x
[H, L] (grp_commutator x y)
      by apply subgroup_commutator_in.
    +
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Kx: K x
subgroup_precomp_commutator_l
  (subgroup_product [H, L] [K, L]) y x apply subgroup_product_incl_r.
G: Group
H, K, L: NormalSubgroup G
y: G
Ly: L y
x: G
Kx: K x
[K, L] (grp_commutator x y)
      by apply subgroup_commutator_in.
  -
G: Group
H, K, L: NormalSubgroup G
x: G
subgroup_product [H, L] [K, L] x ->
[subgroup_product H K, L] x revert x; snapply subgroup_generated_rec.
G: Group
H, K, L: NormalSubgroup G
forall g : G,
(fun x : G => ([H, L] x + [K, L] x)%type) g ->
[subgroup_product H K, L] g
    intros x [HLx | KLx].
G: Group
H, K, L: NormalSubgroup G
x: G
HLx: [H, L] x
[subgroup_product H K, L] x
G: Group
H, K, L: NormalSubgroup G
x: G
KLx: [K, L] x
[subgroup_product H K, L] x
    +
G: Group
H, K, L: NormalSubgroup G
x: G
HLx: [H, L] x
[subgroup_product H K, L] x revert x HLx.
G: Group
H, K, L: NormalSubgroup G
forall x : G, [H, L] x -> [subgroup_product H K, L] x
      apply functor_subgroup_commutator; trivial.
G: Group
H, K, L: NormalSubgroup G
forall x : G, H x -> subgroup_product H K x
      apply subgroup_product_incl_l.
    +
G: Group
H, K, L: NormalSubgroup G
x: G
KLx: [K, L] x
[subgroup_product H K, L] x revert x KLx.
G: Group
H, K, L: NormalSubgroup G
forall x : G, [K, L] x -> [subgroup_product H K, L] x
      apply functor_subgroup_commutator; trivial.
G: Group
H, K, L: NormalSubgroup G
forall x : G, K x -> subgroup_product H K x
      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.
G: Group
H, K, L: NormalSubgroup G
forall x : G,
[H, subgroup_product K L] x <->
subgroup_product [H, K] [H, L] x
Proof.
G: Group
H, K, L: NormalSubgroup G
forall x : G,
[H, subgroup_product K L] x <->
subgroup_product [H, K] [H, L] x
  intros x.
G: Group
H, K, L: NormalSubgroup G
x: G
[H, subgroup_product K L] x <->
subgroup_product [H, K] [H, L] x
  etransitivity.
G: Group
H, K, L: NormalSubgroup G
x: G
[H, subgroup_product K L] x <-> ?Goal
G: Group
H, K, L: NormalSubgroup G
x: G
?Goal <-> subgroup_product [H, K] [H, L] x
  1: symmetry; apply subgroup_commutator_symm.
G: Group
H, K, L: NormalSubgroup G
x: G
[subgroup_product K L, H] x <->
subgroup_product [H, K] [H, L] x
  etransitivity.
G: Group
H, K, L: NormalSubgroup G
x: G
[subgroup_product K L, H] x <-> ?Goal
G: Group
H, K, L: NormalSubgroup G
x: G
?Goal <-> subgroup_product [H, K] [H, L] x
  2: napply (subgroup_eq_functor_subgroup_product grp_iso_id
    (subgroup_commutator_symm _ _) (subgroup_commutator_symm _ _)).
G: Group
H, K, L: NormalSubgroup G
x: G
[subgroup_product K L, H] x <->
subgroup_product [K, H] [L, H] x
  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.
G, H: Group
f: G $-> H
J, K: Subgroup G
forall x : H,
subgroup_image f [J, K] x ->
[subgroup_image f J, subgroup_image f K] x
Proof.
G, H: Group
f: G $-> H
J, K: Subgroup G
forall x : H,
subgroup_image f [J, K] x ->
[subgroup_image f J, subgroup_image f K] x
  snapply subgroup_image_rec.
G, H: Group
f: G $-> H
J, K: Subgroup G
forall x : G,
[J, K] x ->
[subgroup_image f J, subgroup_image f K] (f x)
  change ([?G, ?H] (f ?x)) with (subgroup_preimage f [G, H] x).
G, H: Group
f: G $-> H
J, K: Subgroup G
forall x : G,
[J, K] x ->
subgroup_preimage f
  [subgroup_image f J, subgroup_image f K] x
  snapply subgroup_commutator_rec.
G, H: Group
f: G $-> H
J, K: Subgroup G
forall x y : G,
J x ->
K y ->
subgroup_preimage f
  [subgroup_image f J, subgroup_image f K]
  (grp_commutator x y)
  intros x y Jx Ky.
G, H: Group
f: G $-> H
J, K: Subgroup G
x, y: G
Jx: J x
Ky: K y
subgroup_preimage f
  [subgroup_image f J, subgroup_image f K]
  (grp_commutator x y)
  change (subgroup_preimage f [?G, ?H] ?x) with ([G, H] (f x)).
G, H: Group
f: G $-> H
J, K: Subgroup G
x, y: G
Jx: J x
Ky: K y
[subgroup_image f J, subgroup_image f K]
  (f (grp_commutator x y))
  rewrite grp_homo_commutator.
G, H: Group
f: G $-> H
J, K: Subgroup G
x, y: G
Jx: J x
Ky: K y
[subgroup_image f J, subgroup_image f K]
  (grp_commutator (f x) (f y))
  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] _.

(** We can quotient a group by its derived subgroup. *)
Definition grp_derived_quotient (G : Group) : Group
  := QuotientGroup G (normalsubgroup_derived G).

(** We can show that the multiplication then becomes commutative. *)
Instance commutative_grp_derived_quotient (G : Group)
  : Commutative (A:=grp_derived_quotient G) (.*.).
G: Group
Commutative sg_op
Proof.
G: Group
Commutative sg_op
  intros x.
G: Group
x: grp_derived_quotient G
forall y : grp_derived_quotient G, x * y = y * x
  srapply grp_quotient_ind_hprop; intros y; revert x.
G: Group
y: G
forall x : grp_derived_quotient G,
(fun x0 : G / normalsubgroup_derived G =>
 x * x0 = x0 * x) (grp_quotient_map y)
  srapply grp_quotient_ind_hprop; intros x; cbn beta.
G: Group
y, x: G
grp_quotient_map x * grp_quotient_map y =
grp_quotient_map y * grp_quotient_map x
  apply qglue, tr, sgt_in; exists (y^; tt), (x^; tt).
G: Group
y, x: G
grp_commutator (y^; tt).1 (x^; tt).1 =
(x * y)^ * (y * x)
  unfold grp_commutator; simpl.
G: Group
y, x: G
y^ * x^ * (y^)^ * (x^)^ = (x * y)^ * (y * x)
  by rewrite !grp_inv_op, !grp_inv_inv, !grp_assoc.
Defined.

(** Hence we have a way of producing abelian groups from groups. *)
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)
  : abgroup_derived_quotient G $-> A.
G: Group
A: AbGroup
f: G $-> A
abgroup_derived_quotient G $-> A
Proof.
G: Group
A: AbGroup
f: G $-> A
abgroup_derived_quotient G $-> A
  snapply (grp_quotient_rec _ _ f).
G: Group
A: AbGroup
f: G $-> A
forall n : G, normalsubgroup_derived G n -> f n = 1
  change (f ?n = 1) with (subgroup_preimage f (trivial_subgroup A) n).
G: Group
A: AbGroup
f: G $-> A
forall n : G,
normalsubgroup_derived G n ->
subgroup_preimage f (trivial_subgroup A) n
  snapply subgroup_commutator_rec.
G: Group
A: AbGroup
f: G $-> A
forall x y : G,
maximal_subgroup G x ->
maximal_subgroup G y ->
subgroup_preimage f (trivial_subgroup A)
  (grp_commutator x y)
  intros x y _ _.
G: Group
A: AbGroup
f: G $-> A
x, y: G
subgroup_preimage f (trivial_subgroup A)
  (grp_commutator x y)
  lhs napply grp_homo_commutator.
G: Group
A: AbGroup
f: G $-> A
x, y: G
grp_commutator (f x) (f y) = 1
  apply ab_commutator.
Defined.

(** Furthermore, this construction is an abelianization. *)
Definition isabelianization_derived_quotient (G : Group)
  : IsAbelianization (abgroup_derived_quotient G) grp_quotient_map.
G: Group
IsAbelianization (abgroup_derived_quotient G)
  grp_quotient_map
Proof.
G: Group
IsAbelianization (abgroup_derived_quotient G)
  grp_quotient_map
  intros A.
G: Group
A: AbGroup
IsSurjInj (group_precomp A grp_quotient_map)
  snapply Build_IsSurjInj.
G: Group
A: AbGroup
SplEssSurj (group_precomp A grp_quotient_map)
G: Group
A: AbGroup
forall x y : abgroup_derived_quotient G $-> A,
group_precomp A grp_quotient_map x $==
group_precomp A grp_quotient_map y -> x $== y
  -
G: Group
A: AbGroup
SplEssSurj (group_precomp A grp_quotient_map) intros f.
G: Group
A: AbGroup
f: G $-> A
{a : abgroup_derived_quotient G $-> A &
group_precomp A grp_quotient_map a $== f}
    nrefine (abgroup_derived_quotient_rec f; _).
G: Group
A: AbGroup
f: G $-> A
group_precomp A grp_quotient_map
  (abgroup_derived_quotient_rec f) $== f
    hnf; reflexivity.
  -
G: Group
A: AbGroup
forall x y : abgroup_derived_quotient G $-> A,
group_precomp A grp_quotient_map x $==
group_precomp A grp_quotient_map y -> x $== y intros f g p.
G: Group
A: AbGroup
f, g: abgroup_derived_quotient G $-> A
p: group_precomp A grp_quotient_map f $==
group_precomp A grp_quotient_map g
f $== g
    srapply grp_quotient_ind_hprop; intros x; cbn beta.
G: Group
A: AbGroup
f, g: abgroup_derived_quotient G $-> A
p: group_precomp A grp_quotient_map f $==
group_precomp A grp_quotient_map g
x: G
f (grp_quotient_map x) = g (grp_quotient_map x)
    exact (p x).
Defined.

(** *** Three subgroups lemma *)

Definition three_subgroups_lemma (G : Group) (H J K N : Subgroup G)
  `{!IsNormalSubgroup N}
  (T1 : forall x, [[H, J], K] x -> N x)
  (T2 : forall x, [[J, K], H] x -> N x)
  : forall x, [[K, H], J] x -> N x.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G, [[H, J], K] x -> N x
T2: forall x : G, [[J, K], H] x -> N x
forall x : G, [[K, H], J] x -> N x
Proof.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G, [[H, J], K] x -> N x
T2: forall x : G, [[J, K], H] x -> N x
forall x : G, [[K, H], J] x -> N x
  rapply subgroup_commutator_2_rec.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G, [[H, J], K] x -> N x
T2: forall x : G, [[J, K], H] x -> N x
forall x y z : G,
K x ->
H y ->
J z -> N (grp_commutator (grp_commutator x y) z)
  Local Close Scope group_scope.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
forall x y z : G, K x -> H y -> J z -> N [[x, y], z]
  intros z x y Kz Hx Jy.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
N [[z, x], y]
  pose proof (grp_hall_witt' x y z^) as p.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj x [[x^, y], z^] *
grp_conj z^ [[(z^)^, x], y] *
grp_conj y [[y^, z^], x] = 1
N [[z, x], y]
  rewrite grp_inv_inv in p.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj x [[x^, y], z^] * grp_conj z^ [[z, x], y] *
grp_conj y [[y^, z^], x] = 1
N [[z, x], y]
  apply grp_moveL_1V in p.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj x [[x^, y], z^] * grp_conj z^ [[z, x], y] =
(grp_conj y [[y^, z^], x])^
N [[z, x], y]
  apply grp_moveL_Vg in p.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N [[z, x], y]
  apply (isnormal_conj _ (y:=z^))^-1.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (z^ * [[z, x], y] * (z^)^)
  change (N (grp_conj z^ [[z, x], y])).
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj z^ [[z, x], y])
  rewrite p.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N
  ((grp_conj x [[x^, y], z^])^ *
   (grp_conj y [[y^, z^], x])^)
  apply subgroup_in_op.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj x [[x^, y], z^])^
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj y [[y^, z^], x])^
  -
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj x [[x^, y], z^])^ apply subgroup_in_inv.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj x [[x^, y], z^])
    rapply isnormal_conj.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N [[x^, y], z^]
    apply T1.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator (subgroup_commutator H J) K
  [[x^, y], z^]
    apply tr, sgt_in.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{x0 : subgroup_commutator H J &
{y0 : K & [x0.1, y0.1] = [[x^, y], z^]}}
    unshelve eexists.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator H J
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{y0 : K & [?x.1, y0.1] = [[x^, y], z^]}
    +
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator H J exists [x^, y].
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator H J [x^, y]
      apply subgroup_commutator_in; trivial.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
H x^
      by apply subgroup_in_inv.
    +
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{y0 : K &
[([x^, y];
 subgroup_commutator_in (subgroup_in_inv H x Hx) Jy).1,
y0.1] = [[x^, y], z^]} by exists (z^; subgroup_in_inv _ _ Kz).
  -
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj y [[y^, z^], x])^ apply subgroup_in_inv.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N (grp_conj y [[y^, z^], x])
    rapply isnormal_conj.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
N [[y^, z^], x]
    apply T2.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator (subgroup_commutator J K) H
  [[y^, z^], x]
    apply tr, sgt_in.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{x0 : subgroup_commutator J K &
{y0 : H & [x0.1, y0.1] = [[y^, z^], x]}}
    unshelve eexists.
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator J K
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{y0 : H & [?x.1, y0.1] = [[y^, z^], x]}
    +
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator J K exists [y^, z^].
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
subgroup_commutator J K [y^, z^]
      apply subgroup_commutator_in;
        by apply subgroup_in_inv.
    +
G: Group
H, J, K, N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
T1: forall x : G,
subgroup_commutator (subgroup_commutator H J) K x ->
N x
T2: forall x : G,
subgroup_commutator (subgroup_commutator J K) H x ->
N x
z, x, y: G
Kz: K z
Hx: H x
Jy: J y
p: grp_conj z^ [[z, x], y] =
(grp_conj x [[x^, y], z^])^ *
(grp_conj y [[y^, z^], x])^
{y0 : H &
[([y^, z^];
 subgroup_commutator_in (subgroup_in_inv J y Jy)
   (subgroup_in_inv K z Kz)).1, y0.1] = [[y^, z^], x]} by exists (x; Hx).
  Local Open Scope group_scope.
Defined.

Definition three_trivial_commutators (G : Group) (H J K : Subgroup G)
  : IsTrivialGroup [[H, J], K]
    -> IsTrivialGroup [[J, K], H]
    -> IsTrivialGroup [[K, H], J].
G: Group
H, J, K: Subgroup G
IsTrivialGroup [[H, J], K] ->
IsTrivialGroup [[J, K], H] ->
IsTrivialGroup [[K, H], J]
Proof.
G: Group
H, J, K: Subgroup G
IsTrivialGroup [[H, J], K] ->
IsTrivialGroup [[J, K], H] ->
IsTrivialGroup [[K, H], J]
  rapply three_subgroups_lemma.
Defined.