!4#3208 merge conflicts

Stream: mathlib4

[Kevin Buzzard]

I thought I'd try and help with porting CategoryTheory.Limits.Presheaf this PR as it's on the path to a file I want to see ported, but I'm confused by the conflicts. Why are changes in a normed space file anything to do with porting a category theory file?

!4#3208

[Scott Morrison]

I agree it is strange. I just had the same merge conflicts on another PR, and just accepting the incoming changes seemed to give the right diff, so I've done that again on this PR for you!

[Eric Wieser]

You need to rebase on master

[Eric Wieser]

See the "force push" thread

[Scott Morrison]

Ugh, still that.

[Eric Wieser]

These PRs are tricky, because everyone with a local copy on their machine is affected

[Eric Wieser]

So really the "owner" should do the rebase

[Eric Wieser]

It would be straightforward for me to fix all of the remaining PRs affected by this on github, but then everyone with a local copy they are working on will end up in a mess if they're not experienced with git

[Scott Morrison]

Why don't we straightforwardly fix them all with a merge, instead, so then everyone with a local copy can simply pull?

[Scott Morrison]

The rebase is just annoying for everyone else with a copy, while the merge solves the problem, no?

[Eric Wieser]

The merge require manual effort to resolve conflicts, the rebase resolves them automatically

[Eric Wieser]

It also makes a mess of the bors author and claims the PR is Jeremy's... (Along with 12 or so other people)