Formalizing Hall's Marriage Theorem in Lean. - Alena Gusakov; Bhavik Mehta; Kyle A. Miller (CoRR, 2021)