@PiotrPstrągowski I think quasicompact objects make sense in a topos (e.g.
stacks.math.columbia.edu/tag/090G) so maybe this is a quasicompact object of the slice topos? but maybe the easier thing is to figure out what happens in the proof before Scholze concludes something is quasicompact...