A Fitch derivation of the existence of the intersection of all members of a nonempty set is a better place to start because it can be done in less than ten sheets of paper longhand. The ratio of triviality to pages consumed is quite shocking when you finally confront it. It is at that point that you realize intuition has no formal translation but is vital since the level of detail seems to blur and darken intuition when holding a proof to the standard of formal derivation rather than the ordinary informal standard. So far, I’ve seen relatively little interest in mathematical intuition or even honest appraisal of what it is or how mathematicians should develop it. Rather the trend seems to be pretending that mathematical intuition doesn’t exist and treating formalization as a no-op. I think this is due to an anti-intellectual atmosphere that views mathematics as a source of problems for the military as opposed to pastimes for civilians.

This has reminded of the Two Capacitor Paradox [0]. (The moral of the story is that you have to know the limits of your model.)

[0] https://en.wikipedia.org/wiki/Two_capacitor_paradox