mathlib

4cfe637b - chore(category_theory/sites/*): Adjust some `simp` lemmas. (#10574)

chore(category_theory/sites/*): Adjust some `simp` lemmas. (#10574) The primary change is removing some `simp` tags from the definition of `sheafify` and friends, so that the sheafification related constructions are not unfolded to the `plus` constructions. Also -- added coercion from Sheaves to presheaves, and some `rfl` simp lemmas which help some proofs move along. Some proofs cleaned up as well. Co-authored-by: Johan Commelin <johan@commelin.net>