Bump Lean to 4.11.0-rc2

[sgouezel]

Warning: since it changes the Lean and mathlib version, you will need to redownload the cache once you have merged this one, by doing lake exe cache get (and if this one fails, then erase your .lake folder and do lake exe cache get again).

The main change in the new Lean version is that the rule for variables inclusion has changed (see leanprover/lean4#4814). The short version is that variables that are not mentioned in the statement of a theorem are not included by default (so you need to do

include h_indep in
theorem ...

to make sure that h_indep is available in the proof), and that all typeclasses about objects in the statement are included by default (so sometimes spurious typeclasses are included, which can be avoided by reorganizing things if desired, or one can live with the spurious typeclasses). This is a big change, that increases predictability (before that, what variables were included in a theorem could depend on the proof of the theorem, so changing a proof could change the statement of the theorem, which has bitten us prety badly several times).