mathlib3

82532c19 - chore(data/set/basic): reuse some proofs about `boolean_algebra` (#5728)

chore(data/set/basic): reuse some proofs about `boolean_algebra` (#5728) API changes: * merge `set.compl_compl` with `compl_compl'`; * add `is_compl.compl_eq_iff`, `compl_eq_top`, and `compl_eq_bot`; * add `simp` attribute to `compl_le_compl_iff_le`; * fix misleading name in `compl_le_iff_compl_le`, add a missing variant; * add `simp` attribute to `compl_empty_iff` and `compl_univ_iff`; * add `set.subset.eventually_le`.