!4#3463 universe constraint issues

Stream: mathlib4

[Kevin Buzzard]

!4#3463 . Porting CategoryThjeory.Sites.Limits and right now there are 40+ errors of the form stuck at solving universe constraint which I don't know how to solve. The things Lean is getting stuck on are typically either of the form max v ?u.13688 =?= max u v or max (max v w) ?u.16518 =?= max (max u v) w . I've tagged the PR as help-wanted. Any ideas?

[Eric Wieser]

Usually the fix is to tell Lean explicitly what you want to fill the universe metavariable with, by adding .{u} somewhere

[Eric Wieser]

I think .{_,_,u} might also be legal if u isn't the first universe parameter, but I don't know

[Jireh Loreaux]

I've seen some universe issues like this arising from the ordering of implicit arguments changing (perhaps because of auto implicits?). So maybe compare those to the mathlib3 version.

[Kevin Buzzard]

Universe order changes in the following code.

-- lean3
import category_theory.category.basic

universes v u

open category_theory

variables {C : Type max v u} [i : category.{v} C]

set_option pp.universes true
#check @i -- i : category.{v (max v u)} C

vs

-- lean4
import Mathlib.CategoryTheory.Category.Basic

universe v u

open CategoryTheory

variable {C : Type max v u} [i : Category.{v} C]

set_option pp.universes true in
#check @i -- i : Category.{v, max u v} C

[Reid Barton]

Lean 4 seems to do some kind of universe level normalization that can make solving unification problems later more difficult

[Reid Barton]

We looked at this some in Karlsruhe with @Markus Himmel and others

[Markus Himmel]

Adam suggested at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Universe.20issues.20with.20concrete.20categories/near/346361826 that the problem is related to typeclass inference, but I haven't made any progress on that file even with that knowledge.

[Kevin Buzzard]

Lean 4 is doing a better job of universes than lean 3 in CategoryTheory.Sheaf.multiforkEvaluationCone: Lean 3 has stuff like (max v (max v u) w) where Lean 4 has max (max u v) w. One thing I find particularly surprising with Lean 4's normalisation is that it seems to be alphabetical: the "declare universes in a careful order" stuff we used to do in lean 3 category theory is now irrelevant?

I'm making progress with the PR again.

[Joël Riou]

I have just pushed this https://github.com/leanprover-community/mathlib4/pull/3463/commits/74211493db7923fe9ea0e7696f0a3f172b4888c2 which seems to make the situation less scary.

[Kevin Buzzard]

Yes, I'd also managed to find this fix! In fact you don't even need v. Thanks for alerting me to the push!

[Reid Barton]

The order of declaring universe variables was for controlling the order that you would specify explicit universe level arguments in.

[Kevin Buzzard]

Ok so I've got it all compiling modulo a sorry -- an extra goal which appeared during an erw and which is hopefully easy. But it's no good: the instances aren't firing because of the universe problems. See for example the bottom of the file:

-- porting note: I had to name this instance because I need to explicitly
-- use it in the next instance; in Lean 3 the typeclass inference
-- system could handle the universe problems.
instance instHasColimitsOfShapeSheaf [HasColimitsOfShape K D] : HasColimitsOfShape K (Sheaf J D) :=
  ⟨fun _ => HasColimit.mk
    ⟨sheafifyCocone.{_, _, u} (colimit.cocone _), isColimitSheafifyCocone _ (colimit.isColimit _)⟩⟩

-- porting note: typeclass inference used to do this and now it doesn't because of universe
-- issues.
instance [HasColimits D] : HasColimits (Sheaf J D) := ⟨by
  intro K _
  exact instHasColimitsOfShapeSheaf.{_, _, u}⟩

-- porting note: instance above won't fire because of universe issues.
-- example [HasColimits D] : HasColimits (Sheaf J D) := inferInstance -- doesn't actually work

[Kevin Buzzard]

Gabriel informs us in the porting meeting that Lean.Level.normalize does indeed reorder universes into alphabetical order, which is presumably part of the reason that universes are being randomly permuted in the port.

import Lean

#eval Lean.Level.normalize (.max (.param `v) (.param `w))
-- Lean.Level.max (Lean.Level.param `v) (Lean.Level.param `w)

#eval Lean.Level.normalize (.max (.param `v) (.param `u))
-- Lean.Level.max (Lean.Level.param `u) (Lean.Level.param `v)

[Mario Carneiro]

Just catching up on the meeting now and seeing this issue, and it's not immediately clear to me why the observed reordering matters at all. The careful ordering of universe arguments in the category theory library is about the argument order to regular functions and definitions like Category.{v, u}, not the built in level operation max u v which is supposed to be commutative. Any occurrence of max u v should be treated identically to max v u, so the mentioned canonicalization doesn't seem to be a problem. @Kevin Buzzard mentions recalling that max u v = max u ?v is unified to ?v := v in lean 3 but I don't think this is the case, IIRC it was just as conservative as lean 4 in this regard.

[Gabriel Ebner]

From what I recall (and see in the source code), the order did matter in Lean 3. Level unification seems to be completely rewritten in Lean 4 though, and in a way that seems to intentionally ignore the order.

[Gabriel Ebner]

I couldn't find any design discussion on zulip or github, but my best guess is that this behavior is intentional since max u v = max u ?w does not have a unique solution (e.g. we could assign ?w = v or ?w = max u v).

[Mario Carneiro]

Yes, the lean 4 behavior makes sense to me, but I recall having ambiguous unification issues of exactly that form in lean 3 as well, so perhaps that was a fallback behavior that triggered only in certain circumstances?

[Mario Carneiro]

Also this issue still needs a #mwe demonstrating a failing instance or something that worked in lean 3

[Gabriel Ebner]

universes u v
def foo : Type u × Type max u v := (punit, punit)
#check (foo : Type u × Type max u v) -- works in Lean 3

[Gabriel Ebner]

universe u v
def foo : Type u × Type max u v := (PUnit, PUnit)
#check (foo : Type u × Type max u v) -- fails in Lean 4

[Mario Carneiro]

I see. And #check (foo : Type u × Type max v u) fails in lean 3

[Mario Carneiro]

and #check (foo : Type u × Type max u (max u v)) also yields foo.{u v} which is... fun

[Mario Carneiro]

One possible way to improve the situation here would be if there was a way to declare universe inequalities, as an elaborator feature which desugars def foo.{u, v>=u} to def foo.{u, v} in the declaration site and an annotation to always pass max u v instead of v for the second universe argument

[Gabriel Ebner]

That would only change the unification problem from max u ?w = max u v to max u (max u ?w) = max u v.

[Mario Carneiro]

ex:

def foo.{u, v where v ≥ u} : Type u × Type v := (PUnit, PUnit)
-- sent to kernel: def foo.{u, v} : Type u × Type (max u v) := (PUnit, PUnit)
-- elaborator remembers that foo.{u, v where v ≥ u} : Type u × Type v

universe u v
#check (foo : Type u × Type (max u v)) -- infers foo.{u, max u v}

[Mario Carneiro]

the unification problem in this case would be foo.{?u, ?v} : Type ?u × Type ?v =?= Type u × Type (max u v) because the elaborator remembers that foo was declared with a universe inequality

[Mario Carneiro]

I think we don't have precedent for the "elaborator remembers" part, that would have to be a separate piece of data from the ConstInfo, maybe an environment extension which stores the type with its declared universes rather than the max encoding used for the kernel

[Mario Carneiro]

When creating the foo.{?u, ?v} term we also get a pending defeq problem ?v =?= max ?u ?v which needs to be resolved after ?v is assigned

[Mario Carneiro]

Conceivably this could even be done without user annotations like where v ≥ u, since you can look at the type to try to find candidate universes like v here that only appear in the form max a v for some fixed a

[Gabriel Ebner]

At that point it might be easier to just add the rule that max t s =?= max t r reduces to s =?= r.

[Mario Carneiro]

I assume you mean that it would be too much work to implement? I agree that it's quite a big divergence from the status quo but I think it would definitely lead to better outcomes than the lean 3 heuristic

[Mario Carneiro]

I'm just talking about what we could do to avoid dealing with unification problems of the form max u v = max u ?v without changing the theory, in the long run

[Reid Barton]

Mario Carneiro said:

One possible way to improve the situation here would be if there was a way to declare universe inequalities, as an elaborator feature which desugars def foo.{u, v>=u} to def foo.{u, v} in the declaration site and an annotation to always pass max u v instead of v for the second universe argument

Yeah I mentioned the same idea to Sebastian in Karlsruhe--I only gave it a couple minutes' thought but it seems like it could be a translation managed by the elaborator, at least in ordinary use (e.g. ignoring metaprogramming)

[Adam Topaz]

I'm running into a similar universe issue on line 241 of !4#3487

[Adam Topaz]

instance topCat_hasLimitsOfSize : HasLimitsOfSize.{v} TopCat.{max v u}
    where has_limits_of_shape _ :=
    { has_limit := fun F =>
        HasLimit.mk
          { cone := limitCone.{v,u} F
            isLimit := limitConeIsLimit F } }
#align Top.Top_has_limits_of_size TopCat.topCat_hasLimitsOfSize

example : HasLimitsOfSize.{v} TopCat.{max v u} := by infer_instance
/-
stuck at solving universe constraint
  max (u+1) (v+1) =?= max (v+1) (?u.31052+1)
while trying to unify
  HasLimitsOfSize TopCat
with
  (HasLimitsOfSize TopCat) (HasLimitsOfSize TopCat) (HasLimitsOfSize TopCat)
-/

That can't be good.

[Matthew Ballard]

If you delete the universe annotations, it seems to work

[Adam Topaz]

but that's without general universes

[Adam Topaz]

I think

[Matthew Ballard]

The .{max v u} annotation seems to make Lean 4 very unhappy

[Adam Topaz]

But I don't understand why.

[Adam Topaz]

Anyway, this is not sustainable.

[Adam Topaz]

I'm starting to think that we need to ungeneralize the universe parameters in the (co)limit library :-/

[Matthew Ballard]

That was my initial impression but it seems that stripping out the max’s generally makes things smoother than I first expected.

[Matthew Ballard]

From checking the resulting declaration, it seemed to me that Lean was doing the correct thing (or a reasonable thing).

[Adam Topaz]

I mean, this is ridiculous:

set_option pp.universes true
def foo : HasLimitsOfSize TopCat := inferInstance -- works
#check foo
/-
TopCat.foo.{u_1, u_2} : HasLimitsOfSize.{u_1, u_1, max u_1 u_2, (max u_1 u_2) + 1} TopCat.{max u_1 u_2}
-/
def bar : HasLimitsOfSize.{v, v, max v u, (max v u)+1} TopCat.{max v u} := inferInstance -- fails
/-
stuck at solving universe constraint
  max (u+1) (v+1) =?= max (v+1) (?u.31092+1)
while trying to unify
  HasLimitsOfSize.{v, v, max v u, (max v u) + 1} TopCat.{max v u}
with
  (HasLimitsOfSize.{v, v, max ?u.31092 v, max (?u.31092 + 1) (v + 1)} TopCat.{max v ?u.31092})
    (HasLimitsOfSize.{v, v, max ?u.31092 v, max (?u.31092 + 1) (v + 1)} TopCat.{max v ?u.31092})
    (HasLimitsOfSize.{v, v, max ?u.31092 v, max (?u.31092 + 1) (v + 1)} TopCat.{max v ?u.31092})
-/

[Matthew Ballard]

Yes. Take my suggestion as a workaround and not a permanent solution.

[Kevin Buzzard]

@Adam Topaz does it work if you change u to w? (the reason I'm asking is that "u,v" is in alphabetical order whereas "w,v" isn't)

[Adam Topaz]

def bar : HasLimitsOfSize.{v, v, max v w, (max v w)+1} TopCat.{max v w} := inferInstance -- fails

nope, still fails.

[Adam Topaz]

@Gabriel Ebner @Mario Carneiro (or any other lean4 universe experts?) do you have any suggestions here?

[Mario Carneiro]

can you make a MWE? The types of relevant constants should suffice

[Adam Topaz]

I need to run in a few minutes, but I'll do my best.

[Adam Topaz]

Maybe Matt has time to make a MWE?

[Mario Carneiro]

pulling this stuff deep in mathlib always means getting the latest mathlib, lean, and cache which takes long enough for me to forget what I was trying to do in the first place

[Kevin Buzzard]

I'm about to get on the tube, I'll try minimising and report back in 50 minutes (if I don't get a seat then it won't happen)

[Matthew Ballard]

I’ve got to meet with a student in a few minutes

[Kevin Buzzard]

Meh do we not have the instance in master?

[Kevin Buzzard]

found it in !4#3487

[Matthew Ballard]

Sorry. I didn’t realize that was the question.

[Adam Topaz]

section
universe v u

class Foo (C : Type u) where
  Bar : Type v
end

section

universe v' v u' u

class Bar (C : Type u) [Foo.{v} C] (D : Type u') [Foo.{v'} D] where
  Baz : Type (max (max u' u) v)

end

universe v u
variable (C : Type ((max v u) + 1)) (D : Type v)
  [Foo.{max v u} C] [Foo.{v} D]

instance : Bar.{v} C D := sorry

example : Bar.{v} C D := inferInstance

[Adam Topaz]

I think that should capture essentially the same error @Mario Carneiro with no mathlib4 dependency

[Gabriel Ebner]

Can you remind me what Foo/Bar/Baz are again?

[Adam Topaz]

Foo.{v} C should correspond to Category.{v} C and Bar C D should correspond to HasLimitsOfShape C D (approximately)

[Mario Carneiro]

This instance looks like it should be linted against

[Mario Carneiro]

because Bar has four universe parameters and the second one is not constrained in a useful way

[Adam Topaz]

I did this in a rush, so I'm not 100% sure I got the universes right.

[Eric Wieser]

Would that linter forbid the docs4#Lean.ToLevel instances too Mario?

[Adam Topaz]

But the error at the end looks similar.

[Mario Carneiro]

no, since you can determine that universe from the output type

[Eric Wieser]

What do you mean "the output type"? The output type is Lean.ToLevel.toLevel.{u} : Nat

[Mario Carneiro]

I mean the typeclass type

[Mario Carneiro]

the thing that is being instance-searched

[Mario Carneiro]

ToLevel.{u} in this case

[Mario Carneiro]

The error message here seems pretty borked though:

stuck at solving universe constraint
  max (u+1) (v+1) =?= max (v+1) (?u.165+1)
while trying to unify
  Bar C D
with
  (Bar C D) C inst✝¹ D inst✝

Bar C D is not a function, it looks like the error message put the type of the instance instead of the instance itself

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

because Bar has four universe parameters and the second one is not constrained in a useful way

It's constrained via the [Category.{v} C] argument.

[Mario Carneiro]

also lean says the type of Bar.{v} C D is

⊢ Type (max (max ((max (u + 1) (v + 1)) + 1) (v + 1)) ((max u v) + 1))

which seems like a failure of level normalization, although I doubt it is the actual issue

[Mario Carneiro]

sorry I meant v u in the anonymous instance

[Gabriel Ebner]

You mean u, right? The v is well constrained, but the only way to figure out the u is by solving max ?u v = max u v.

[Mario Carneiro]

The instance has type:

⊢ (C : Type ((max v u) + 1)) →
  (D : Type v) →
    [inst : Foo.{max v u, max (u + 1) (v + 1)} C] →
      [inst_1 : Foo.{v, v} D] → Bar.{v, max u v, v, max (u + 1) (v + 1)} C D

u never appears alone in this type, so the mathlib3 linter should fire on it

[Mario Carneiro]

it's possible it is fooled by the max (u + 1) (v + 1) at the end, which seems to be the lean 4 preferred way to spell max u v + 1

[Gabriel Ebner]

From what I remember, the mathlib linter explicitly accepts this. It expects the unifier to solve max u v = max ?u v.

[Gabriel Ebner]

The +1 is a red herring here.

[Gabriel Ebner]

Slightly cleanup up MWE:

universe v' v u' u -- specify order of universe parameters

class Category (C : Type u) where
  Morphisms : Type v

class HasLimitsOfShape (C : Type u) [Category.{v} C] (D : Type u') [Category.{v'} D] where
  Limits : Type max u' u v

variable (C : Type max v u) (D : Type v) [Category.{max v u} C] [Category.{v} D]

instance : HasLimitsOfShape.{v} C D := sorry

example : HasLimitsOfShape.{v} C D := inferInstance
/-
stuck at solving universe constraint
  max u v =?= max v ?u.165
-/

[Mario Carneiro]

I mean it might be fooling our linter

[Gabriel Ebner]

To quote the linter doc:

This usually means that there is a max u v in the type where neither u nor v occur by themselves.

Here, the v already appears by itself, so max u v is kosher.

[Mario Carneiro]

I see. I maintain that this should be rejected by a linter though

[Eric Wieser]

Note that the example above still fails even if you hand-hold lean on the universe arguments of the desired type, and cut out typeclass search

def bar : Bar.{v, max u v, v, max (u + 1) (v + 1)} C D := sorry
example : Bar.{v, max u v, v, max (u + 1) (v + 1)} C D := bar _ _ -- fails
example : Bar.{v, max u v, v, max (u + 1) (v + 1)} C D := bar.{_,u} _ _ -- ok

[Mario Carneiro]

@Eric Wieser that's basically what I mean, from the input and output types alone you still can't solve the universe argument in bar.{_}

[Mario Carneiro]

this kind of instance will never work

[Gabriel Ebner]

It did work "just fine" in Lean 3 though.

[Mario Carneiro]

I don't like the idea of reintroducing the broken lean 3 normalization / level unification though

[Gabriel Ebner]

from the input and output types alone you still can't solve the universe argument

Of course you can solve it. Solving max ?u v = max u v is not impossible, it's merely unclear whether we want or should do it.

[Mario Carneiro]

I am actually wondering whether we should try to prefer ?u := max u v for that kind of problem

[Eric Wieser]

Do we have a scenario where solving it is harmful?

[Gabriel Ebner]

It is harmful if you later need to unify ?u = u or ?u = max u v. Right now, this kind of constraint gets postponed.

[Mario Carneiro]

Then again, if we get to the point that we are going to reject the solution entirely due to stuck universe constraints, we apparently never got to ?u = u or ?u = max u v

[Mario Carneiro]

so maybe it's fine to just pick one

[Mario Carneiro]

and I think max u v is the more predictable one, if we had to choose

[Kevin Buzzard]

Just catching up but here's the MWE I made:

-- set_option pp.universes true

class Quiver'.{v, u} (V : Type u) where
  Hom : V → V → Sort v

class Category'.{v, u} (obj : Type u) extends Quiver'.{v + 1} obj : Type max u (v + 1) where

def TopCat'.{u} : Type (u + 1) := PUnit

instance moo.{u} : Category'.{u, u + 1} TopCat' := sorry

class HasLimitsOfSize'.{v₁, u₁, v, u} (C : Type u) [Category'.{v} C] : Prop where
  has_limits_of_shape : ∀ (J : Type u₁) [Category'.{v₁} J], True

instance foo.{u_1, u_2} :
    HasLimitsOfSize'.{u_1, u_1, max u_1 u_2, (max u_1 u_2) + 1} TopCat'.{max u_1 u_2} :=
sorry

def bar.{u_1, u_2} :
    HasLimitsOfSize'.{u_1, u_1, max u_1 u_2, (max u_1 u_2) + 1} TopCat'.{max u_1 u_2} :=
inferInstance
/-
stuck at solving universe constraint
  max u_1 u_2 =?= max u_1 ?u.98
while trying to unify
  HasLimitsOfSize' TopCat'
with
  (HasLimitsOfSize' TopCat') (HasLimitsOfSize' TopCat') (HasLimitsOfSize' TopCat')
-/

[Kevin Buzzard]

The error message here seems pretty borked though:

Yeah, that was already observed by Jeremy Tan in another thread. There's a lot of repetition.

[Kevin Buzzard]

My example shows that there's an issue even without the universe order switch.

[Kevin Buzzard]

Note also the incorrect repetitions in the error message.

[Gabriel Ebner]

I think we understand now pretty well what Lean code triggers this issue. It happens whenever we have two types and we want one of them to live in a bigger universe than the other. All of the examples in this thread are of this form:

class Something (A : Type u) (B : Type v)
instance whenUniversesLE (A : Type u) (B : Type max u v) : Something A B where
example (A : Type u) (B : Type max u v) : Something A B := inferInstance -- fails

[Gabriel Ebner]

What I still don't completely get is where these constraints come from in the first place, and how essential they are. Could we replace them by a Type u ↪ Type v assumption?

[Matthew Ballard]

I’m curious. What do you have in mind?

[Johan Commelin]

@Gabriel Ebner They come from the fact that we want to support both small categories and large categories: https://en.wikipedia.org/wiki/Category_(mathematics)#Small_and_large_categories

[Kevin Buzzard]

Reid posted an example of why we care about universe inequalities: the category Type u has v-small limits if v <= u and doesn't have them if v > u.

[Johan Commelin]

In pseudo-code:

GroupCat := Σ (G : Type u), GroupStructure G
#check GroupCat : Type (u+1) -- the large universe

variables (G₁ G₂ : GroupCat)
#check G₁ ⟶ G₂ : Type u -- the small universe

[Johan Commelin]

Here's a wild thought: we could have syntax for v ≤ u, and the kernel could run a micro-version of omega (probably omicron?) to check that universe constraints are satisfied.
I have no idea how realistic this is performancewise....

[Gabriel Ebner]

Thanks Kevin for spelling this out to me.

[Matthew Ballard]

It guarantees you can quantify over some things without bumping universe levels for the objects.

[Matthew Ballard]

If universe inequalities are a feasible option, that would be great.

[Adam Topaz]

I'm just playing around with some ideas for now.

import Mathlib

class ULE.{u,v} : Prop where
  cond : Nonempty (Cardinal.{u} ↪ Cardinal.{v})

instance [ULE.{u,v}] [ULE.{v,w}] : ULE.{u,w} where
  cond := by
    obtain ⟨a⟩ := ULE.cond.{u,v}
    obtain ⟨b⟩ := ULE.cond.{v,w}
    exact ⟨a.trans b⟩

instance : ULE.{u,u} where
  cond := ⟨Function.Embedding.refl _⟩

instance : ULE.{u,u+1} where
  cond := ⟨Cardinal.lift.{u+1}, Cardinal.lift_injective⟩

--instance : ULE.{u, max v u} where
--  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩

--instance : ULE.{u, max u v} where
--  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩

example [ULE.{u,v}] [ULE.{v,w}] [ULE.{w,v'}] : ULE.{u,v'} := inferInstance

If you uncomment one or both of the the two commented out instances, then the last one fails. Does TC search just stop when it can't unify universes? That seems strange.

[Gabriel Ebner]

I think this runs into the same issue as this thread. The two commented instances require unifying max u ?v = max u v.

[Adam Topaz]

right, that's what I figured. But once this fails, why doesn't TC search just keep going?

[Gabriel Ebner]

Oh, it keeps going. But what happens is that it con't solve the unification constraint immediately, and postpones it. So it actually "successfully" returns an instance. It's only at the very end that it figures it can't solve max u ?v = max u v and fails.

[Adam Topaz]

Ah I see.

[Adam Topaz]

I guess that's why reordering things works:

import Mathlib

class ULE.{u,v} : Prop where
  cond : Nonempty (Cardinal.{u} ↪ Cardinal.{v})

instance : ULE.{u,u} where
  cond := ⟨Function.Embedding.refl _⟩

instance : ULE.{u,u+1} where
  cond := ⟨Cardinal.lift.{u+1}, Cardinal.lift_injective⟩

instance : ULE.{u, max v u} where
  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩

instance : ULE.{u, max u v} where
  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩

instance [ULE.{u,v}] [ULE.{v,w}] : ULE.{u,w} where
  cond := by
    obtain ⟨a⟩ := ULE.cond.{u,v}
    obtain ⟨b⟩ := ULE.cond.{v,w}
    exact ⟨a.trans b⟩

example [ULE.{u,v}] [ULE.{v,w}] [ULE.{w,v'}] : ULE.{u,v'} := inferInstance

[Adam Topaz]

Is this intended?

[Gabriel Ebner]

I mean, yeah. What instances are tried first depends among other things on the order they're declared in. (If the order is important, it's better to put a priority on the instance though.) In this case, one instance works out at the end while another one blows up.

[Adam Topaz]

Sure, that I understand. But I still find it strange that lean remembers the universe unification problem from a failed attempt, and then tries the same problem on a successful attempt later on.

[Adam Topaz]

But of course I know nothing about the internals of the typeclass system, and there's probably a good reason for this which I don't understand.

[Gabriel Ebner]

lean remembers the universe unification problem from a failed attempt

From Lean's POV, it was a successful attempt!

[Adam Topaz]

hmm... okay now I'm confused again :)

[Adam Topaz]

Ah okay I see. The TC trace is as follows:

import Mathlib

/-- foo -/
class ULE.{u,v} : Prop where
  /-- bar -/
  cond : Nonempty (Cardinal.{u} ↪ Cardinal.{v})
instance [ULE.{u,v}] [ULE.{v,w}] : ULE.{u,w} where
  cond := by
    obtain ⟨a⟩ := ULE.cond.{u,v}
    obtain ⟨b⟩ := ULE.cond.{v,w}
    exact ⟨a.trans b⟩

instance rfl_ULE : ULE.{u,u} where
  cond := ⟨Function.Embedding.refl _⟩

instance succ_ULE : ULE.{u,u+1} where
  cond := ⟨Cardinal.lift.{u+1}, Cardinal.lift_injective⟩

instance max_right_ULE : ULE.{u, max v u} where
  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩

instance max_left_ULE : ULE.{u, max u v} where
  cond := ⟨Cardinal.lift.{v}, Cardinal.lift_injective⟩


set_option pp.universes true in
set_option trace.Meta.synthInstance true in
example [ULE.{u,v}] [ULE.{v,w}] [ULE.{w,v'}] : ULE.{u,v'} := inferInstanc

[Meta.synthInstance] ✅ ULE.{u, v'} ▼
  [] new goal ULE.{u, v'} ▶
  [] ❌ apply inst✝ to ULE.{u, v'} ▶
  [] ❌ apply inst✝¹ to ULE.{u, v'} ▶
  [] ❌ apply inst✝² to ULE.{u, v'} ▶
  [] ✅ apply max_left_ULE.{?u.238, u} to ULE.{u, v'} ▼
    [tryResolve] ✅ ULE.{u, v'} ≟ ULE.{u, max u ?u.238}
  [] result max_left_ULE.{?u.240, u}

so for some reason typeclass search stops thinking it succeeded, and only then tries to unify universes which causes a failure.

[Gabriel Ebner]

Okay, Lean tries to apply ULE.{?u, max ?u ?v} to the ULE.{u,v'} in the example. It can unify ?u = u so it does that right away. But it can't solve max u ?v = v' just yet, so it puts it on a todo list somewhere to figure out later. Maybe something down the line will give us a value for ?v, maybe when we solve one of the subgoals, who knows? But there are no more subgoals, so Lean declares the instance a complete success. Does that make sense?

[Adam Topaz]

Yes, I think I understand. Thanks for the explanation!

[Adam Topaz]

Matthew Ballard said:

If you delete the universe annotations, it seems to work

Unfortunately, lean does not choose appropriately general universes in this case:

def piIsoPi {ι : Type v} (α : ι → TopCat) :
  ∏ α ≅ TopCat.of (∀ i, α i) :=
  (limit.isLimit _).conePointUniqueUpToIso (piFanIsLimit α)
#align Top.pi_iso_pi TopCat.piIsoPi

set_option pp.universes true in #check piIsoPi

/-
TopCat.piIsoPi.{v} {ι : Type v} (α : ι → TopCat.{v}) :
  Iso.{v, v + 1} (piObj.{v, v, v + 1} α) (of.{v} ((i : ι) → (α i).α))
-/

Replacing v with _ gives this result:

{ι : Type (max u_1 u_2)} →
  (α : ι → TopCat.{max u_1 u_2}) →
    Iso.{max u_1 u_2, (max u_1 u_2) + 1} (piObj.{max u_1 u_2, max u_1 u_2, (max u_1 u_2) + 1} α)
      (of.{max u_1 u_2} ((i : ι) → (α i).α))

I fiddled for a bit with specifying universes explicitly for this declaration, but I just couldn't get things to work out.

[Mario Carneiro]

At the porting meeting it was suggested that this problem could be addressed by using a constant with separate universe arguments to avoid trying to unify two max expressions directly. Here is an example of using that technique to solve all the MWEs in this thread:

abbrev BigType.{u, v} := Type max u v
namespace X
universe u v
def foo : Type u × BigType.{u,v} := (PUnit, PUnit)
#check (foo : Type u × BigType.{u,v})
end X

section
universe v u

class Foo (C : Type u) where
  Bar : Type v
end

section

universe v' v u' u

class Bar (C : Type u) [Foo.{v} C] (D : Type u') [Foo.{v'} D] where
  Baz : Type (max (max u' u) v)

end

section

universe v u
variable (C : BigType.{u+1, v+1}) (D : Type v)
  [Foo.{max v u} C] [Foo.{v} D]

instance : Bar.{v} C D := sorry

example : Bar.{v} C D := inferInstance

class Category (C : Type u) where
  Morphisms : Type v
abbrev BigCategory (C : BigType.{u, v'}) := Category.{v} C

class HasLimitsOfShape (C : Type u) [Category.{v} C] (D : Type u') [Category.{v'} D] where
  Limits : Type max u' u v
abbrev BigHasLimitsOfShape (C : BigType) [Category C] (D : Type u') [Category.{v'} D] :=
  HasLimitsOfShape C D

variable (C : BigType.{u, v}) (D : Type v) [Category C] [Category.{v} D]

instance : BigHasLimitsOfShape.{v} C D := sorry

example : BigHasLimitsOfShape.{v} C D := inferInstance

end

section
-- set_option pp.universes true

class Quiver'.{v, u} (V : Type u) where
  Hom : V → V → Sort v

class Category'.{v, u} (obj : Type u) extends Quiver'.{v + 1} obj : Type max u (v + 1) where
abbrev BigCategory'.{v, u, u'} (C : BigType.{u, u'}) := Category.{v} C

def TopCat'.{u} : Type (u + 1) := PUnit
abbrev BigTopCat'.{u, v} : BigType.{u+1,v+1} := TopCat'

instance moo.{u} : Category'.{u, u + 1} TopCat' := sorry

class HasLimitsOfSize'.{v₁, u₁, v, u} (C : Type u) [Category'.{v} C] : Prop where
  has_limits_of_shape : ∀ (J : Type u₁) [Category'.{v₁} J], True

instance foo : HasLimitsOfSize' BigTopCat' := sorry

def bar : HasLimitsOfSize' BigTopCat' := inferInstance

end

class Something (A : Type u) (B : Type v)
instance whenUniversesLE (A : Type u) (B : BigType.{u, v}) : Something A B where
example (A : Type u) (B : BigType.{u, v}) : Something A B := inferInstance -- fails

[Scott Morrison]

Except you need to remove the -- fails on the last line, as happily it doesn't fail! :-)

[Kevin Buzzard]

Interesting idea! Sorry I wasn't at the meeting yesterday, it coincided with family dinner. But this universe issue is "blocking Copenhagen" so thanks a lot for looking at it!

[Adam Topaz]

Nice! How could we use this in the TopCat example? I suppose we could redefine it as TopCat.{u,v} to cave carrier Type (max u v). Would that cause issues in the case where u=v?

[Mario Carneiro]

I think I did the TopCat example

[Mario Carneiro]

the basic strategy is to make a BigTopCat wrapper when you want to be able to separately unify the u and v arguments of a max u v universe somewhere

[Adam Topaz]

Ah I see.

[Mario Carneiro]

Since everything here is an abbrev, it should not seriously block any unification problem when lean is in tryhard mode, but it gives a bit of extra hint in some cases. Notably, (rfl : BigType.{u, v} = BigType.{v, u}) fails, although using Eq.refl (Type _) works as a proof

[Mario Carneiro]

my hope is that these tricks only need to be used in some implementation detail instances, so most theorems can still be stated "naturally"

[Yaël Dillies]

And if you want Type max u v w you define BigBigType.{u, v, w}?

[Mario Carneiro]

Note that the two universes in BigType are not really interchangeable and I expect we will come up with some convention regarding which is the unbound universe and which is the bound one. For Type max u v w I would expect only one unbound universe and hence BigType.{u, max v w} should suffice

[Adam Topaz]

Yeah we will probably need to stick to the old "universe level of morphisms come before objects"

[Matthew Ballard]

Thanks Mario! Is this viewed as a workaround until something changes upstream or something more permanent?

[Mario Carneiro]

I have no idea what the prospects are for something better, as all the proposed solutions are at various levels of pie in the sky

[Adam Topaz]

I'm trying to make this trick work for the following decl:

def piIsoPi {ι : Type v} (α : ι → TopCat.{max v u}) :
  ∏ α ≅ TopCat.of (∀ i, α i) :=
  (limit.isLimit _).conePointUniqueUpToIso (piFanIsLimit α)

[Adam Topaz]

But I'm still getting the error:

stuck at solving universe constraint
  max u v =?= max v ?u.56877
while trying to unify
  HasLimitsOfSize TopCat
with
  (HasLimitsOfSize BigTopCat) (HasLimitsOfSize BigTopCat) (HasLimitsOfSize BigTopCat)

[Adam Topaz]

Even this

def piIsoPi {ι : Type v} (α : ι → BigTopCat.{v, u}) :
  ∏ α ≅ BigTopCat.of (∀ i, α i) :=
  sorry

gives an error

stuck at solving universe constraint
  max (u+1) (v+1) =?= max (?u.57707+1) (?u.57708+1)
while trying to unify
  Type (max u v) : Type (max (u + 1) (v + 1))
with
  Type (max ?u.57708 ?u.57707) : Type ((max ?u.57708 ?u.57707) + 1)

[Adam Topaz]

And besides we want the type of this def to not involve BigTopCat, I suppose.

[Mario Carneiro]

you might need to define BigHasLimitsOfSize

[Kevin Buzzard]

I think you might want to avoid max v u on the basis that Lean occasionally applies a universe normalisation procedure which changes this to the alphabetically-ordered max u v.

[Mario Carneiro]

I don't think this will matter in practice since the sorting is relative to alphabetical order in the usage code, not the constant declaration

[Mario Carneiro]

also, exactly because lean 4 refuses to unify max problems, the unification algorithm is independent of variable ordering, which is why the alphabetic canonicalization is fine and should not result in any observable differences

[Adam Topaz]

Mario Carneiro said:

you might need to define BigHasLimitsOfSize

I'm not sure what you're suggesting with this.

[Adam Topaz]

I don't see how to get this BigTopCat to work nicely with a declaration such as

def piIsoPi {ι : Type v} (α : ι → TopCat.{max v u}) :
  ∏ α ≅ TopCat.of (∀ i, α i) := ...

[Adam Topaz]

The issue is that lean needs some instance with problematic universes to even talk about ∏ α. I could rewrite everything in terms of BigTopCat as

def piIsoPi {ι : Type v} (α : ι → BigTopCat.{v, u}) :
  ∏ α ≅ BigTopCat.of.{v,u} (∀ i, α i) := ...

but that doesn't help us because we want this isomorphism for TopCat and not for BigTopCat.

[Kevin Buzzard]

Mario Carneiro said:

I don't think this will matter in practice since the sorting is relative to alphabetical order in the usage code, not the constant declaration

Does this example contradict your claim?

[Matthew Ballard]

Here is something that gets the correct signature with proper universe parameters but is unpleasant.

def piIsoPi.{a,b} {ι : Type b} (α : ι → TopCat.{max a b}) :
@limit (Discrete.{b} ι) _ TopCat.{max a b} _ (Discrete.functor α) (by
have I := topCat_hasLimitsOfSize.{a,b}; infer_instance) ≅ TopCat.of ((i:ι) → α i) := sorry

[Kevin Buzzard]

(deleted)

[Scott Morrison]

I hadn't realised until now how badly these universe constraints had borked https://github.com/leanprover-community/mathlib4/pull/2712. There's all these haveI := hasLimit.{v, v}s that we probably shouldn't have merged.

[Scott Morrison]

Could I propose before we go further with experiments here that we rename Mario's BigType to TypeMax (and similarly for other uses of Big)?

[Matthew Ballard]

Can we do something silly like

instance [HasLimitsOfMaxSize] : HasLimitsOfSize

?

[Scott Morrison]

Okay, I have used TypeMax to fix CategoryTheory.Limits.Types, and it is seamless.

[Scott Morrison]

I did not attempt to minimise the use of TypeMax; I just put it everywhere we previously had Type max.

[Scott Morrison]

We can drop every haveI from that file as a result.

[Scott Morrison]

https://github.com/leanprover-community/mathlib4/pull/3653

[Scott Morrison]

Where should TypeMax live?

[Matthew Ballard]

Mathlib.Data.TypeMax?

[Matthew Ballard]

Do we still have ReflectedUniv?

[Scott Morrison]

TopCatMax seems to help in !4#3464, so I have pushed a merge with !4#3653 and made the "low-hanging fruit" changes. There is still a lot of work on this file, and it is marked as help-wanted, so please jump in. :-)

[Matthew Ballard]

One of the hardest problems in CS ;) obtuse way to saying !4#3463

[Adam Topaz]

I'm not sure how I feel about this... for example, this still fails, even with the TypeMax change:

import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Shapes.Products

example {α : Type v} (f : α → Type (max v u)) : Type (max v u) := ∏ f

[Mario Carneiro]

Kevin Buzzard said:

Mario Carneiro said:

I don't think this will matter in practice since the sorting is relative to alphabetical order in the usage code, not the constant declaration

Does this example contradict your claim?

No, because that's not a defeq problem, you are just calling the level normalizer as a bare function. The meaning of that function depends on the context in which it is used. One reason why that kind of normalization is important (any consistent normalization, alphabetical or otherwise) is because lean wants to be able to use normalize l1 == normalize l2 as a way to prove that l1 and l2 are defeq, so this is exactly what you need to make max u v = max v u be a defeq.

[Mario Carneiro]

(I am of course fine with the name change. I spent about half a second on the name choice)

[Scott Morrison]

Adam Topaz said:

I'm not sure how I feel about this... for example, this still fails, even with the TypeMax change:

import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Shapes.Products

example {α : Type v} (f : α → Type (max v u)) : Type (max v u) := ∏ f

Here

example {α : Type v} (f : α → Type (max v u)) : TypeMax.{v, u} := ∏ f

does work, but it's not quite up to Mario's "my hope is that these tricks only need to be used in some implementation detail instances".

[Mario Carneiro]

I think you rather want f : A -> TypeMax.{v, u} here

[Mario Carneiro]

the output universe probably doesn't have to be a TypeMax

[Scott Morrison]

No, unfortunately that gives the same error message!

[Scott Morrison]

import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Shapes.Products

example {α : Type v} (f : α → Type (max v u)) : Type (max v u) := ∏ f -- fails
example {α : Type v} (f : α → Type (max v u)) : TypeMax.{v, u} := ∏ f -- succeeds
example {α : Type v} (f : α → TypeMax.{v, u}) : Type (max v u) := ∏ f -- fails
example {α : Type v} (f : α → TypeMax.{v, u}) : TypeMax.{v, u} := ∏ f -- succeeds

[Mario Carneiro]

What is the type of pi?

[Scott Morrison]

abbrev piObj (f : β → C) [HasProduct f] : C :=
  limit (Discrete.functor f)

notation "∏ " f:20 => piObj f

[Mario Carneiro]

I think this will work if pi is expecting a TypeMax function

[Mario Carneiro]

what is the "source" of the max v u here?

[Scott Morrison]

That the category Type u has Type v indexed products iff v <= u?

[Mario Carneiro]

how about "the category TypeMax.{v, u} has Type v indexed products"

[Scott Morrison]

The actual instance is:

CategoryTheory.Limits.Types.hasLimit.{v, u} {J : Type v} [inst✝ : SmallCategory.{v} J]
  (F : Functor.{v, max u v, v, max (u + 1) (v + 1)} J TypeMax.{v, u}) : HasLimit.{v, v, max u v, max (u + 1) (v + 1)} F

[Mario Carneiro]

So how did Type max v u get involved?

[Mario Carneiro]

I suppose it's right in the example

[Scott Morrison]

Adam wanting it to work "for the user" without having to know about TypeMax, I think.

[Scott Morrison]

Currently piObj is excessively general:

CategoryTheory.Limits.piObj.{w, v, u} {β : Type w} {C : Type u} [inst✝ : Category.{v, u} C] (f : β → C)
  [inst✝¹ : HasProduct.{w, v, u} f] : C

[Scott Morrison]

In practice HasProduct.{w, v, u} instances with unbounded w are never ever going to exist, so perhaps we should just reformulate this using TypeMax CategoryMax (which doesn't yet exist).

[Mario Carneiro]

I think it will push in the opposite direction, you want to try not to ever mention Type (max v u), TypeMax is "a universe with v-morphisms at least as large as u"

[Mario Carneiro]

"for the user" they won't be using Type (max u v) they will be using Type v or Type (v + 1)

[Mario Carneiro]

As long as maxes (with unbound universes) are involved you want to stick with TypeMax

[Scott Morrison]

I'm pretty happy with that. We can put a "don't use max in the category theory library" sticker somewhere. :-)

[Scott Morrison]

!4#3653 is hopefully almost ready to go for TypeMax. Would someone (@Mario Carneiro? @Adam Topaz?) be willing to contribute a doc-string for TypeMax, and hit merge? I can have a go tomorrow if no one has got to it.

After that, !4#3487 (Topology.Category.Top.Limits) should be ready to go! (In its new post #18871 chopped down form.)

[Adam Topaz]

Mario Carneiro said:

"for the user" they won't be using Type (max u v) they will be using Type v or Type (v + 1)

This doesn't quite work out, e.g. with the following:

import Mathlib.CategoryTheory.Limits.Shapes.Types

example {α : Type v} (f : α → Type v) : ∏ f ≅ (∀ i, f i) :=
  CategoryTheory.Limits.Types.productIso f

[Adam Topaz]

stuck at solving universe constraint
  max v ?u.293 =?= v
while trying to unify
  α → α → TypeMax : Type (max (v + 1) (?u.293 + 1))
with
  α → Type v : Type (v + 1)

[Adam Topaz]

well, in this case

noncomputable example {α : Type v} (f : α → Type v) : ∏ f ≅ (∀ i, f i) :=
  CategoryTheory.Limits.Types.productIso.{v,v} f

works out, so maybe that's okay.

[Adam Topaz]

And yes, my main concern with TypeMax TopCatMax etc. is the user experience

[Adam Topaz]

It's funny, library_search finds CategoryTheory.Limits.Types.productIso f, but then results in the error above without the universe annotations.

[Adam Topaz]

Anyway, I think TypeMax is a good solution to let us move forward with the port. But it means that we will have yet another confusing thing to explain to newcomers who want to interact with the category theory library.

[Kevin Buzzard]

Adam Topaz said:

And yes, my main concern with TypeMax TopCatMax etc. is the user experience

We've had concerns with the user experience before in category theory (e.g. "please write universes v u and not universes u v", and "please write [\McC : category C] instead of [category C]"), and basically they were solved over time as the system got better.

[Matthew Ballard]

Are we waiting for #18871 to go through mathport before dealing with the other files? There are quite a few fixes in the other chunks that were made from the original mathport output.

[Matthew Ballard]

Scott Morrison said:

!4#3653 is hopefully almost ready to go for TypeMax. Would someone (Mario Carneiro? Adam Topaz?) be willing to contribute a doc-string for TypeMax, and hit merge? I can have a go tomorrow if no one has got to it.

I wrote something for the documentation.

[Scott Morrison]

Yes, I think we can wait for mathport for the other files. Unfortunate my hasty approach here means we will need to retrieve the fixes from the other chunks from git history. :-(

[Scott Morrison]

Thanks Matthew for the docs. Can someone merge !4#3653 now?

[Matthew Ballard]

Scott Morrison said:

Yes, I think we can wait for mathport for the other files. Unfortunate my hasty approach here means we will need to retrieve the fixes from the other chunks from git history. :-(

I’ve got them on my local machine :)

[Adam Topaz]

Quick report re TypeMax and friends: I just ported CompHaus.Basic in !4#3688 and had to actually use TopCatMax. With just a little hint for lean, I didn't have to introduce CompHausMax! See https://github.com/leanprover-community/mathlib4/blob/76e8aeb932d9637fef67f8444bc8ae7c39c277cb/Mathlib/Topology/Category/CompHaus/Basic.lean#L252

[Matthew Ballard]

I’ve started the process of migrating the changes from !4#3487 to the new files in the Limits folder with !4#3709. I probably won’t have much time for addressing the remaining errors until Monday. Please feel free to help rectifying it.

[Joël Riou]

If everything fails, another approach would be to implement universe inequalities like:

import Mathlib.Logic.Small.Basic

universe u₁ u₂

class UnivLE where
  condition : ∀ (α : Type u₁), Small.{u₂} α

def ULiftOfLE [UnivLE.{u₁, u₂}] (α : Type u₁) : Type u₂ :=
  @Shrink α (UnivLE.condition.{u₁, u₂} α)

noncomputable def equivULiftOfLE [UnivLE.{u₁, u₂}] (α : Type u₁) : α ≃ ULiftOfLE.{_, u₂} α :=
  @equivShrink α (UnivLE.condition.{u₁, u₂} α)

Then, for example, under the assumption [Univ.Le.{u₁, u₂}], we could ensure that some limits/colimits in Type u₂ indexed by some J : Type u₁ exists by transporting the index set to Type u₂. But I hope the TypeMax approach will work...

[Adam Topaz]

I think this approach still has similar issues with max. See the code I posted way up in this thread with ULE.

[Joël Riou]

What I would suggest is to make the definitions more universe polymorphic, by mostly getting rid of the max u v universe parameters in the assumptions, replacing it with some w and suitable assumptions UnivLE.{u, w}.

[Adam Topaz]

But would you want an instance for UnivLE.{u, max u v}? Maybe I’m misunderstanding the proposal

[Joël Riou]

In my proposal, there are no longer any max u v we have to cope with!

[Adam Topaz]

What about Module.{u} R where R : Type v?

[Adam Topaz]

Oh maybe that’s just in Type (u+1), but I think you get my point. Categories living in some max universe can arise naturally, so we would have to introduce instances for UnivLE for max, which would result in similar issues

[Yaël Dillies]

I think Joël's point is that we would never introduce max u v but instead always work "in a big enough universe".

[Yaël Dillies]

And in particular your "category living in some max universe" would instead be a "category living in any big enough universe".

[Adam Topaz]

Okay, here is an actual example: docs4#CategoryTheory.StructuredArrow

[Adam Topaz]

How do you propose to say that this category has a big enough universe without using max?

[Adam Topaz]

Another docs4#CategoryTheory.Over

[Joël Riou]

This Module.{u} R : Type (max v (u+1)) is a problem only if the categorical constructions you want to do with it are not enough universe polymorphic. This is why I suggest we could try to avoid assuming categories have special universe parameters: then, it would apply to any category, even Module.{u} R.

[Yaël Dillies]

Replace

universe v₁ v₂ u₁ u₂
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]

def StructuredArrow (S : D) (T : C ⥤ D) : Type (max u₁ v₂) :=
  Comma (Functor.fromPUnit S) T

with

universe v₁ v₂ u₁ u₂ w
variable [UnivLE.{u₁, w} [UnivLE.{v₂, w}]
  {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]

def StructuredArrow (S : D) (T : C ⥤ D) : Type w :=
  Comma (Functor.fromPUnit S) T

[Joël Riou]

@Yaël Dillies: this is not what I suggest. I suggest attempting at replacing variable (X : Type (max u v)) by variable (X : Type w), and if it is needed somewhere, we would add the assumption UnivLE.{u, w}.

[Yaël Dillies]

Ah then I agree with Adam that it won't work!

[Joël Riou]

I am not saying it would solve all the universe issues: sometimes we may still have to remind Lean that UnivLE.{u, max u v} holds because this cannot be an instance, but this is not my definition of "it won't work".

[Scott Morrison]

Some more news on TypeMax.

First, if someone could review #5535, that would be great. It does a slight universe generalization, but mostly it documents some of the difficulties with instances involving TypeMax.

[Scott Morrison]

I've been working on forward porting !3#19153, and have #5536, which fails due to max u v =?u max u ?v errors, and #5534, which is the same except that it uses a patched version of Lean 4 and succeeds.

[Scott Morrison]

@Heather Macbeth, would you mind reviewing #5534 to check that it really did forward port the changes from !3#19153?

This can either be done "by hand" by comparing the diffs, or by going to #out-of-sync, clicking on each file affected by !3#19153, and then clicking "Overall diff" in the left pane (this shows the diff between the SHA in the header and mathlib3 master).

[Scott Morrison]

The motivation for the patch to Lean 4 is described at https://github.com/leanprover/lean4/issues/2297, and the patch itself is at https://github.com/leanprover/lean4/issues/2298. The verification that mathlib4 doesn't mind the patch is at #5416.