The commutator of a finite direct product is contained in the direct product of the commutators.

theorem
Subgroup.commutator_pi_pi_of_finite
{η : Type u_1}
[Finite η]
{Gs : η → Type u_2}
[(i : η) → Group (Gs i)]
(H : (i : η) → Subgroup (Gs i))
(K : (i : η) → Subgroup (Gs i))
:

⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun (i : η) => ⁅H i, K i⁆

The commutator of a finite direct product is contained in the direct product of the commutators.