mathlib3

288cc2e4 - feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint (#5866)

feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint (#5866) Add lemma stating that dite of two injective functions is injective if their images are disjoint. Part of #5695 in order to prove Hall's Marriage Theorem. Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>