Let $f:X\to BGL_1(\mathbb{S})$ be a morphism of $E_n$-spaces and determine a principle $GL_1(\mathbb{S})$-bundle over $X$. Then it can be shown in the classical case that there is always a Thom isomorphism $Mf\wedge Mf\to Mf\wedge X_+$ (Mahowald shows this, for instance here, modulo the concerns about operadic structure).

I'm interested in understanding how this map is produced in the modern $\infty$-categorical framework developed in work of Ando, Blumberg, Gepner and others. What this comes down to is showing that there is an *orientation* of $f$. This can be described as an equivalence of functors between $F=f\circ(-\wedge Mf):X\to BGL_1(\mathbb{S})\to BGL_1(Mf)$ and $\ast:X\to BGL_1(Mf)$. In other words, there should be an equivalence $F\simeq p^*Mf$ in the category $Mf_X\mathrm{-line}\simeq Fun(X^{op},Mf\mathrm{-line})$ where $Mf\mathrm{-line}$ is the category of $Mf$-modules which are equivalent to $Mf$ and $p:X\to \ast$ is the terminal map (note that to simplify notation I've called the composite map $F$). Such an equivalence would, upon applying $p_!$, yield an equivalence $Mf\wedge Mf=p_!F\simeq p_!p^\ast Mf=Mf\wedge X_+$.

One way to try to obtain such an orientation is to notice that the multiplication map $Mf\wedge Mf\to Mf$ is actually a map $p_!F\to Mf$ in $Mf\mathrm{-mod}$, which yields a map (simply by noting that $p_!$ is left adjoint to $p^\ast$) $F\to p^\ast Mf$ in $Mf_{X}\mathrm{-mod}$.

My question is the following: why is the map so obtained an equivalence? If it is not, is there another map $MF\to Mf$ that does give us this equivalence?