!4#2457

Stream: mathlib4

[Moritz Doll]

There is one error (technically two, but it is the same issue) left that I have no idea how to fix, namely that comp_rangeSplitting seems to have changed from mathlib3 to mathlib4 and I don't know whether this is port problem or a Lean 4 problem.