∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)}
  {J : Subgroup ((i : η) → f i)}, J ≤ Subgroup.pi I H ↔ ∀ i ∈ I, J ≤ Subgroup.comap (Pi.evalMonoidHom f i) (H i)