!4#3578

Stream: mathlib4

[Jeremy Tan]

!4#3578 can someone help fix the 3 remaining errors in this file?

[Scott Morrison]

First: @Jeremy Tan, it would be helpful when you link to PRs if you can include the name of the file, either in the topic title (preferred) or in the first message. This assists others deciding if they have the expertise/time/inclination to look at the linked PR, without being expected to click through.

[Scott Morrison]

Second, I've fixed these three errors. One I think we can blame on over-golfing in mathlib3. :-) The other two are simp regressions, not particularly different than we see frequently, so if someone would like to investigate that's great, or we could probably merge with the porting notes as is.