The interesting thing about doing mathematics — in a research sense — is that often there is no intuition. Instead, there's a projection from one domain into another, where that projection might have an intuitive proof yet is itself completely unintuitive; and then there are people using that domain-mapping equivalence to prove things in one domain using completely unintuitive statements about them that can only be made in the other domain.

I might liken it to what LLVM's IR optimizer passes do. You put in source code (intuitive), get out object code (also intuitive, for those who know the processor) — but in between, the code passes through various projective and derived forms that are not clean representations of either the source or target form, but instead are just models amenable to certain static analyses — i.e. proofs! — that then allow/deny certain rewrites to happen.

A mathematician is someone who has to do what those IR optimization passes do, in their head. They know that they can derive a projective model, that they can then poke at symbolically, to derive more lemmas that will be able to be mapped back into lemmas about the model outside the projection. That doesn't mean that they intuitively understand what those within-projection steps mean in terms of the outer model. (If they did, they wouldn't need the projected model; they'd just make their deductions in terms of the outer model!) Instead, they just know how the inner model works as a model — how to poke it to make it do things, etc — and they know general rules of math and logic that allow them to prove things within that model, and to transform and map proofs between models. But, in "feeling grounded" terms, they're mostly working blind.