This is an unofficial reimagining of the Archive of Formal Proofs
Hall's Marriage Theoremby Dongchen Jiang and Tobias Nipkow