The density theorem in the ordinary category theory asserts that every presheaf on a small category is a colimit of representables in a canonical way. In Lemma 5.1.5.3 of Higher Topos Theory, Lurie proves an $\infty$-categorical version of this. There is a part of the proof which is not clear to me, and I hope someone kindly gives me an elaboration of the proof. (This question has already been asked previously on MSE (see here), but the question has not received an accepted answer yet. Given that it was asked about a year and a half ago, I decided that it wouldn't be inappropriate to ask the question again here.)

The lemma asserts the following:

If $S$ is a simplicial set, then $\operatorname{id}_{\mathcal{P}(S)}$ is the left Kan extension of the Yoneda embedding $j:S\to\mathcal{P}(S)=\operatorname{Fun}(S^{\mathrm{op}},\mathcal{S})$ along itself.

In the proof, he reduces the claim to the following assertion:

Let $\mathcal{C}\subset \mathcal{P}(S)$ be the essential image of the Yoneda embedding. Let $X\in\mathcal{P}(S)$ be an arbitrary object and $s$ an arbitrary object. Set $\mathcal{E}=(\mathcal{C}_{/X})^\triangleright\times_{\mathcal{P}(S)}(\mathcal{P}(S)_{j(s)/})$ and $\mathcal{E}^0=(\mathcal{C}_{/X})\times _{(\mathcal{C}_{/X})^\triangleright}\mathcal{E}$. Then the inclusion $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence.

Lurie then finishes the proof by claiming that both $\mathcal{E}$ and $\mathcal{E}^0$ deformation retracts onto $\mathcal{E}^1= \mathcal{C}_{/X}\times _{\mathcal{C}}\{\operatorname{id}_{\mathcal{C}}\}$. It is this very last step I am having trouble understanding. Why do $\mathcal{E}$ and $\mathcal{E}^0$ deformation retract onto $\mathcal{E}^1$? It is easy to see that they both have the homotopy type of $\operatorname{Map}_{\mathcal{P}(S)}(j(s),X),$ so I know that the claim isn't unreasonable. Also, the claim is easy to see if we are working with ordinary categories (and set-valued presheaves); but the proof (or my proof) does not seem to carry on direclty to the $\infty$-categorical case, because it relies heavily on the strict composition of 1-categories.

Any help (including alternative ways to see that $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence, or even alternative proofs of Lemma 5.1.5.3) is appreciated. Thanks in advance.

The density theorem in the ordinary category theory asserts that every presheaf on a small category is a colimit of representables in a canonical way. In Lemma 5.1.5.3 of Higher Topos Theory, Lurie proves an $\infty$-categorical version of this. There is a part of the proof which is not clear to me, and I hope someone kindly gives me an elaboration of the proof. (This question has already been asked previously on MSE (see here), but the question has not received an accepted answer yet. Given that it was asked about a year and a half ago, I decided that it wouldn't be inappropriate to ask the question again here.)

The lemma asserts the following:

If $S$ is a simplicial set, then $\operatorname{id}_{\mathcal{P}(S)}$ is the left Kan extension of the Yoneda embedding $j:S\to\mathcal{P}(S)=\operatorname{Fun}(S^{\mathrm{op}},\mathcal{S})$ along itself.

In the proof, he reduces the claim to the following assertion:

Let $\mathcal{C}\subset \mathcal{P}(S)$ be the essential image of the Yoneda embedding. Let $X\in\mathcal{P}(S)$ be an arbitrary object and $s$ an arbitrary object. Set $\mathcal{E}=(\mathcal{C}_{/X})^\triangleright\times_{\mathcal{P}(S)}(\mathcal{P}(S)_{j(s)/})$ and $\mathcal{E}^0=(\mathcal{C}_{/X})\times _{(\mathcal{C}_{/X})^\triangleright}\mathcal{E}$. Then the inclusion $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence.

Lurie then finishes the proof by claiming that both $\mathcal{E}$ and $\mathcal{E}^0$ deformation retracts onto $\mathcal{E}^1= \mathcal{C}_{/X}\times _{\mathcal{C}}\{\operatorname{id}_{j(s)}\}$. It is this very last step I am having trouble understanding. Why do $\mathcal{E}$ and $\mathcal{E}^0$ deformation retract onto $\mathcal{E}^1$? It is easy to see that they both have the homotopy type of $\operatorname{Map}_{\mathcal{P}(S)}(j(s),X),$ so I know that the claim isn't unreasonable. Also, the claim is easy to see if we are working with ordinary categories (and set-valued presheaves); but the proof (or my proof) does not seem to carry on direclty to the $\infty$-categorical case, because it relies heavily on the strict composition of 1-categories.

Any help (including alternative ways to see that $\mathcal{E}^0\subset \mathcal{E}$ is a weak homotopy equivalence, or even alternative proofs of Lemma 5.1.5.3) is appreciated. Thanks in advance.