Why, if the geometric realisation of a simplicial map $p$ is a (topological) covering map, must $p$ be a (simplicial) covering map? 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 know this should be true since it was commented by Tom and also stated in Lurie's "Kerodon", though it was there stated without proof as "proposition: $?$".
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. As a note to myself (inspired by Maxime’s answer), this is only true by invariance of domain for homeomorphisms $p$, since we can have in general a mapping of a nondegenerate $n$-simplex (corresponding to an $n$-cell in the CW structure) to a degenerate one (not corresponding to any particular cell) which breaks the argument.
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.
 A: Cf. here, geometric realization commutes with finite limits, at least if taken in the category of compactly generated spaces.
In particular, for any $n$-simplex $\sigma :\Delta^n\to X$, we find that $|E\times_X\Delta^n|\cong |E|\times_{|X|}|\Delta^n|$. Note that the latter pullback is supposed to be taken in the category of compactly generated spaces, however, the ordinary pullback is a covering space over $|\Delta^n|$, hence it is trivial as a covering space (because $|\Delta^n|$ is contractible), and hence it is compactly generated, and therefore it is the compactly generated pullback too.
This implies, using again the fact that this covering space must be trivial, that $|E\times_X\Delta^n|\cong |\Delta^n|\times F$ for some discrete $F$, over $|\Delta^n|$. By invariance of domain, and looking at the interior of each of the top $n$-simplices in the right hand side, we find that they must come from $n$-simplices in $E\times_X\Delta^n$, so we have $\sigma_f\in E\times_X\Delta^n, f\in F$ which induce a map $\Delta^n\times F\to E\times_X\Delta^n$ such that the composite $|\Delta^n\times F|\to |E\times_X\Delta^n|\to |\Delta^n|\times F$ is the canonical isomorphism. In particular, because the second map is a homeomorphism, so is the first map. Note that it follows automatically that $\Delta^n\times F\to E\times_X \Delta^n$ is a map over $\Delta^n$.
So now we are reduced to: let $f:A\to B$ be a map of simplicial sets such that $|f|$ is a homeomorphism, then $f$ is an isomorphism. This isn't too hard; in fact you can prove it using again the fact that $|-|$ commutes with finite limits and the fact that $|X|$ is never a point if $X$ is not a point (which is an easier special case). You can also prove it by hand, using invariance of domain for instance.
