theorem SimpleGraph.hall_marriage_theorem {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {A B : Set V} (hBip : G.IsBipartiteWith A B) : (∃ (M : G.Subgraph), A ⊆ M.verts ∧ M.IsMatching) ↔ ∀ U ⊆ A, U.ncard ≤ (⋃ x ∈ U, G.neighborSet x).ncard