mathlib

421ed703 - chore(topology/metric_space/baire): review (#3146)

chore(topology/metric_space/baire): review (#3146) * Simplify some proofs in `topology/metric_space/baire`; * Allow dependency on `hi : i ∈ S` in some `bUnion`/`bInter` lemmas.