[Merged by Bors] - chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0

[kim-em]

---

[github-actions]

PR summary c100c8f24a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.DeriveToExpr	21	0	-21 (-100.00%)
Mathlib.Tactic.ToExpr	23	19	-4 (-17.39%)
Mathlib.Tactic.ITauto	46	43	-3 (-6.52%)
Mathlib.Algebra.BigOperators.Group.List	390	385	-5 (-1.28%)
Mathlib.Tactic.Common	237	234	-3 (-1.27%)
Mathlib.Data.Vector.Basic	403	398	-5 (-1.24%)
Mathlib.Data.List.Basic	284	281	-3 (-1.06%)
Mathlib.Data.List.Lex	287	284	-3 (-1.05%)
Mathlib.Data.List.Chain	290	287	-3 (-1.03%)
Mathlib.Computability.TuringMachine	489	484	-5 (-1.02%)
Mathlib.Data.QPF.Multivariate.Constructions.Fix	513	508	-5 (-0.97%)
Mathlib.Data.List.MinMax	317	314	-3 (-0.95%)
Mathlib.Data.Fin.Basic	334	331	-3 (-0.90%)
Mathlib.Data.Fin.Tuple.Basic	336	333	-3 (-0.89%)
Mathlib.Data.Fin.Tuple.Take	337	334	-3 (-0.89%)
Mathlib.Data.List.Lemmas	337	334	-3 (-0.89%)
Mathlib.Data.Nat.Bitwise	337	334	-3 (-0.89%)
Mathlib.Data.String.Basic	337	334	-3 (-0.89%)
Mathlib.Order.Fin.Basic	348	345	-3 (-0.86%)
Mathlib.Data.Int.Bitwise	349	346	-3 (-0.86%)
Mathlib.Data.List.Permutation	350	347	-3 (-0.86%)
Mathlib.Algebra.BigOperators.Fin	584	579	-5 (-0.86%)
Mathlib.Computability.TMToPartrec	611	606	-5 (-0.82%)
Mathlib.Deprecated.LazyList	385	382	-3 (-0.78%)
Mathlib.ModelTheory.Semantics	654	649	-5 (-0.76%)
Mathlib.LinearAlgebra.Matrix.SemiringInverse	741	736	-5 (-0.67%)
Mathlib.SetTheory.Ordinal.Notation	741	736	-5 (-0.67%)
Mathlib.Data.Int.Lemmas	469	466	-3 (-0.64%)
Mathlib.LinearAlgebra.LinearIndependent	885	880	-5 (-0.56%)
Mathlib.Tactic.Linarith.Frontend	548	545	-3 (-0.55%)
Mathlib.CategoryTheory.Galois.Decomposition	955	950	-5 (-0.52%)
Mathlib.Algebra.MvPolynomial.SchwartzZippel	1076	1071	-5 (-0.46%)
Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms	1127	1122	-5 (-0.44%)
Mathlib.LinearAlgebra.Dual	1228	1223	-5 (-0.41%)
Mathlib.NumberTheory.Bernoulli	1231	1226	-5 (-0.41%)
Mathlib.RingTheory.Polynomial.Chebyshev	1070	1067	-3 (-0.28%)
Mathlib.RingTheory.Kaehler.JacobiZariski	1391	1388	-3 (-0.22%)
Mathlib.MeasureTheory.Integral.Marginal	1405	1402	-3 (-0.21%)
Mathlib.FieldTheory.Finite.GaloisField	1469	1466	-3 (-0.20%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno	1545	1542	-3 (-0.19%)
Mathlib.Analysis.Convex.Continuous	1672	1669	-3 (-0.18%)
Mathlib.NumberTheory.Modular	1682	1679	-3 (-0.18%)
Mathlib.RingTheory.Ideal.Norm.AbsNorm	1682	1679	-3 (-0.18%)
Mathlib.Topology.Category.Profinite.Nobeling	1701	1698	-3 (-0.18%)
Mathlib.MeasureTheory.Integral.FundThmCalculus	1989	1986	-3 (-0.15%)
Mathlib.Tactic	2448	2445	-3 (-0.12%)

Import changes for all files

Files	Import difference
There are 4937 files with changed transitive imports taking up over 209401 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ decidableLT'
+ instance (priority := low) nat (n : ℕ) : OfNat ONote n
+ instance (priority := low) {n : ℕ} : OfNat PosNum (n + 1)
+ repr_zero
- Lex
- ToLevel.imax
- ToLevel.max
- ToLevel.{u}
- countP_flatMap
- count_flatMap
- decidableLT
- fixIndType
- getElem_cons
- instance : ToLevel.{0}
- instance [ToLevel.{u}] : ToLevel.{u+1}
- instance {n : ℕ} : OfNat PosNum (n + 1)
- instance {α : Type u} [ToExpr α] [ToLevel.{u}] : ToExpr (Array α)
- length_flatMap
- lt_div_iff_mul_lt
- mkAppNTerm
- mkAuxFunction
- mkInstanceCmds
- mkLocalInstanceLetDecls
- mkMutualBlock
- mkToExprBody
- mkToExprHeader
- mkToExprInstanceCmds
- mkToExprInstanceHandler
- mkToLevelBinders
- mkToTypeExpr
- nat
- nil_le
- nil_lt_cons
- replicate_succ'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
199	1	adaptation notes

Current commit c100c8f24a
Reference commit 9837ca9d65

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Should this wait until we've sorted out the issues with the 4.15.0 release? I think there are some dependency version issues, and we can't easy move the 4.15.0 tag once master has moved on.

[kim-em]

Should this wait until we've sorted out the issues with the 4.15.0 release? I think there are some dependency version issues, and we can't easy move the 4.15.0 tag once master has moved on.

In fact, all the problems reported there are because we have not yet merged this PR. doc-gen4's main branch is already at v4.16.0-rc1, and so people are seeing lake update trying to advance the toolchain to v4.16.0-rc1, and then seeing everything break because Mathlib is not ready for it.

[kim-em]

bors merge

[mathlib-bors]

Build failed:

• Build

[kim-em]

bors p=10

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style