How Would an Intuitionist Prove This?

In general, when working in constructive mathematics, the strategy for proving $Q \lor R$ is to prove $Q$ or to prove $R$. In this case, just knowing abstractly that "there is an $n \not = 1$ that divides both $a$ and $b$" does not directly tell you whether $b$ is composite or whether $b$ divides $a$. So you will need more information to come up with a constructive proof.

If you know more than the fact that there is such an $n$, and you actually know the value of $n$, that would help. In particular, if you could tell whether your value of $n$ is equal to $b$, then you can tell which side of the disjunction holds. So we could use the fact $(\forall k)[k = b \lor k \not = b]$ to finish the constructive proof.

Many real-world constructive systems include additional facts like that about the natural numbers, which would not be true for other objects. In particular, many constructive systems prove the sentence $(\forall n,m \in \mathbb{N})[n = m \lor n \not = m]$, which says the natural numbers have decidable equality. The motivation for accepting this in constructive systems is that, given two concrete (terms for) natural numbers, we could in principle examine them to see if they are equal. This is not the case for other objects, such as real numbers, for which equality is not decidable. The fact that equality of natural numbers is decidable is provable, in many systems of constructive math, from induction axioms that are already included.

With a little work, these constructive systems prove that each natural number is either composite or not composite. And, with that extra fact, the remainder of the original proof goes through constructively. This may be out of the scope of an introductory proofs class, but it is one way a constructivist could prove the result.

To add a few details to Carl's answer...

Assuming your system includes full induction, your system can prove that any bounded arithmetic formula is decidable (i.e., $P \lor \lnot P$ is provable for these). The bounded arithmetic formulas are those built from atomic formulas ($s = t$ and $s \leq t$ for terms $s,t$) using logical connectives (${\land},{\lor},{\to},{\lnot}$) and bounded quantifiers $\forall x \leq t\ldots$ and $\exists x \leq t\ldots$ where $t$ is an arithmetic term in which the variable symbol $x$ does not occur. The proof that such formulas are decidable relies on the fact that, assuming $\forall x(P(x) \lor \lnot P(x))$ one can prove by induction on $y$ that $\forall x \leq y P(x)$ and $\exists x \leq y P(x)$ are decidable as well.

These formulas include many elementary arithmetic notions in (essentially) their natural forms: $$\begin{aligned} x \mid y \quad&\equiv\quad \exists z \leq y(xz = y)\\ \operatorname{Prime}(x) \quad&\equiv\quad x\geq 2 \land \forall y \leq x\forall z \leq x(yz = x \to y = x \lor z = x)\\ \operatorname{Composite}(x) \quad&\equiv\quad \exists y \leq x(y \neq 1 \land y \neq x \land y \mid x) \end{aligned}$$

Although $\lnot P \to Q$ does not entail $P \lor Q$ intuitionisitcally, the additional hypothesis that $P$ is decidable ($P \lor \lnot P$) does allow us to reach this conclusion using only intuitionistic reasoning. Assuming $P$, we immediately derive $P \lor Q$. Assuming $\lnot P$ and $\lnot P \to Q$, we conclude $Q$ and hence $P \lor Q$. Thus $$(P \lor \lnot P) \to (\lnot P \to Q) \to (P \lor Q)$$ is intuitionistically valid. Therefore, the $(\lnot P \to Q) \to (P \lor Q)$ is provable intuitionistically so long as $P$ is a bounded arithmetic statement.

The question was about intuitionism specifically, not some variant of constructivism, nor about some particular formalization of intuitionism (I don't think an intuitionist would recognize any particular formalization as being complete or even meaningful).

Your statement is not of the form $$P \to (Q \vee R).$$ It's of the form $$(\forall n)\Big(P(n) \to \big(Q(n) \vee R(n)\big)\Big).$$ (Quantification here is over natural numbers.)

To prove this intuitionistically, we don't necessarily need a proof of $(\forall n)(P(n) \to Q(n))$ or a proof of $(\forall n)(P(n) \to R(n)).$ What we need is a constructive way of finding, for each natural number $n,$ either a proof for that specific $n$ of $P(\underline{n}) \to Q(\underline{n})$ or a proof for that specific $n$ of $P(\underline{n}) \to R(\underline{n}),$ where $\underline{n}$ is the numeral representing $n.$

In general, to prove intuitionistically that $(\forall n)S(n),$ we need a constructive way of finding, for each natural number $n,$ a proof of $S(\underline{n})$ for that specific $n.$

In your example, it's clear that one can intuitionistically determine whether $b$ is composite or prime (simply check all possible factors between $2$ and $b-1\text{)}.$ If $b$ is composite, we immediately have a proof that "$b$ is composite or $(b \mid a)\text{."}$ If $b$ is prime, then since we are given that $n\ne 1\,\wedge\,(n\mid a)\,\wedge\,(n\mid b),$ we can conclude that $n=b,$ so $b\mid a,$ and again we have a proof of $\text{"}b$ is composite or $(b \mid a)\text{."}$

So we have an intuitionistically acceptable method, given any any $a, b, \text{ and }n$ such that $n\ne 1$ and $n$ divides both $a$ and $b$, of finding a proof that $"\!\underline{b}$ is a composite number or $\underline{b}$ divides $\underline{a}\!",$ which is exactly what is needed.

Now, there are ultrafinitists who might dispute the fact that each natural number $\gt 1$ is either prime or composite, but intuitionists would have no problem with that statement.