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