From 555b3cdc4238068912593d11f2b5e7b7e6fd0a96 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sun, 1 Mar 2026 17:37:54 +1100
Subject: [PATCH] fix: mark `levelZero`, `levelOne`, and `Level.ofNat` as
 `implicit_reducible` (#12719)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR marks `levelZero` and `Level.ofNat` as `@[implicit_reducible]`
so that `Level.ofNat 0 =?= Level.zero` succeeds when the definitional
equality checker respects transparency annotations. Without this,
coercions between structures with implicit `Level` parameters fail, as
reported by @FLDutchmann on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/576131374).

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
(cherry picked from commit d59f229b74c69284663388c39bd7f17ca64b886a)
---
 src/Lean/Level.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 0ccdc0da1e8f..eeab601bbc03 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -129,7 +129,7 @@ def hasParam (u : Level) : Bool :=
 
 end Level
 
-@[expose] def levelZero :=
+@[expose, implicit_reducible] def levelZero :=
   Level.zero
 
 def mkLevelMVar (mvarId : LMVarId) :=
@@ -213,7 +213,7 @@ def isAlwaysZero : Level → Bool
   | max l₁ l₂    => isAlwaysZero l₁ && isAlwaysZero l₂
   | imax _  l₂   => isAlwaysZero l₂
 
-@[expose] def ofNat : Nat → Level
+@[expose, implicit_reducible] def ofNat : Nat → Level
   | 0   => levelZero
   | n+1 => mkLevelSucc (ofNat n)