For a $2$-category $\mathcal{K}$, the free completion of $\mathcal{K}$ under Eilenberg-Moore-objects (EM-objects) is a $2$-category which has $0$-cells the (internal) monads $(A, t, \mu^t, \eta^t)$ in $\mathcal{K}$, and $1$-cells $(A, t, \mu^t, \eta^t) \longrightarrow (B, s, \mu^s, \eta^s)$ pairs $(m, \phi)$, in which $m: A \longrightarrow B$ is a $1$-cell in $\mathcal{K}$, and $\phi: sm \Longrightarrow mt$ a $2$-cell in $\mathcal{K}$ satisfying $m \mu^t \cdot \phi t \cdot s \phi = \phi \cdot \mu^s m$ and $\phi \cdot \eta^s m = m \eta^t$. In the case that $\mathcal{K}$ has EM-objects, these morphims of monads correspond bijectively to liftings: pairs $(\overline{m}, m)$ in which $\overline{m}: A^t \longrightarrow B^s$ and $m: A \longrightarrow B$ are $1$-cells in $\mathcal{K}$ such that $u^s \overline{m} = m u^t$, where $A^t$ and $B^s$ are the EM-objects of $(A, t, \mu^t, \eta^t)$ and $(B, s, \mu^s, \eta^s)$, respectively, and $u^t : A^t \longrightarrow A$ and $u^s : B^s \longrightarrow B$ are the so-called "forgetful" $1$-cells.
The one direction of this bijection is obvious. The other seems messy.
Specifically, $u^t$ and $u^s$ have left-adjoints $f^t: A \longrightarrow A^t$ and $f^s: B \longrightarrow B^s$, respectively, so given a lifting $(\overline{m}, m)$, we take the mate of the identity $2$-cell $u^s \overline{m} = m u^t$ and paste these two squares together to get a $2$-cell $\phi: sm \Longrightarrow mt$. Then together with $m$, one should verify that the two equalities above are satisfied. However, the mate is unwieldy and I can't seem to simplify its form easily to complete the verification.
Are there alternatives?