[#15198] test: lean4Lean's Level.isEquiv

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#15198.

[downstream-lean4]

Build report for downstream: follow upstream PR

Stayed red

Repo	Critical	Build	Test	Lint
repl		🟥 in 1s	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 17s	✅ in 4s	⏭️
batteries	✅	✅ in 12s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 3s	✅ in 0s	⏭️
mathlib4	✅	✅ in 1029s	✅ in 331s	✅ in 97s
plausible	✅	✅ in 3s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 5s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 76s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
cslib		✅ in 33s	✅ in 9s	✅ in 3s
doc-gen4		✅ in 16s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 4s	⏭️	⏭️
lean4export		✅ in 3s	✅ in 8s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 9s	✅ in 20s	⏭️
nerodia		✅ in 5s	✅ in 21s	⏭️
verso		✅ in 126s	✅ in 176s	⏭️
verso-slides		✅ in 21s	✅ in 9s	⏭️
verso-web-components		✅ in 8s	⏭️	⏭️

View run

[arthur-adjedj]

!bench mathlib

[leanprover-radar]

Benchmark results for 3656e4b against 2a539a5 are in. There are significant results. @arthur-adjedj

• 🟥 build//instructions: +157.9G (+0.11%)

Large changes (1🟥)

• 🟥 build/module/Mathlib.CategoryTheory.Triangulated.Triangulated//instructions: +7.5G (+30.66%)

Small changes (1✅, 7🟥)

• 🟥 build/module/Mathlib.CategoryTheory.Functor.CurryingThree//instructions: +468.4M (+1.64%)
• 🟥 build/module/Mathlib.CategoryTheory.Limits.Preserves.Bifunctor//instructions: +312.4M (+1.25%)
• 🟥 build/module/Mathlib.CategoryTheory.Whiskering//instructions: +825.8M (+2.16%)
• ✅ build/module/Mathlib.Combinatorics.SimpleGraph.Walks.Basic//instructions: -59.1M (-2.04%)
• 🟥 build/module/Mathlib.Data.Rat.Cast.OfScientific//instructions: +100.7M (+2.77%)
• 🟥 build/module/Mathlib.FieldTheory.PurelyInseparable.Tower//instructions: +372.4M (+1.30%)
• 🟥 build/module/Mathlib.RingTheory.Unramified.Dedekind//instructions: +89.3M (+1.35%)
• and 1 hidden