[Merged by Bors] - chore: Forward-port leanprover-community/mathlib#19230

[YaelDillies]

This doesn't forward-port the removal of .{u} as this doesn't actually change the type, and just results in .{u_1} being implied instead.

---

This forward-ports the revert (leanprover-community/mathlib#19230) of changes that were never forward-ported (leanprover-community/mathlib#19153). Therefore only the SHA needs updating.

[urkud]

Thanks! 🎉
bors merge

[eric-wieser]

bors r-

@YaelDillies, I'm confused by this claim. If you look at the file in its current state, it mentions (X : Scheme.{u}) not (X : Scheme). Are you sure we shouldn't be forward-porting the removal of the {u}?

[bors]

Canceled.

[YaelDillies]

@semorrison, can you explain more? The history for the mathlib4 file contains no PR that claims to forward-port leanprover-community/mathlib#19153, so I am confusion.

[eric-wieser]

I suspect it was forward-ported while the file was still in progress

[eric-wieser]

We should either:

• Update the mathlib4 file to reflect the content that mathport is outputting, whether or not the diff makes sense
• Update the mathlib3 file to reflect the version that was put into mathlib4 (i.e. revert the revert)

Probably only Scott can say which of these is correct

[semorrison]

These file have already diverged from mathlib3 due to the UnivLE experiments. Any discrepancies are mathlib3's problem, at this point. :-)

[semorrison]

We tried to forward port 19153, failed, and so reverted it back in mathlib3. Instead we've introduced the UnivLE mechanism to deal with universe inequalities where Lean 4 can't cope with the max u v unification problems.

[YaelDillies]

So should this file appear on out-of-sync, yes or no? Scott, as the author of the mathlib changes, this is your responsability.

[semorrison]

I'll make a SHA only PR now.

[semorrison]

This is already a SHA only PR... I don't understand why the bors merge was cancelled in the first place.

bors merge

[bors]

Canceled.

[eric-wieser]

bors merge

I don't know why we didn't just forward-port the diff here...

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style