∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [Finite η] {s : (i : η) → Set (f i)},
  (∀ (i : η), 1 ∈ s i) →
    Subgroup.closure (Set.univ.pi fun i => s i) = Subgroup.pi Set.univ fun i => Subgroup.closure (s i)