meta code needed for `restrict_tac/sheaf_restrict`

Stream: mathlib4

[Joël Riou]

While trying to port AlgebraicGeometry.Morphisms.QuasiCompact #5642 I found out that the tactic restrict_tac now relies on aesop, but it does not seem to apply lemmas tagged with the sheaf_restrict attribute. Then, in this file, when f is a section of the structure sheaf of a scheme on an open U, the tactic restrict_tac is not able to see that the basic open where f is invertible is contained in U, even though the lemma Scheme.basicOpen_le is properly tagged as sheaf_restrict.