I have been reading about and trying out type theory based proof assistants Lean and Coq, and I have seen a few formalized proofs of basic, isolated propositions.
I am looking for examples, showcases, of a formalized body of theory of e.g. standard undergraduate texts, to showcase how one would go about setting up complex formalized theories. E.g. I'd be interested to see a formalization in a proof assistant like Lean or Coq, of the theory of groups, together with the homomorphism theorems, and so forth.