References about "monoidal fibrations" in $\infty$-category theory $\newcommand{\cat}{\mathsf} \newcommand{\fun}{\mathrm{Fun}} \newcommand{\calg}{\mathrm{CAlg}}$
Let $\cat C^\otimes,\cat D^\otimes, \cat E^\otimes$ be symmetric monoidal $\infty$-categories, and $p^\otimes: \cat D^\otimes \to \cat E^\otimes$ a map of $\infty$-operads (aka a lax symmetric monoidal functor).
Assume $p: \cat D\to \cat E$ is a cartesian fibration.
I'd like to know under what natural conditions $\fun^{lax}(\cat C^\otimes,\cat D^\otimes)\to \fun^{lax}(\cat C^\otimes,\cat E^\otimes)$ is still a cartesian fibration, and more specifically if there are references regarding this type of situation.
A few remarks:

*

*In the cases I'm interested in, $p^\otimes$ is a map of symmetric monoidal $\infty$-categories, so a strict symmetric monoidal functor. If that's necessary to give an interesting statement, I'm willing to assume it.

*Still in those cases, $\cat{D,E}$ are presentable with a compatible tensor product, and I can reduce to the case where $\cat C$ is small, so using Day-convolution, one can reduce to the question of whether $\calg(\cat D)\to \calg(\cat E)$ is still a cartesian fibration, i.e. to the case $\cat C = N(Fin_*)$.

*Finally, I'm also in a situation where $p$ is a "monoidal fibration", by which I mean that if $x\to y$ is a $p$-cartesian edge, then so is $x\otimes z\to y\otimes z$; I think this can be relevant - and hopefully this, together with the first bullet point, should be enough.

Has something like this been written up anywhere ?
EDIT : I wrote down what I think is a complete proof, and indeed items 1 and 3 are the ones that make it work. But the proof is long for this sort of technical result and I'm still interested in references so as not to lengthen what I'm writing too much.
 A: I don't know a reference but here is a not-too-long proof. The condition that $\mathsf{D} \to \mathsf{E}$ is a cartesian fibration implies that for every $\langle n \rangle \in \mathrm{Fin}_*$ the map $\mathsf{D}^{\otimes}_{\langle n\rangle} \to \mathsf{E}^{\otimes}_{\langle n\rangle}$ is a cartesian fibration and that for every inert map $\alpha : \langle n\rangle \to \langle m\rangle$ the transition functor $\alpha_*:\mathsf{D}^{\otimes}_{\langle n\rangle} \to \mathsf{D}^{\otimes}_{\langle m\rangle}$ sends $p^{\otimes}_{\langle n\rangle}$-cartesian edges to $p^{\otimes}_{\langle m\rangle}$-cartesian edges.
Now apply (the dual of) [HTT, Corollary 4.3.1.15] to deduce that every $p^{\otimes}_{\langle n\rangle}$-cartesian edge in the fiber $\mathsf{E}^{\otimes}_{\langle n\rangle}$ is also $p^{\otimes}$-cartesian as an edge in $\mathsf{E}$ (note that being a cartesian edge is a form of a relative limit). This means that the map $p^{\otimes}: \mathsf{D} \to \mathsf{E}$, though possibly not a cartesian fibration itself, still admits cartesian lifts for a certain collection of edges in $\mathsf{E}$: all the edges which are contained in a fiber $\mathsf{E}^{\otimes}_{\langle n\rangle}$ for some $\langle n\rangle$. Otherwise put: all the arrows which map to an equivalence in $\mathrm{Fin}_*$. It then follows that the functor
$$ \mathrm{Fun}_{\mathrm{Fin}_*}(\mathsf{C}^{\otimes},\mathsf{D}^{\otimes}) \to \mathrm{Fun}_{\mathrm{Fin}_*}(\mathsf{C}^{\otimes},\mathsf{E}^{\otimes}) $$
is a cartesian fibration, where $\mathrm{Fun}_{\mathrm{Fin}_*}$ denotes functors preserving the projection to $\mathrm{Fin}_*$ (but not necessarily preserving inert edges). Indeed, any natural transformation of functors $\mathsf{C}^{\otimes} \to \mathsf{E}^{\otimes}$ whose projection to $\mathrm{Fin}_*$ is constant consists object-wise of arrows in $\mathsf{E}^{\otimes}$ which admit cartesian lifts in $\mathsf{D}^{\otimes}$ by the above, and hence itself admits cartesian lifts as a natural transformation. By base change we then conclude that the functor
$$ \mathrm{Fun}^{\mathrm{lax}/\mathsf{E}}(\mathsf{C}^{\otimes},\mathsf{D}^{\otimes}) \to \mathrm{Fun}^{\mathrm{lax}}(\mathsf{C}^{\otimes},\mathsf{E}^{\otimes}) $$
is a cartesian fibration, where $\mathrm{Fun}^{\mathrm{lax}/\mathsf{E}}$ here stands for the those functors $\mathsf{C}^{\otimes} \to \mathsf{D}^{\otimes}$ over $\mathrm{Fin}_*$ whose projection to $\mathsf{E}^{\otimes}$ preserves inert edges. To finish the proof it will suffice to show that for cartesian edge in $\mathrm{Fun}^{\mathrm{lax}/\mathsf{E}}(\mathsf{C}^{\otimes},\mathsf{D}^{\otimes})$, if its target preserves inert edges then its domain preserves inert edges. Given that inert edges in $\mathsf{D}^{\otimes}$ are exactly the cocartesian lifts of the inert edges in $\mathrm{Fin}_*$, this follows from the fact that inert transition functors $\alpha_*:\mathsf{D}^{\otimes}_{\langle n\rangle} \to \mathsf{D}^{\otimes}_{\langle m\rangle}$ sends $p^{\otimes}_{\langle n\rangle}$-cartesian edges to $p^{\otimes}_{\langle m\rangle}$-cartesian edges.
A: I have accepted Yonatan's answer because ultimately his proof is what's appearing in the reference, but for future reference, we included his proof in this preprint, as Appendix B (rather than the one I had in mind at first, which was longer and used more hypotheses). So now, there is a reference.
