  We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion
in mathlib, which is a community-driven effort to build a unified mathematics
library for Lean. One goal of the mathlib project is to contain all of the
topics of a complete undergraduate mathematics education.
  We provide three presentations of the main theorem statement: in terms of
indexed families of finite sets, of relations on types, and of matchings in
bipartite graphs. We also formalize a version of K\H{o}nig's lemma (in terms of
inverse limits) to boost the theorem to the case of countably infinite index
sets. We give a description of the design of the recent mathlib library for
simple graphs, and we also give a necessary and sufficient condition for a
simple graph to carry a function.
