SetTheory.Cardinal.Basic !4#2084

Stream: mathlib4

[Lukas Miaskiwskyi]

Opening this thread for one because it's a big file & it might be good to coordinate its port, but also because it's currently a red carpet. Many issues come from lean 4's weaker unification, but also from unresolved universe constraints

stuck at solving universe constraint
  max (u+1) (v+1) =?= max (u+1) (?u.71153+1)

These can generally be fixed by adding universe hints à la .{u+1,v+1} in the correct places, but I just want to raise awareness that lean 4 seems to struggle with universe constraints, perhaps more than we'd like it to. I'm guessing this will become more and more relevant for porting SetTheory files.

I was just editing this file, but I won't anymore for a bit, so feel free to have a look at it. Lots of simple and not so simple things still need to be fixed, I believe.