chore: bump mathlib to v4.27.0

[YaelDillies]

No description provided.

[eric-wieser]

Does this build at every intermediate commit? Note that currently nothing is green.

[YaelDillies]

lake build succeeded at v4.23, v4.26, v4.27. For v4.24, v4.25, I believe it succeeds as well but I haven't tried because I found the relevant fixes only after building to the version after (and subsequently hid the changes in the corresponding commits with a rebase). CI failing is due to the change in the String API, which I unfortunately don't know much about besides the fact that it is very disruptive...

Would you want lake build to succeed at each stage, or the whole CI? The latter promises to be annoying since the String API changed at least twice between v4.22 and v4.27.

[eric-wieser]

I suppose all that really matters is that lake build succeeds at every stage, and the whole CI succeeds at the final stage. Let's see what @mo271 thinks.

[mo271]

as @eric-wieser said, only lake build at every step (unless that would be an unreasonable amount of effort for some reason) and CI at the last step

[eric-wieser]

Why was this added?

[YaelDillies]

motzkin_polynomial_nonneg was moved to Counterexamples

[eric-wieser]

I'm not sure any care has been taken to make Counterexampless reasonable to import (besides the fact that doc-gen checks names don't clash with mathlib); I'd be more comfortable just sorrying out

formal-conjectures/FormalConjectures/HilbertProblems/17.lean

Lines 52 to 56 in f01550c

	theorem f_nonneg : ∀ x y : ℝ, 0 ≤ f.eval ![x, y] := by
	intro x y
	unfold f
	simp
	exact Real.motzkin_polynomial_nonneg x y

[eric-wieser]

(or inlining the short proof with a comment)

[Paul-Lez]

@YaelDillies what's the issue with the String API? (I suspect this might be showing up in code i wrote, so happy to look into this)

[YaelDillies]

I now locally have a sequence of bump commits that succeed on lake build over latest main, but Eric asked me privately to hold off pushing it.

@Paul-Lez, the issue with strings is that the substring API changed completely and most of the functions are now deprecated. Could you have a look at the CI failure and address it? Feel free to push to this branch, I can deal with the conflicts with my local version.

[Paul-Lez]

@YaelDillies Sounds good, will take a look!