Every proof I can find of this result is by way of regular expressions. Is there any "constructive" proof that defines the corresponding DFA (probably NFA)? For instance the proof of concatenation closure is most often presented by demonstrating the NFA. I'm just curious whether this is out there somewhere
There is a simple proof using automata. Suppose the original language is $L$, and we are substituting $R_a$ for $a$ (for each $a \in \Sigma$). Starting with an automaton for $L$, replace each edge $(x,y)$ annotated $a$ with a copy of an automaton $A_a$ for $R_a$, connecting $x$ to the starting state of $A_a$ with an $\epsilon$-edge, and connecting each accepting state of $A_a$ (which is not accepting any more in the new automaton) to $y$ with an $\epsilon$-edge.
I would think that, given that there are contructive methods to pass from one definition to another, about all methods used to prove these things may be considered constructive.
Regarding NFA, if $R_a$ is the DFA for the regular set substituted to $a$, then you remove any $a$-transition from state $p$ to state $q$ of you original automaton, and replace it by an $\epsilon$-transition from $p$ to the initial state of $R_a$ and $\epsilon$-transitions from the final states of $R_a$ to $q$. You must simply be careful to use a different copy of $R_a$ for each $a$-transition, which entails renaming all the states of $R_a$.
Remarks (following a comment by sjmc)
Theorists need nearly none of these proofs specific to regular sets. They use general proofs regarding full trios and full AFls (abstract families of languages). Since the family of regular sets is a full trio (which does have to be proved with some constructions), actually even a full AFL, it inherits a whole canned collection of closure properties that have been proved for all members of these families.
Explicit constructions are usually very simple for regular sets, so that anyone with a tiny bit of experience in building automata can imagine them. But they can also be tedious when you go into details. Hence they are "left as an exercise" for whoever needs them.
The proof based on regular expressions is probably the most interesting because of its architecture based on an interpretation of a formal term algebra, built on some operators corresponding to closure properties of regular sets: union, concatenation, Kleene star, and on a set of constants corresponding to the alphabet. Regular set are then a specific interpretation (morphism) of this algebra,associating each term (i.e., regular expression) with a set of strings on the alphabet, and each operator with the corresponding operations on sets of strings. The interest of this approach is that substitution of a variable by a term is a standard operation in term algebras that stays within the algebra, and can thus be interpreted in the same domain. Hence the closure.
A full specification of the construction of a finite automaton for regular substitution is given by Algorithm 4.2.7 of  (with a several-page proof of correctness). Tedious indeed!
 Meduna, Alexander. Automata and languages: theory and applications Springer, 2000.