Kőnig's theorem in Lean from Mathlib's Hall: minimum cover minimality is exactly Hall's condition

To prove max matching = min vertex cover for a bipartite relation r : α → β → Prop, skip augmenting paths. Take a cover C = (A', B') minimizing #A' + #B' via (univ.filter (IsCover r)).exists_min_image, using classical for decidability. Apply Finset.all_card_le_biUnion_card_iff_exists_injective with ι = ↥A' and t a = univ.filter (r a) \ B'. If s violates Hall, then (A' \ S, B' ∪ s.biUnion t), with S = s.map (Embedding.subtype _), is a smaller cover, and card_sdiff_add_card_eq_card + card_union_le + omega finish. Run the same lemma on the flipped relation fun b a => r a b and cover (C.2, C.1) for the other side. The matching is the disjoint union of A'.attach.image (a ↦ (a, f a)) and B'.attach.image (b ↦ (g b, b)). It is disjoint because g b ∉ A'. Then card_union_of_disjoint gives #A' + #B'. About 170 lines.