two branches differing only through capitalization

Stream: mathlib4

[Sébastien Gouëzel]

@Anne Baanen , you are owning two different branches integrallyClosedIn and IntegrallyClosedIn. Windows doesn't like that, unfortunately. Could you delete or rename one of them?

[Junyan Xu]

On the other hand, Mac doesn't like checking out a branch where a file name's capitalization is changed ... many times I had to delete the file before checkout, but I later find out I can force checkout.

[Anne Baanen]

Oops! integrallyClosedIn is the correct one. GitHub UI doesn't even display the IntegrallyClosedIn branch so I had to try and remember which magic commands delete it on the server - did I do it right?

[Sébastien Gouëzel]

Perfect, thanks!

[Junyan Xu]

This is causing issues when running the migration script scripts/migrate_to_fork.py on Windows:

=== Step 4: Setting up git remotes ===
✗ Command failed: git fetch --all --prune
✗ Error: error: could not delete references: cannot lock ref 'refs/remotes/origin/integrallyClosedIn': Unable to create '.../mathlib4/.git/refs/remotes/origin/integrallyClosedIn.lock': File exists.

Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.

and my solution is

git branch -d -r origin/integrallyClosedIn