mathlib

85d6221d - refactor(topology/sheaf_condition): remove redundant constructions (#17378)

refactor(topology/sheaf_condition): remove redundant constructions (#17378) The constructions used to prove `is_sheaf_iff_is_sheaf_equalizer_products` in *sites.lean* is redundant because the equivalence can now be achieved via `is_sheaf` (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff. The author @justus-springer of the constructions has previously [approved the removal](https://github.com/leanprover-community/mathlib/pull/11706#issuecomment-1024476451) in #11706. The universe levels in *equalizer_products.lean* are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions. - [x] depends on: #17361 Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>