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](http://www.math.harvard.edu/~lurie/papers/Ambidexterity.pdf) 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.