Searching for some sheaf theoretic lemmas

Stream: mathlib4

[Nathan Corbyn]

I'm currently stuck searching for a lemma roughly of the form: given a Grothendieck topology J on a small category C and a sieve S on an object X (not assumed to belong to the topology), if every sheaf on (C, J) satisfies the sheaf condition for the sieve S, then S belongs to J(X). I'm hoping this is already included in mathlib4, but I've been searching for a few hours and keep coming up blank. Thanks in advance!

[Bhavik Mehta]

This isn't particularly direct, but maybe you could build J2, as the smallest topology containing S and J, show that a presheaf on C is a sheaf on (C, J2) iff it's a sheaf on (C, J), then use docs#CategoryTheory.topology_eq_iff_same_sheaves. But I'd hope there's an easier way.
That's the only theorem in mathlib I know of of the form "(if every sheaf ...), then", but maybe others exist

[Nathan Corbyn]

The most straightforward proof I know is: that every sheaf satisfies the sheaf condition for S gives that the sheafification of the functor inclusion is an isomorphism and therefore locally surjective. You can use the characterisation of local surjections given in MLM to get the required result.