A collection of theorems that probably already exist in Mathlib4. The goal of these formalisations is to follow my paper proofs maximally, even if it hurts readability or makes the proofs terribly long. This is to assist me in learning the best practices and getting around Mathlib itself.