forward-port 19105 #5749

Stream: mathlib4

[Scott Morrison]

I just finished the forward porting PR #5749, which forward ports !3#19105 on local cohomology.

Again I ran into this situtation where an instance search fails, with a universe unification error, #synth can find the required instance just fine, and adding the instance suggested by #synth as a shortcut instance solves the problem... It's a bit annoying to have to keep jupming through this hoop!!

[Scott Morrison]

Notifying @Kevin Buzzard and @Jake Levinson as you've been looking at this recently.