*writing* proofs involving commutative diagrams

This question is a little fuzzy so might be closed, but I'll give it a shot. I'm sorry this question has quite a long introduction, I don't see how to formulate it more concisely.

In modern algebraic geometry (for example), many objects are defined by universal properties of commutative diagrams etc. Now sometimes we want to prove statements about them (see below for a specific example). If we were working in, say, sets, then there are often proofs that one might call "element-wise". That is to say we prove say that two objects are isomorphic by writing down a morphism (explicitely!), a claimed inverse, and check on all points that the compositions indeed are the identity.

This does not work in (for example) the category of schemes, where a morphism "is" more than what it "does to points", and where moreover we may not have very explicit descriptions of various objects (e.g. fibred products). I thus find myself resorting to work with commutative diagrams and universal properties. This works, in the following sense: for any particular statement, I could convince a friend of it's correctness. This would go by drawing some diagram, saying a few words, extending the diagram and so on (this is the step where I get my morphisms, say). Finally I retrace various various of the maps I started with to show certain properties about composites and can then conclude that the morphism I have produced are actually inverses.

There typically are three things to be observed about this:

(1) Everything I did was "obvious" - in the sense that by writing down what I want to prove, I am immediately guided towards what I have to show in succession to make sense of it, and then verifying every step is usually trivial.

(2) Even though I can (with some thought) talk through a proof, I do not feel like I actually understand it very well.

(3) I have no idea how I would possibly write down such a proof. (Short of spending pages on trivialities, most of which consists of very similar-looking diagrams).

My question is, then, how to improve my situation. Note that if (2) were to improve then I would feel less of a need of being able to do (3) [although it would of course be nice].

A specific Example

"Show that relative frobenius commutes with base change".

Recall that for $X \in Sch/\mathbb{F}_p$, the morphism $\mathcal{O}_X \to \mathcal{O}_X, x \mapsto x^p$ induces a morphism $F_X: X \to X$ known as absolute frobenius. If we now fix $S \in Sch/\mathbb{F}_p$, we can define, for $X \in Sch/S$, $X^{(p)} = X \times_{S} S'$, where $S'$ is the scheme $S$ with structure morphism $F_S$. It is then easy to see that $X \to S$ and $F_X: X \to X$ canonically induce a morphism $F_{X/S}: X \to X^{(p)}$ known as relative frobenius.

Now given a base change $T \to S$, we have to show that $(X^{(p)})_T$ is canonically isomorphic to $(X_T)^{(p)}$, and that the composite $X_T \to (X_T)^{(p)} \to (X^{(p)})_T$ (first morphism being $F_{X_T/T}$) is just $F_{X/S} \times id_S.$

As I said above, I know (some way) to show this, it involves a mess of commutative diagrams, and writing this out would take a remarkable amount of space for a sequence of trivialities.

"As I said above, I know (some way) to show this, it involves a mess of commutative diagrams, and writing this out would take a remarkable amount of space for a sequence of trivialities."

Maybe that's okay to begin with. As you become more adept at the subject you can start leaving out details, but writing a sequence of commutative diagrams, while time and space consuming, is not that different from showing two knots are the same by writing down an explicit sequence of Reidemeister moves. In both cases, it seems like there is no simpler way of doing it.

I guess the "difficult" part is hidden behind the "universal property". Maybe, in order to feel that you fully understand your proof, you have to "find out" the construction hidden in it. Maybe you could try to embed the construction directly into the proof, in order to fill the gap...