∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidableEq (Subgroup G)],
      ∀ j ∈ s, ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex