∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i), (∀ (i : η), Pi.mulSingle i (x i) ∈ H) → x ∈ H