In this MO question I asked for some help with several definitions of formally etale maps. The definitions I'm asking about are 'isomorphism of tangent spaces', i.e the square below is a pullback $$\require{AMScd} \begin{CD} TM @>{df}>> TN\\ @V{\pi}VV @VV{\pi^\prime}V\\ M @>>{f}> N, \end{CD}$$ and the right lifting property against infinitesimal extensions, i.e for surjections with nilpotent kernel $\hat R\twoheadrightarrow R$ the existence of a unique diagonal filler $$\array{ \operatorname{Spec}R &\longrightarrow& \operatorname{Spec}B \\ \downarrow &\nearrow& \downarrow \\ \operatorname{Spec}\hat R &\longrightarrow& \operatorname{Spec}A. }$$

There's a comment I would really like to unravel. It says:

... you should think of $\operatorname{Spec}\hat R$ as some kind of tubular neighborhood of $\operatorname{Spec}R$, so the property is saying that you can lift (small enough) tubular neighborhoods along local diffeomorphisms. If you think about it for a while you'll see that this is more or less equivalent to being a local diffeomorphism.

I thought about this for a while but didn't really get anywhere. I'm looking for:

1. Geometric intuition (in the usual Euclidean world) to help me see why I should expect this equivalence intuitively.
2. Formal statement. Which properties can actually be said to be equivalent?

In this MO question I asked for some help with several definitions of formally etale maps. The definitions I'm asking about are 'isomorphism of tangent spaces', i.e the square below is a pullback $$\require{AMScd} \begin{CD} TM @>{df}>> TN\\ @V{\pi}VV @VV{\pi^\prime}V\\ M @>>{f}> N, \end{CD}$$ and the right lifting property against infinitesimal extensions, i.e for surjections with nilpotent kernel $\hat R\twoheadrightarrow R$ the existence of a unique diagonal filler $$\array{ \operatorname{Spec}R &\longrightarrow& \operatorname{Spec}B \\ \downarrow &\nearrow& \downarrow \\ \operatorname{Spec}\hat R &\longrightarrow& \operatorname{Spec}A. }$$

There's a comment I would really like to unravel. It says:

... you should think of $\operatorname{Spec}\hat R$ as some kind of tubular neighborhood of $\operatorname{Spec}R$, so the property is saying that you can lift (small enough) tubular neighborhoods along local diffeomorphisms. If you think about it for a while you'll see that this is more or less equivalent to being a local diffeomorphism.

I thought about this for a while but didn't really get anywhere. I'm looking for:

1. Geometric intuition (in the usual Euclidean world) to help me see why I should expect this equivalence intuitively.
2. Formal statement. Which properties can actually be said to be equivalent?