mathlib4#537

Stream: mathlib4

[Moritz Doll]

@Scott Morrison thanks for merging, however I don't know how to proceed: I've tested whether the aliases are used and they are not, however Yury and Yael don't want to remove them from that file for now (see #17353). What is the best way to continue?

[Scott Morrison]

Oh, I put those aliases directly into Init.CcLemmas before hitting merge on that, so we should be good to go.