Porting note: essentially already ported to std4

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971