Freyd–Mitchell's embedding theorem states that: if A$A$ is a small abelian category, then there exists a ring R and a full, faithful and exact functor $F\colon A \to R\text{-}\mathrm{Mod}$.
I have been trying to find a proof which does not rely on so many technicalities as the ones I have found. I have leafed through:
Freyd's Abelian Categories says that the text, excepting the exercises, tries to be a geodesic leading to the theorem. If you take out the exercises, probably the text is 120 pages long...
Mitchell's Theory of Categories (pdf) is very hard to read, and also to prove the theorem you have tons of definitions and propositions and lemmas to prove. For example, the study of AB-5 categories (C3 in Mitchell's notation) is fairly tedious.
Weibel's An Introduction to Homological Algebra (pdf) redirects me to Swan, The Theory of Sheaves, a book which is unavailable in my university's library. I've leafed through Swan's Algebraic K-Theory: the theorem is proved, but it is also long, hard and painful to read, and assumes a lot of knowledge I don't have (I had never seen a weakly effaceable functor, or a Serre subcategory; and it certainly is not well known to me that the category of additive functors from a small abelian category to the category of abelian groups is well-powered, right complete, and has injective envelopes!)
Maybe there are more modern proofs which require less heavy machinery and technicalities?