I essentially am asking for an explanation of the comment under this post by Tom Goodwillie.

In the "Kerodon", Lurie defines a simplicial covering map as follows:

A map $p:E\to X$ of simplicial sets is a covering map iff. for every pair of $v:\Delta^n\to X,h:\Lambda^n_i\to E$, with $p(h)=v|_{\Lambda^n_i}$, there is a unique $s:\Delta^n\to E$ with $s|_{\Lambda^n_i}=h$ and $p(s)=v$.

In "Calculus of fractions and homotopy theory", Gabriel-Zisman define it as follows:

The map $p$ is a covering map iff. for every $v\in X_n$, every $i\in[n]$ and every vertex $u$ of $E_0$ with $p(u)=v(i)$, there is a unique $s\in E_n$ with $s(i)=u$ and $p(s)=v$.

I have shown that both definitions are equivalent, and are further equivalent to the following:

The map $p$ is a covering map iff. for every $v\in X_n$, the pullback of $\Delta^n\overset{v}{\longrightarrow}X\overset{p}{\longleftarrow}E$ in simplicial sets - i.e., the fibre $p^{-1}(v)$ - is fibrewise isomorphic to $\Delta^n\times D$ where $D$ is a discrete simplicial set.

Using this, we can show that for every covering map $p$, the realisation $|p|$ is a covering map of topological spaces under a tweaked version of the usual definitions, where we allow for $|p|$ not surjecting, i.e. $|p|$ is an (ordinary) covering map of its image. If $f$ is a covering map of spaces, we can also show $\mathrm{Sing}(f)$ is a simplicial covering map without too much trouble. It is known that $\mathrm{Sing}(f)$ being a simplicial covering map does not imply that $f$ is a topological covering map.

However, we do, apparently, have that if $|p|$ is a topological covering map (in either the usual or tweaked sense) then $p$ must be a simplicial covering map. I've been able to show all of the above equivalences and implications myself, but this one I am thrown by.

I think the Gabriel-Zisman definition is the easiest one to use here. Take $v,u,i$ as in the definition, and identify all vertices of simplicial sets with their realisations (harmless). We know there is an evenly covered open neighbourhood $U$ of $x:=|p|(u)=|v|(i)$ in $X$, and that $|p|^{-1}(U)\cong U\times F$ fibrewise for some discrete space $F$. Among all the $n$-simplices $s$ of $E$ with $p(s)=v$, we know the vertices $s(i)$ have $p(s(i))=p(u)$ so that the vertices $|s|(i)$ all land in $|p|^{-1}(U)$ and are thus identifiable with pairs $(x,f_s)$ for unique $f_s\in F$. If $f_s=f_{s'}$, for connectivity reasons I know that for small enough neighbourhoods $V$ of $i$ $|s|(V)$ and $|s'|(V)$ will be equal in $|E|$: were $s\neq s'$, then since the 'open' cells corresponding to $s,s'$ are disjoint in $|E|$ (viewed as a CW complex) $|s|(V)=|s'|(V)$ would be a contradiction. Therefore the $f_s$ are unique to $s$.

From this, if $s,s'$ are two simplices of $E$ which solve the lifting problem - $s(i)=u=s'(i)$ and $p(s)=p(s')=v$ - then necessarily $s=s'$ since there is a unique $f$ with $u\in|p|^{-1}(U)$ associated to $(x,f)$, hence $f_s=f=f_{s'}$ and $s=s'$ follows.

Solutions then exist uniquely, if they exist at all. My problem is that I cannot see why we are guaranteed that any solution exists! It may well be that $E$ does not have enough simplices; the map $s\mapsto f_s$ is an injection into $F$ (among $s$ with $p(s)=v$) but not necessarily a surjection, a priori. A generic map $|\Delta^n|\to|E|$ does not need to correspond to a simplex $s\in E_n$. We know $\mathrm{Sing}(|p|)$ is a simplicial covering map, but it does not follow from this that $p$ is a covering map in any way I can see.

It is possibly relevant to note that, by definition, $|p|$ is a cellular map. If $e$ is a cell of $|E|$ with its natural CW structure, so too is $|p|(e)$ a cell of $|X|$. Conversely, $|p|^{-1}(e)$ is a disjoint union of cells in $|E|$ for every cell $e$ of $|X|$. I think this could be useful.

I would appreciate any relevant references, proofs or sketches of proofs for why solutions $s$ should exist in the first place. Under the linked post, references were given to May and to Goerss-Jardine: I skim-read the cited chapters, but could not find anything related to this.