In group theory, we often deal with subsets that are denoted by 'lifting' the group operation to subsets. For instance, the coset $gH = \{gh:h\in H\}$, or the conjugate $gHg^{-1} = \{ ghg^{-1}: h\in H \}$, or even $HK=\{hk:h\in H, k\in K\}$.
We also reason on these sets. For instance, if we have $$gHg^{-1}\subseteq H$$ then we can say that for any $h\in H$, by assumption $ghg^{-1} = h'$ for some $h'\in H$, and therefore that $h=g^{-1}h'g\in g^{-1}Hg$, and so $H\subseteq g^{-1}Hg$. Alternatively, we can do the more slick one line argument \begin{equation}\tag{1} H= g^{-1}gHg^{-1}g \subseteq g^{-1}Hg. \end{equation}
My question is something like -- when and why are we justified in doing the slick algebraic manipulation on subsets like in (1)?
What is the general thing that's going on here? E.g. this also works when $H$ is just a subset, not a subgroup. What if we're not working with groups at all (e.g. this would also work if we were working with monoids)? Or what if we're reasoning about longer strings of elements and subsets, like $abCdEF = GhIjkL$ where lowercase denotes elements and uppercase denotes subsets?
One idea I had was to think of a subset like $gS=\{gs: S\in S\}$ as the result of a group action of $g\in G$ on the powerset $\mathcal{P}(G)$. But even this view seems to require some further coherence conditions between e.g. left and right group actions. And even then we would want to generalize this to non-group settings. It feels like there should be an easier characterisation just in terms of sets and functions.