∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] [inst_1 : DecidableEq η] {I : Set η}
  {H : (i : η) → Subgroup (f i)} (i : η) (x : f i), (Pi.mulSingle i x ∈ Subgroup.pi I H) = (i ∈ I → x ∈ H i)