The point of view where this title come from is that Grothendieck theorem can be seen as a characterization of toposes of the form $BG$ for $G$ a profinite group. It shows that some topos can be represented as $BG$.

I think before Joyal-Tierney's paper it was also known how to generalize from profinite group to general localic groups.

Joyal-Tierney theorem shows that if you replace "pro-finite group" by "localic groupoid" then you actually get all Grothendieck toposes this way.


You can't directly recover Grothendieck theorem from Joyal-Tierney's theorem in the sense that the theorem as stated above don't tell you for which topos the localic groupoid can be chosed to be a profinite group. But if you are familiar with the methode used in the paper and how the groupoid is obtained (which in my opinion are even more important than the theorem itself) then it is fairly easy to recover Grothendieck theorem. For example, it immediately follows from Joyal-Tierney's paper that a topos is of the form $BG$ for $G$ a localic groups if and only if it admit a point $* \to \mathcal{T}$ which is an open surjection. (which does feel similar to Grothendieck theorem in terms of a fiber functor)


Regarding the use of internal logic, it is definitely not essential, it justs make everything simpler (at least if you are ok with its use) but one could do without it.

The main way they use internal logic is that in the first sections they prove some results about sup-lattice and frames locales, that are latter applied not to sup-latice and frames, but to suplatices and frame in a topos $\mathcal{T}$.
I believe there are also a few places where they make a claim about a morphism  of locales $f:X \to Y$ and then only prove it when $Y$ is the point (sorry I don't have the paper with me to give precise reference).


Another place where one can consider they use a bit of internal logic - though this one might be only at the level of intuition - is when they show that every topos admit an open cover by a locale. They do this by considering the topos as a classyfing topos of some theory $T$ and considering the propositional $T'$ of "enumerated $T$-model" that is $T$-model that are explicitely given as subquotient of the natural number. Though if I remember correctly, they present the argument in a way that don't directly involve any logic... (and in any case there are other proof of this results that are purely in terms of sites, for exemple the one is MacLane and Moerdijk book "Sheaves in geometry and logic" )