mathlib3

69e9344c - feat(data/set/finite): add lemma with iff statement about when finite sets can be subsets (#5725)

feat(data/set/finite): add lemma with iff statement about when finite sets can be subsets (#5725) Part of #5698 in order to prove statements about strongly regular graphs. Co-author: @shingtaklam1324 Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>