Mathlib bump to v4.16.0-rc2

Stream: FLT

[Kim Morrison]

Mathlib is now at v4.16.0-rc2, and I've verified lake exe cache get is working again within FLT. However there are a number of breakages from Mathlib having moved along, so I'll leave it to you all to do the bump!

[Kim Morrison]

oh, whatever, I got sucked in: FLT#311

[Kim Morrison]

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean is not done yet

[Kim Morrison]

and there are three new sorries about .Finite assumptions that seem to be new, marked with a comment

[Ruben Van de Velde]

I may have time to look at the remaining issues later this morning

[Kevin Buzzard]

I will have time at 2025-01-14T10:45:00Z but not before

[Ruben Van de Velde]

Looking for a bit now

[Ruben Van de Velde]

Typeclass inference seems to go haywire - this is as far as I got: https://github.com/Ruben-VandeVelde/FLT-Wiles/commit/7dfe26c2821fa6a9d227965a2c901a41609b5120

[Kevin Buzzard]

I still haven't had time to deal with this and I have more admin to deal with before I start running Lean Together so I might not get to this today.

[Ruben Van de Velde]

FLT#313 finishes the bump

[Kevin Buzzard]

I'll try to review this weekend -- thanks so much!

[Kevin Buzzard]

Merged!