Why is the 'mapping space' between two objects in a quasi-category a Kan complex?

The proof appears quite late in HTT. The simplicial set $X (a, b)$ (in Lurie's notation, $\mathrm{Hom}_X (a, b)$) is first mentioned after Remark 1.2.2.5, and the fact that it is a Kan complex appears implicitly in Corollary 4.2.1.8. A similar result appears as Corollary 4.8 in [Dugger and Spivak, Mapping spaces in quasi-categories], but they do not explicitly state that $X (a, b)$ (in their notation, $\mathrm{Hom}_X^\mathrm{cyl} (a, b)$) is a Kan complex. (They are more interested in showing that the different models of hom-spaces are weakly equivalent.)

I should probably mention that it is comparatively easy to show that $X (a, b)$ is a quasicategory. Indeed, the class of inner fibrations is well behaved with respect to exponentiation, so the projection $[\Delta^1, X] \to [\partial \Delta^1, X]$ is an inner fibration; and the class of inner fibrations is closed under pullback, so $X (a, b) \to \Delta^0$ is also an inner fibration, i.e. $X (a, b)$ is a quasicategory. In principle, it then suffices to prove that the "homotopy category" $\tau_1 (X (a, b))$ is a groupoid, but I don't see any quick way of doing this.

As Zhen noted, $\newcommand{\Hom}{\mathrm{Hom}}\Hom_X(a,b)$ is an $\infty$-category and it suffices to show that every 1-morphism of $\Hom_X(a,b)$ is an equivalence. In particular it is sufficient to show that every $(2,0)$-horn $\Lambda^2_0 \to \Hom_X(a,b)$ can be filled. One can translate this to the condition that any morphism $$ \Lambda^2_0 \times \Delta^1 \bigsqcup_{\Lambda^2_0 \times \partial\Delta^1} \Delta^2 \times \partial\Delta^1 \longrightarrow X, $$ that maps $\Lambda^2_0 \times \{0\}$ to $a$, lifts to a morphism $\Delta^2 \times \Delta^1 \to X$. Since in particular the 1-simplex $d^2(\Delta^2) \times \{0\}$ is mapped to an equivalence of $X$, the claim follows from Proposition 2.4.1.8 of HTT. To see how that proposition is applied here, see the proof of Lemma 2.3.3.5, for example. It may be overkill here, though, the idea is just the same as the proof of the implication (1) => (2) in Proposition 2.1.2.6 (Joyal's characterization of left anodyne maps).