[Merged by Bors] - feat(combinatorics/hall): Hall's marriage theorem

[agusakov]

We state and prove Hall's marriage theorem with respect to fintypes and relations.

Coauthor: @b-mehta @kmill

---

• depends on: [Merged by Bors] - feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint #5866
• depends on: [Merged by Bors] - feat(data/finset/basic): add lemmas about bUnion and images of functions on finsets #5887

[agusakov]

I need some help satisfying the linter - certain arguments go unused but figuring out how to order them is a bit weird.

[agusakov]

Switching to the awaiting-author label because I realized we can use image from data/rel instead of creating image_rel, and that's gonna take some time to refactor

[kmill]

@agusakov I added a rel.image version in hall2.lean. I also generalized the original hall to be in terms of indexed families of finite sets, because it was easier to eliminate image_rel that way (the translation was mostly mechanical, and then I started factoring some stuff out and trying to simplify things to some degree). This lets β both be infinite and be removed from the induction hypothesis.

Getting rel.image to work nicely even if β is infinite involves a typeclass that's at the beginning of the file. If [fintype β], then hall_rel is equivalent to

theorem hall_rel {α β : Type*} [fintype α] [decidable_eq β]
  (r : α → β → Prop) [fintype β] :
  (∀ (A : finset α), A.card ≤ fintype.card (rel.image r A))
  ↔ (∃ (f : α → β), function.injective f ∧ ∀ x, r x (f x)) :=

[bryangingechen]

Thanks! This looks pretty much ready to go to me.
bors d+

[bors]

✌️ agusakov can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

@bryangingechen Thanks -- I've incorporated your suggestions

[agusakov]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests