chore(topology/sheaves): fix timeout by splitting proof (#9436)
In #7033 we were getting a timeout in `app_surjective_of_stalk_functor_map_bijective`. Since the proof looks like it has two rather natural components, I split out the first half into its own lemma. This is a separate PR since I don't really understand the topology/sheaf library, so I might be doing something very weird.
Timings:
* original (master): 4.42s
* original (master + #7033): 5.93s
* new (master + this PR): 4.24s + 316ms
* new (master + #7033 + this PR): 5.48s + 212ms
