mathlib3

879da1cf - fix(algebraic_geometry/presheafedspace): fix lame proofs (#1273)

fix(algebraic_geometry/presheafedspace): fix lame proofs (#1273) * fix(algebraic_geometry/presheafedspace): fix lame proofs * fix * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin <johan@commelin.net>