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 commutative square $$\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?