∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : DecidableEq G] {R S : Finset G}
  (hR : Subgroup.IsComplement ↑H ↑R),
  1 ∈ R →
    Subgroup.closure ↑S = ⊤ → Subgroup.closure ↑(Finset.image (fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤