[#15210] test: robin's Level.isEquiv

[downstream-lean4]

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

[arthur-adjedj]

!bench mathlib

[leanprover-radar]

Benchmark results for 00e5f72 against 09c06ff are in. No significant results found. @arthur-adjedj

• 🟥 build//instructions: +66.2G (+0.05%)

Small changes (3✅, 10🟥)

• 🟥 build/module/Aesop.RuleTac//instructions: +17.9M (+1.38%)
• 🟥 build/module/Batteries.Tactic.Lint.TypeClass//instructions: +76.8M (+4.31%)
• ✅ build/module/Batteries.Tactic.NoMatch//instructions: -23.2M (-0.89%)
• 🟥 build/module/Mathlib.Analysis.Polynomial.Factorization//instructions: +141.4M (+2.09%)
• ✅ build/module/Mathlib.CategoryTheory.Whiskering//instructions: -363.3M (-0.95%)
• ✅ build/module/Mathlib.Combinatorics.SimpleGraph.Walks.Basic//instructions: -61.7M (-2.13%)
• 🟥 build/module/Mathlib.MeasureTheory.Measure.CharacteristicFunction//instructions: +77.7M (+1.70%)
• 🟥 build/module/Mathlib.NumberTheory.LSeries.Deriv//instructions: +338.8M (+3.71%)
• 🟥 build/module/Mathlib.NumberTheory.LSeries.HurwitzZeta//instructions: +566.0M (+5.09%)
• 🟥 build/module/Mathlib.NumberTheory.NumberField.InfinitePlace.Completion//instructions: +112.8M (+2.31%)
• 🟥 build/module/Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def//instructions: +94.3M (+1.77%)
• 🟥 build/module/Mathlib.Probability.Independence.Process.HasIndepIncrements//instructions: +88.6M (+2.26%)
• 🟥 build/module/Mathlib//instructions: +204.4M (+2.06%)

[arthur-adjedj]

!bench mathlib

[leanprover-radar]

Benchmark results for dd36d52 against 8f083ee are in. No significant results found. @arthur-adjedj

• 🟥 build//instructions: +91.8G (+0.06%)

Small changes (4✅, 8🟥)

• 🟥 build/module/Batteries.Tactic.Lint.TypeClass//instructions: +80.5M (+4.53%)
• ✅ build/module/Mathlib.CategoryTheory.Whiskering//instructions: -373.7M (-0.98%)
• 🟥 build/module/Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring//instructions: +58.0M (+1.92%)
• ✅ build/module/Mathlib.Data.Finsupp.BigOperators//instructions: -145.8M (-2.55%)
• ✅ build/module/Mathlib.Data.Rat.Cast.OfScientific//instructions: -62.2M (-1.67%)
• 🟥 build/module/Mathlib.Data.Set.Lattice//instructions: +57.7M (+2.52%)
• 🟥 build/module/Mathlib.LinearAlgebra.LeftExact//instructions: +116.8M (+2.68%)
• ✅ build/module/Mathlib.NumberTheory.LSeries.HurwitzZeta//instructions: -480.7M (-4.13%)
• 🟥 build/module/Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def//instructions: +95.9M (+1.79%)
• 🟥 build/module/Mathlib.RingTheory.Noetherian.Nilpotent//instructions: +146.7M (+3.52%)
• 🟥 build/module/Mathlib.Topology.Algebra.MetricSpace.Lipschitz//instructions: +332.2M (+4.15%)
• 🟥 build/module/Mathlib.Topology.Order.OrderClosedExtr//instructions: +78.6M (+2.24%)

[downstream-lean4]

Build report for downstream: follow upstream PR

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 1028s	✅ in 334s	✅ in 99s
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 8s	✅ 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	⏭️
repl		✅ in 4s	✅ in 61s	⏭️
verso		✅ in 128s	✅ in 172s	⏭️
verso-slides		✅ in 21s	✅ in 9s	⏭️
verso-web-components		✅ in 8s	⏭️	⏭️

View run