mathlib3

1d650c2e - chore(category_theory/sites/dense_subsite): minor refactor (#19002)

chore(category_theory/sites/dense_subsite): minor refactor (#19002) Lean 4 pointed out that `include H` came slightly too early in `category_theory/sites_dense_subsite`; it doesn't need to be in the definition of https://leanprover-community.github.io/mathlib_docs/category_theory/sites/dense_subsite.html#category_theory.cover_dense.types.pushforward_family , for example. I removed both the `include`s in the file, which changes the types of at least one declaration (a superfluous `H` is no longer there). This file is not a leaf file -- it's imported by all the algebraic geometry hierarchy for example -- but mathlib still compiles with these edits and I propose making this change in the ported version of this file.