Addressing porting notes?

Stream: mathlib4

[Thomas Murrills]

I'm nearly finished with mono, and was wondering if I should restore the @[mono] attributes which were commented out and left with a porting note. I was about to go through and do it, but then started wondering if this would cause problems with SHA synchronization between mathlib3 and mathlib4, or if that's taken care of by automation.

In general, if a porting note becomes easy to fix in a completely unambiguous way (e.g. restoring @[mono] now that mono will be available) can it simply be fixed, or is there extra work a human has to do to make the SHA's line up? If so, what's the correct procedure?

[Jireh Loreaux]

There's no issue with SHAs because you aren't editing mathlib3 (or synchronizing a mathlib3 PR), so go ahead.

[Casavaca]

just a note, I've restored many of them. see https://github.com/leanprover-community/mathlib4/pull/2491

[Thomas Murrills]

Ok, great, I’ll rebase to master! :)