Commit 2024-09-04 11:42 9a8bfbea

chore(CategoryTheory/Sites): remove unused lemmas and simplify some proofs in Sites.Discrete (#16385) This PR does the following

• Renames Sheaf.IsDiscrete to Sheaf.IsConstant and changes the definition to being in the essential image of the constant sheaf functor instead of requiring the counit to be an isomorphism.
• Removes two lemmas from the file Sites.Discrete which were essentially duplicates of other ones, and simplifies a proof to be able to remove an auxiliary lemma.
• Moves the remaining contets of Sites.Discrete to the file Sites.ConstantSheaf.