In Higher Algebra Lemma 6.1.6.3, most of the proof is pretty straightforward, but after thinking I understood it all correctly, I realized I had a gap in my understanding.

Suppose we have a homotopy cartesian square of $\infty$-categories (the Lemma has these as Kan complexes, but I think this is irrelevant to my question here) $$\begin{matrix}X'&\xrightarrow{f'}&Y'\\ \downarrow^{g_X}&&\downarrow^{g_Y}\\X&\xrightarrow{f}&Y \end{matrix}$$

and for simplicity, $C$ is an $\infty$-category with enough limits for $f^*$ and $f'^*$ to admit right adjoints.

In the proposition (which has more conditions, though they are irrelevant to this question), we want to see if the Beck-Chevalley transformation $$g^*_Yf_* \to f'_*f'^*g_Y^*f_* \simeq f'_*g_X^*f^*f_*\to f'_*g_X^*$$ is an is an equivalence.

Lurie suggests we prove this by pointwise evaluation on a functor $F:X\to C$ and an object $y$ of $Y'$ of the Beck-Chevalley transformation as the induced map $$\operatorname{lim}(F|X\times_Y Y_{g_Y(y)/}) \to \operatorname{lim}(F|X'\times_Y' Y'_{y/}).$$

The trouble is, it's not clear to me why this map, induced by the diagram

$$\begin{matrix} X' & \to & Y'& \leftarrow & Y'_{y/}\\ \downarrow &&\downarrow&&\downarrow\\ X&\to&Y&\leftarrow&Y_{g_Y(y)/} \end{matrix}$$

is homotopic to the component of the Beck-Chevalley map at $F$ and $y$.

I tried evaluating the intermediate terms, but they are huge and messy, and I can't find a reference showing that they are indeed homotopic.

Is the proof easy? Does anybody have a reference?

Edit: I think this is related to the proof of 4.3.3 in Ambidexterity paper of Lurie and Hopkins. It looks like he uses cartesianness of the square there to identify (the adjuncts of) these maps (in the dual case of left Kan extensions), so I have added a cartesianness condition.