∀ {η : Type u_2} [Finite η] {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] (H 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⁆