rt.representation theory – Comparing two definitions of Harish-Chandra bimodules

Let $mathfrak{g}$ be a finite dimensional semisimple Lie algebra over $mathbb{C}$, and let $mathscr{U}$ denote its universal enveloping algebra. I am interested in comparing two definitions in the literature of (finitely generated) Harish-Chandra bimodules.

Definition 1: A finitely generated $(mathscr{U}, mathscr{U})$-bimodule $H$ is said to be a Harish-Chandra bimodule if the adjoint action of $mathfrak{g}$ on $H$, $mathrm{ad}(a) : v mapsto av – va$, is locally finite (meaning that $H$ is a union of finite dimensional $operatorname{ad}mathfrak{g}$-invariant subspaces). For example, this is the definition given here.

Definition 2: Let $G$ be the simply connected algebraic group with Lie algebra $mathfrak{g}$, let $K$ be the diagonal copy of $G$ in $G times G$, and let $mathfrak{k}$ denote its Lie algebra. A Harish-Chandra bimodule is a finitely generated $(mathfrak{g} times mathfrak{g})$-module $V$ that is $K$-equivariant, in the following sense: $V$ has a $K$-module structure such that the action of $mathfrak{k}$ on $V$ obtained by differentiating the $K$-action coincides with the restriction of the $(mathfrak{g} times mathfrak{g})$-action; moreover, we have
begin{equation} tag{*}
k cdot (a cdot v) = (operatorname{Ad}(k)(a)) cdot (k cdot v) qquad
end{equation}

for all $k in K, a in mathfrak{g} times mathfrak{g}, v in V$.

Note that $H$ is a module over $mathscr{U}otimes mathscr{U}^{mathrm{op}}$ while $V$ is a module over $mathscr{U}otimes mathscr{U}$, but that the right action on $H$ can be turned into a left action by using the `principal anti-automorphism’ $psi: mathscr{U} to mathscr{U}$, which is given by $psi(x_1 cdots x_n) = (-1)^n x_n cdots x_1$. Modulo this difference, I would like to know if the two definitions are the same.

If I start with a HC bimodule $H$ in the sense of Definition 1 and consider it as a $(mathscr{U}otimes mathscr{U})$-module via $psi$, then the assumption is that the action of the diagonal $mathfrak{k}$ is locally finite, and hence can be integrated to an algebraic action of $K$ by semisimplicity (I think the simply connected hypothesis is also necessary here). But I am not sure if and how the adjoint compatibility condition (*) is satisfied.

On other hand, if I start with HC bimodule $V$ in the sense of Definition 2, then the adjoint action of the corresponding bimodule is locally finite, since it is obtained by differentiating the action of an algebraic group. So we do obtain a HC bimodule in the first sense.

I believe that in some sense Definition 2 must be the right definition, since the compatibility condition (*) is clearly very natural, and is also necessary for the equivariant form of the Beilinson-Bernstein equivalence to work.