feat: add backward.isDefEq.implicitBump option

This PR adds the `backward.isDefEq.implicitBump` option (default: `false`)
that controls whether all implicit arguments get their transparency bumped
to `TransparencyMode.instances` during `isDefEq`, not just instance-implicit
ones. When enabled, `[implicit_reducible]` definitions like `Nat.add` and
`Array.size` are unfolded when checking implicit arguments, closing the gap
between instance-implicit and regular implicit argument handling.

The default is `false` for staging purposes. After stage0 is updated, the
default will be flipped to `true`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/MetaTypes.lean

@@ -47,12 +47,13 @@ Each level unfolds everything the previous level does, plus more:
   (e.g., discrimination tree lookups in `simp`, type class resolution). Think of `[reducible]` as
   `[inline]` for type checking and indexing.
 
-- **`instances`**: Also unfolds `[instance_reducible]` definitions. Instance diamonds are common:
+- **`instances`**: Also unfolds `[implicit_reducible]` definitions. Instance diamonds are common:
   for example, `Add Nat` can come from a direct instance or via `Semiring`. These instances are all
   definitionally equal but structurally different, so `isDefEq` must unfold them to confirm equality.
-  However, instances must not be *eagerly* reduced (they become huge terms), and discrimination trees
-  do not index instances. This makes `.instances` safe for speculative checks involving instance
-  arguments without the performance cost of `.default`.
+  This level also handles definitions used in types that appear in implicit arguments (e.g.,
+  `Nat.add`, `Array.size`). However, these definitions must not be *eagerly* reduced (instances
+  become huge terms), and discrimination trees do not index them. This makes `.instances` safe for
+  speculative checks involving implicit arguments without the performance cost of `.default`.
 
 - **`default`**: Also unfolds `[semireducible]` definitions (anything not `[irreducible]`).
   Used for type checking user input where we want to try hard.
@@ -82,11 +83,11 @@ inductive TransparencyMode where
   `isDefEq` in proof automation (`simp`, `rw`, type class resolution) where most checks fail
   and we must not try too hard. -/
   | reducible
-  /-- Unfolds reducible constants and constants tagged with `@[instance_reducible]`.
-  Used for checking instance-implicit arguments during proof automation, and for unfolding
+  /-- Unfolds reducible constants and constants tagged with `@[implicit_reducible]`.
+  Used for checking implicit arguments during proof automation, and for unfolding
   class projections applied to instances. Instance diamonds (e.g., `Add Nat` from a direct instance
   vs from `Semiring`) are definitionally equal but structurally different, so `isDefEq` must unfold
-  them. -/
+  them. Also handles definitions used in types of implicit arguments (e.g., `Nat.add`, `Array.size`). -/
   | instances
   /-- Do not unfold anything. -/
   | none

src/Lean/Compiler/LCNF/Basic.lean

@@ -1019,7 +1019,7 @@ def Decl.isTemplateLike (decl : Decl pu) : CoreM Bool := do
   let env ← getEnv
   if ← hasLocalInst decl.type then
     return true -- `decl` applications will be specialized
-  else if (← isInstanceReducible decl.name) then
+  else if (← isImplicitReducible decl.name) then
     return true -- `decl` is "fuel" for code specialization
   else if decl.inlineable || hasSpecializeAttribute env decl.name then
     return true -- `decl` is going to be inlined or specialized

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -216,7 +216,7 @@ def eagerLambdaLifting : Pass where
   name       := `eagerLambdaLifting
   run        := fun decls => do
     decls.foldlM (init := #[]) fun decls decl => do
-      if decl.inlineable || (← isInstanceReducible decl.name) then
+      if decl.inlineable || (← isImplicitReducible decl.name) then
         return decls.push decl
       else
         return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (allowEtaContraction := false) (suffix := `_elam))

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -66,7 +66,7 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) :
       We assume that at the base phase these annotations are for the instance methods that have been lambda lifted.
       -/
       if (← inBasePhase) then
-        if (← isInstanceReducible decl.name) then
+        if (← isImplicitReducible decl.name) then
           unless decl.name == ``instDecidableEqBool do
             /-
             TODO: remove this hack after we refactor `Decidable` as suggested by Gabriel.

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -76,7 +76,7 @@ def etaPolyApp? (letDecl : LetDecl .pure) : OptionT SimpM (FunDecl .pure) := do
   let .const declName us args := letDecl.value | failure
   let some info := (← getEnv).find? declName | failure
   guard <| (← hasLocalInst info.type)
-  guard <| !(← isInstanceReducible declName)
+  guard <| !(← isImplicitReducible declName)
   let some ⟨.pure, decl⟩ ← getDecl? declName | failure
   guard <| decl.getArity > args.size
   let params ← mkNewParams letDecl.type

src/Lean/Compiler/LCNF/Specialize.lean

@@ -400,7 +400,7 @@ mutual
   partial def specializeApp? (e : LetValue .pure) : SpecializeM (Option (LetValue .pure)) := do
     let .const declName us args := e | return none
     if args.isEmpty then return none
-    if (← isInstanceReducible declName) then return none
+    if (← isImplicitReducible declName) then return none
     let some specEntry ← getSpecEntry? declName | return none
     unless (← shouldSpecialize specEntry args) do return none
     let some ⟨.pure, decl⟩ ← getDecl? declName | return none

src/Lean/Elab/DefView.lean

@@ -164,7 +164,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
-  -- NOTE: `[instance_reducible]` is added conditionally in `elabMutualDef`
+  -- NOTE: `[implicit_reducible]` is added conditionally in `elabMutualDef`
   let attrStx         ← `(attr| instance $(quote prio):num)
   let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
   let (binders, type) := expandDeclSig stx[4]

src/Lean/Elab/MutualDef.lean

@@ -1222,12 +1222,12 @@ where
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
 
-    -- Now that we have elaborated types, default data instances to `[instance_reducible]`. This
+    -- Now that we have elaborated types, default data instances to `[implicit_reducible]`. This
     -- should happen before attribute application as `[instance]` will check for it.
     for header in headers do
       if header.kind == .instance && !header.modifiers.anyAttr (·.name matches `reducible | `irreducible) then
         if !(← isProp header.type) then
-          setReducibilityStatus header.declName .instanceReducible
+          setReducibilityStatus header.declName .implicitReducible
 
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
       if Elab.async.get (← getOptions) && view.kind.isTheorem &&

src/Lean/Elab/Print.lean

@@ -28,7 +28,7 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   match (← getReducibilityStatus id) with
   | .irreducible =>   attrs := attrs.push m!"irreducible"
   | .reducible =>     attrs := attrs.push m!"reducible"
-  | .instanceReducible => attrs := attrs.push m!"instance_reducible"
+  | .implicitReducible => attrs := attrs.push m!"implicit_reducible"
   | .semireducible => pure ()
 
   let env ← getEnv

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -206,7 +206,7 @@ def elabGrindLocals (params : Grind.Params) : MetaM Grind.Params := do
     -- Filter similar to LibrarySuggestions.isDeniedPremise (but inlined to avoid dependency)
     -- Skip internal details, but allow private names (which are accessible from current module)
     if name.isInternalDetail && !isPrivateName name then continue
-    if (← isInstanceReducible name) then continue
+    if (← isImplicitReducible name) then continue
     match ci with
     | .defnInfo _ =>
       try

src/Lean/Elab/Tactic/Simp.lean

@@ -423,7 +423,7 @@ def elabSimpLocals (thms : SimpTheorems) (kind : SimpKind) : MetaM SimpTheorems
   for (name, ci) in env.constants.map₂.toList do
     -- Skip internal details, but allow private names (which are accessible from current module)
     if name.isInternalDetail && !isPrivateName name then continue
-    if (← isInstanceReducible name) then continue
+    if (← isImplicitReducible name) then continue
     match ci with
     | .defnInfo _ =>
       -- Definitions are added to unfold

src/Lean/LibrarySuggestions/Basic.lean

@@ -75,7 +75,7 @@ unsafe def fold {α : Type} (f : Name → α → MetaM α) (e : Expr) (acc : α)
         return acc
       else
         modify fun s => { s with visitedConsts := s.visitedConsts.insert c }
-        if ← isInstanceReducible c then
+        if ← isImplicitReducible c then
           return acc
         else
           f c acc
@@ -319,7 +319,7 @@ def isDeniedPremise (env : Environment) (name : Name) (allowPrivate : Bool := fa
   if name == ``sorryAx then return true
   -- Allow private names through if allowPrivate is set (e.g., for currentFile selector)
   if name.isInternalDetail && !(allowPrivate && isPrivateName name) then return true
-  if isInstanceReducibleCore env name then return true
+  if isImplicitReducibleCore env name then return true
   if Lean.Linter.isDeprecated env name then return true
   if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
   if let some moduleIdx := env.getModuleIdxFor? name then

src/Lean/Meta/ExprDefEq.lean

@@ -34,11 +34,13 @@ so that `isDefEq` would try harder and unfold semireducible definitions to make
 **Why `true` is now the default:** The transparency bump meant that every speculative `isDefEq` call
 in proof automation could trigger expensive unfolding of semireducible definitions on implicit
 arguments — and most of these calls *fail*. This eventually became a performance bottleneck in
-Mathlib. With `true`, implicit arguments are checked at the caller's transparency, except
-instance-implicit arguments (`[..]`) which are checked at `TransparencyMode.instances` (to resolve
-instance diamonds).
+Mathlib. With `true`, instance-implicit arguments (`[..]`) are checked at
+`TransparencyMode.instances` (to resolve instance diamonds). Other implicit arguments are checked
+at the caller's transparency unless `backward.isDefEq.implicitBump` is also `true`, in which case
+all implicit arguments are bumped to `.instances`.
 
-See `isDefEqArgs` for the implementation and `TransparencyMode` for the overall design.
+See `isDefEqArgs` for the implementation, `backward.isDefEq.implicitBump` for the implicit
+argument bump, and `TransparencyMode` for the overall design.
 -/
 register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   defValue := true
@@ -46,6 +48,27 @@ register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   when checking whether implicit arguments are definitionally equal"
 }
 
+/--
+Controls whether *all* implicit arguments (not just instance-implicit `[..]`) get their
+transparency bumped to `TransparencyMode.instances` during `isDefEq`.
+
+When `true`, all implicit arguments are checked at `.instances`, which unfolds
+`[implicit_reducible]` definitions (instances, `Nat.add`, `Array.size`, etc.). This is the
+intended behavior: users don't choose implicit arguments directly, so Lean should try harder
+to make them match. The `[implicit_reducible]` attribute provides guardrails — only explicitly
+marked definitions get unfolded, not arbitrary semireducible definitions.
+
+When `false` (current default for staging), only instance-implicit arguments (`[..]`) are bumped
+to `.instances`; other implicit arguments stay at the caller's transparency.
+
+This option only has an effect when `backward.isDefEq.respectTransparency` is `true`.
+-/
+register_builtin_option backward.isDefEq.implicitBump : Bool := {
+  defValue := false
+  descr    := "if true, bump transparency to `.instances` for all implicit arguments, \
+  not just instance-implicit ones"
+}
+
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -332,14 +355,17 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     unless (← Meta.isExprDefEqAux args₁[i]! args₂[i]!) do
       return false
   let respectTransparency := backward.isDefEq.respectTransparency.get (← getOptions)
+  let implicitBump := backward.isDefEq.implicitBump.get (← getOptions)
   for i in postponedImplicit do
     /- Second pass: unify implicit arguments.
        When `respectTransparency` is `false` (old behavior), we bump to `.default` so that
        semireducible definitions are unfolded — the rationale being that users don't think about
        implicit arguments and expect them to "just work."
-       When `respectTransparency` is `true` (new behavior), we respect the caller's transparency
-       for non-instance implicits, and use `.instances` for instance-implicit arguments to resolve
-       instance diamonds. See `backward.isDefEq.respectTransparency` for the motivation. -/
+       When `respectTransparency` is `true` and `implicitBump` is `true`, we bump all implicit
+       arguments to `.instances` so that `[implicit_reducible]` definitions are unfolded (instances,
+       `Nat.add`, `Array.size`, etc.) but not arbitrary semireducible definitions.
+       When `respectTransparency` is `true` and `implicitBump` is `false`, only instance-implicit
+       arguments (`[..]`) are bumped to `.instances`. -/
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!
@@ -352,8 +378,10 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     if info.binderInfo.isInstImplicit then
       discard <| trySynthPending a₁
       discard <| trySynthPending a₂
-    if respectTransparency && info.isInstImplicit then -- **TODO**: replace with `isInstance`
-      -- It is an instance, then we must allow at least instances to be unfolded.
+    if respectTransparency && (implicitBump || info.isInstImplicit) then
+      -- Bump to `.instances` so that `[implicit_reducible]` definitions (instances, `Nat.add`,
+      -- `Array.size`, etc.) are unfolded. The user doesn't choose implicit arguments directly,
+      -- so Lean should try harder than the caller's transparency to make them match.
       unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if respectTransparency then
       unless (← Meta.isExprDefEqAux a₁ a₂) do return false
@@ -363,13 +391,11 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
   for i in postponedHO do
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
-    let info := finfo.paramInfo[i]!
-    if info.isInstance then
-      if respectTransparency then
-        unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
-      else
-        -- Old behavior
-        unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+    if respectTransparency && (implicitBump || finfo.paramInfo[i]!.isInstance) then
+      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+    else if !respectTransparency && finfo.paramInfo[i]!.isInstance then
+      -- Old behavior
+      unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else
       unless (← Meta.isExprDefEqAux a₁ a₂) do return false
   return true

src/Lean/Meta/GetUnfoldableConst.lean

@@ -22,7 +22,7 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
     let status ← getReducibilityStatus info.name
     if status == .reducible then
       return true
-    else if m == .instances && status == .instanceReducible then
+    else if m == .instances && status == .implicitReducible then
       return true
     else
       return false

src/Lean/Meta/Instances.lean

@@ -233,10 +233,10 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
-  unless status matches .reducible | .instanceReducible do
+  unless status matches .reducible | .implicitReducible do
     let info ← getConstInfo declName
     if info.isDefinition then
-      logWarning m!"instance `{declName}` must be marked with `@[reducible]` or `@[instance_reducible]`"
+      logWarning m!"instance `{declName}` must be marked with `@[reducible]` or `@[implicit_reducible]`"
     else if wasOriginallyDefn (← getEnv) declName then
       logWarning m!"instance `{declName}` must be marked with `@[expose]`"
   let projInfo? ← getProjectionFnInfo? declName
@@ -244,7 +244,7 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 /-
-Adds instance **and** marks it with reducibility status `@[instance_reducible]`. We use this function
+Adds instance **and** marks it with reducibility status `@[implicit_reducible]`. We use this function
 to elaborate `instance` command.
 
 **Note**: We used to check whether `declName` had `instance` reducibility by using `isInstance declName`.
@@ -266,7 +266,7 @@ not its transparency status.
 Thus, we added a new transparency setting and set it here.
 -/
 def registerInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
-  setReducibilityStatus declName .instanceReducible
+  setReducibilityStatus declName .implicitReducible
   addInstance declName attrKind prio
 
 /--

src/Lean/Meta/SynthInstance.lean

@@ -897,7 +897,7 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
           /-
           **Note**: The expensive `preprocessOutParam` step is morally **not** needed here because
           the output params should be uniquely determined by the input params. During type class
-          resolution, definitional equality only unfolds `[reducible]` and `[instance_reducible]`
+          resolution, definitional equality only unfolds `[reducible]` and `[implicit_reducible]`
           declarations. This is a contract with our users to ensure performance is reasonable.
           However, the same `OrderDual` declaration that creates problems for `assignOutParams`
           also prevents us from using this optimization. As an example, suppose we are trying to

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -443,7 +443,7 @@ Returns `true` if we should use `funCC` for applications of the given constant s
 private def useFunCongrAtDecl (declName : Name) : GrindM Bool := do
   if (← hasFunCCModifier declName) then
     return true
-  if (← isInstanceReducible declName) then
+  if (← isImplicitReducible declName) then
     /- **Note**: Instances are support elements. No `funCC` -/
     return false
   if let some projInfo ← getProjectionFnInfo? declName then

src/Lean/Meta/Tactic/Grind/MBTC.lean

@@ -85,7 +85,7 @@ private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do
 /-- Returns `true` if `f` is a type class instance -/
 private def isFnInstance (f : Expr) : CoreM Bool := do
   let .const declName _ := f | return false
-  isInstanceReducible declName
+  isImplicitReducible declName
 
 /-- Model-based theory combination. -/
 def mbtc (ctx : MBTC.Context) : GoalM Bool := do

src/Lean/Meta/WHNF.lean

@@ -491,7 +491,7 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   | .default => return !(← isIrreducible info.name)
   | _ =>
     let status ← getReducibilityStatus info.name
-    if status matches .reducible | .instanceReducible then
+    if status matches .reducible | .implicitReducible then
       return true
     else if hasMatchPatternAttribute (← getEnv) info.name then
       return true
@@ -814,10 +814,10 @@ When `true`, unfolding a `[reducible]` class field at `TransparencyMode.reducibl
 the associated instance projection at `TransparencyMode.instances`.
 
 **Motivation:** Consider `a ≤ b` where `a b : Nat` and `LE.le` is `[reducible]`. Unfolding `LE.le`
-gives `instLENat.1 a b`, which is stuck because `instLENat` is `[instance_reducible]` (not
+gives `instLENat.1 a b`, which is stuck because `instLENat` is `[implicit_reducible]` (not
 `[reducible]`). Similarly, `stM m (ExceptT ε m) α` unfolds to an instance projection that is stuck
 at `.reducible`. Without this option, marking a class field as `[reducible]` is pointless when the
-instance providing it is only `[instance_reducible]`. This option makes the `[reducible]` annotation
+instance providing it is only `[implicit_reducible]`. This option makes the `[reducible]` annotation
 on class fields work as the user expects by temporarily bumping to `.instances` for the projection.
 
 See `unfoldDefault` for the implementation.
@@ -833,7 +833,7 @@ This function has special support for unfolding class fields.
 The support is particularly important when the user marks a class field as `[reducible]` and
 the transparency mode is `.reducible`. For example, suppose `e` is `a ≤ b` where `a b : Nat`,
 and `LE.le` is marked as `[reducible]`. Simply unfolding `LE.le` would give `instLENat.1 a b`,
-which would be stuck because `instLENat` has transparency `[instance_reducible]`. To avoid this, when we unfold
+which would be stuck because `instLENat` has transparency `[implicit_reducible]`. To avoid this, when we unfold
 a `[reducible]` class field, we also unfold the associated projection `instLENat.1` using
 `.instances` reducibility, ultimately returning `Nat.le a b`.
 -/

src/Lean/ReducibilityAttrs.lean

@@ -17,9 +17,13 @@ See `TransparencyMode` for the full design rationale.
   appear in user-facing terms, but are eagerly unfolded when indexing terms into discrimination
   trees (`simp`, type class resolution) and in `grind`. Think of it as `[inline]` for indexing.
   Suitable for abbreviations and definitions that should be transparent to proof automation.
-- **`instanceReducible`**: Unfolded at `TransparencyMode.instances` or above. Used for type class
-  instances. Instances cannot be eagerly reduced (they expand into large terms), but must be
-  unfoldable to resolve instance diamonds (e.g., `Add Nat` via direct instance vs via `Semiring`).
+- **`implicitReducible`**: Unfolded at `TransparencyMode.instances` or above. Used for type class
+  instances and definitions that appear in types matched during implicit argument resolution
+  (e.g., `Nat.add`, `Array.size`). These definitions cannot be eagerly reduced (instances expand
+  into large terms, recursive definitions are problematic), but must be unfoldable when checking
+  implicit arguments and resolving instance diamonds (e.g., `Add Nat` via direct instance vs via
+  `Semiring`). The attribute `[implicit_reducible]` (or its alias `[instance_reducible]`) marks
+  a definition with this status.
 - **`semireducible`**: The default. Unfolded at `TransparencyMode.default` or above. Used for
   ordinary definitions. Suitable for user-written code where `isDefEq` should try hard during
   type checking, but not during speculative proof automation.
@@ -27,14 +31,14 @@ See `TransparencyMode` for the full design rationale.
   hidden from `isDefEq` in normal usage.
 -/
 inductive ReducibilityStatus where
-  | reducible | semireducible | irreducible | instanceReducible
+  | reducible | semireducible | irreducible | implicitReducible
   deriving Inhabited, Repr, BEq
 
 def ReducibilityStatus.toAttrString : ReducibilityStatus → String
   | .reducible => "[reducible]"
   | .irreducible => "[irreducible]"
   | .semireducible => "[semireducible]"
-  | .instanceReducible => "[instance_reducible]"
+  | .implicitReducible => "[implicit_reducible]"
 
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {
@@ -137,11 +141,11 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
         unless statusOld matches .semireducible do
           throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
       | .irreducible =>
-        unless statusOld matches .semireducible | .instanceReducible do
-          throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]` nor `[instance_reducible]`, but `{statusOld.toAttrString}`{suffix}"
-      | .instanceReducible =>
+        unless statusOld matches .semireducible | .implicitReducible do
+          throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]` nor `[implicit_reducible]`, but `{statusOld.toAttrString}`{suffix}"
+      | .implicitReducible =>
         unless statusOld matches .semireducible do
-          throwError "failed to set `[instance_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+          throwError "failed to set `[implicit_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
       | .semireducible =>
         throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}"
     | .local =>
@@ -149,11 +153,11 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
       | .reducible =>
         throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
       | .irreducible =>
-        unless statusOld matches .semireducible | .instanceReducible do
-          throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` nor `[instance_reducible]` expected{suffix}"
-      | .instanceReducible =>
+        unless statusOld matches .semireducible | .implicitReducible do
+          throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` nor `[implicit_reducible]` expected{suffix}"
+      | .implicitReducible =>
         unless statusOld matches .semireducible do
-          throwError "failed to set `[local instance_reducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
+          throwError "failed to set `[local implicit_reducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
       | .semireducible =>
         unless statusOld matches .irreducible do
           throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
@@ -192,23 +196,36 @@ builtin_initialize
  }
 
 /--
-Marks a definition as `[instance_reducible]`, meaning it is unfolded at
+Marks a definition as `[implicit_reducible]`, meaning it is unfolded at
 `TransparencyMode.instances` or above but *not* at `TransparencyMode.reducible`.
 
-This attribute decouples whether a definition participates in type class resolution
-(the `[instance]` attribute) from its transparency. The `instance` command automatically
-adds both `[instance]` and `[instance_reducible]`.
+Use this attribute for:
+- **Type class instances**: The `instance` command automatically adds `[implicit_reducible]`.
+  Instance diamonds (e.g., `Add Nat` from a direct instance vs via `Semiring`) are definitionally
+  equal but structurally different, so `isDefEq` must unfold them. When using `attribute [instance]`
+  on an existing definition, you typically also need `attribute [implicit_reducible]`.
+- **Definitions used in types that appear in implicit arguments**: For example, `Nat.add`, `Array.size`.
+  When proof automation applies a lemma, implicit arguments are checked with increased transparency
+  so that type-level computations (e.g., `n + 0` vs `n`) are resolved.
 
-When using `attribute [instance]` on an existing definition, you typically also need
-`attribute [instance_reducible]` so that `isDefEq` can unfold the definition when resolving
-instance diamonds.
+`[instance_reducible]` is an alias for this attribute.
 -/
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `implicit_reducible
+    descr           := "implicit reducible declaration"
+    add             := addAttr .implicitReducible
+    applicationTime := .afterTypeChecking
+ }
+
+/-- Alias for `[implicit_reducible]`. See `implicit_reducible` for documentation. -/
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
     name            := `instance_reducible
-    descr           := "instance reducible declaration"
-    add             := addAttr .instanceReducible
+    descr           := "alias for implicit_reducible"
+    add             := addAttr .implicitReducible
     applicationTime := .afterTypeChecking
  }
 
@@ -232,12 +249,15 @@ def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   return (← getReducibilityStatus declName) matches .irreducible
 
-def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool :=
-  getReducibilityStatusCore env declName matches .instanceReducible
+def isImplicitReducibleCore (env : Environment) (declName : Name) : Bool :=
+  getReducibilityStatusCore env declName matches .implicitReducible
 
-/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/
-def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
-  return isInstanceReducibleCore (← getEnv) declName
+/-- Return `true` if the given declaration has been marked as `[implicit_reducible]`. -/
+def isImplicitReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
+  return isImplicitReducibleCore (← getEnv) declName
+
+@[deprecated isImplicitReducibleCore (since := "2026-02-18")] abbrev isInstanceReducibleCore := isImplicitReducibleCore
+@[deprecated isImplicitReducible (since := "2026-02-18")] abbrev isInstanceReducible := @isImplicitReducible
 
 /-- Set the given declaration as `[irreducible]` -/
 def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/defInst.lean.expected.out

@@ -10,5 +10,5 @@ fun x y => x == y : Foo → Foo → Bool
 false
 true
 true
-@[instance_reducible] def instMonadM : Monad M :=
+@[implicit_reducible] def instMonadM : Monad M :=
 ReaderT.instMonad

tests/lean/diamond4.lean.expected.out

@@ -1,4 +1,4 @@
-@[instance_reducible] def D.toB : {α : Type} → [self : D α] → B α :=
+@[implicit_reducible] def D.toB : {α : Type} → [self : D α] → B α :=
 fun (α : Type) [self : D α] => self.1
-@[instance_reducible] def D.toC : {α : Type} → [self : D α] → C α :=
+@[implicit_reducible] def D.toC : {α : Type} → [self : D α] → C α :=
 fun (α : Type) (self : D α) => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self)

tests/lean/diamond6.lean.expected.out

@@ -16,7 +16,7 @@ FooAC.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α]
       @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
         (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) :
   FooAC α
-@[instance_reducible] def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
+@[implicit_reducible] def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
 fun (α : Type) (self : FooAC α) =>
   @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self)
     (@FooAC.mul_assoc α self)
@@ -39,7 +39,7 @@ FooAC'.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α]
       @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
         (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) :
   FooAC' α
-@[instance_reducible] def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
+@[implicit_reducible] def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
 fun (α : Type) (self : FooAC' α) =>
   @FooAssoc'.mk α
     (@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self)

tests/lean/diamond7.lean.expected.out

@@ -6,7 +6,7 @@ CommMonoid.mk.{u} {α : Type u} [toMonoid : Monoid.{u} α]
         (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α toMonoid))) b
           a)) :
   CommMonoid.{u} α
-@[instance_reducible] def CommMonoid.toCommSemigroup.{u} : {α : Type u} →
+@[implicit_reducible] def CommMonoid.toCommSemigroup.{u} : {α : Type u} →
   [self : CommMonoid.{u} α] → CommSemigroup.{u} α :=
 fun (α : Type u) (self : CommMonoid.{u} α) =>
   @CommSemigroup.mk.{u} α (@Monoid.toSemigroup.{u} α (@CommMonoid.toMonoid.{u} α self))
@@ -20,12 +20,12 @@ CommGroup.mk.{u} {α : Type u} [toGroup : Group.{u} α]
         (@HMul.hMul.{u, u, u} α α α
           (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α (@Group.toMonoid.{u} α toGroup)))) b a)) :
   CommGroup.{u} α
-@[instance_reducible] def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
+@[implicit_reducible] def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
 fun (α : Type u) (self : CommGroup.{u} α) =>
   @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self)
 Field.mk.{u} {α : Type u} [toDivisionRing : DivisionRing α] (mul_comm : ∀ (a b : α), a * b = b * a) : Field α
-@[instance_reducible] def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
+@[implicit_reducible] def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
 fun (α : Type u) [self : Field.{u} α] => self.1
-@[instance_reducible] def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
+@[implicit_reducible] def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
 fun (α : Type u) (self : Field.{u} α) =>
   @CommRing.mk.{u} α (@DivisionRing.toRing.{u} α (@Field.toDivisionRing.{u} α self)) (@Field.mul_comm.{u} α self)

tests/lean/run/derivingBEq.lean

@@ -54,7 +54,7 @@ inductive L' (α : Type u) : Type u
 
 end InNamespace
 /--
-info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+info: @[implicit_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
 -/
 #guard_msgs in #print sig InNamespace.instBEqL'
 /--
@@ -163,7 +163,7 @@ private structure PrivStruct where
 deriving BEq
 
 -- Instance and spec should be private
-/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
+/-- info: @[implicit_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
 #guard_msgs in
 #print sig instBEqPrivStruct
 

tests/lean/run/derivingBEqLinear.lean

@@ -58,7 +58,7 @@ inductive L' (α : Type u) : Type u
 
 end InNamespace
 /--
-info: @[instance_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
+info: @[implicit_reducible, expose] def InNamespace.instBEqL'.{u_1} : {α : Type u_1} → [BEq α] → BEq (InNamespace.L' α)
 -/
 #guard_msgs in #print sig InNamespace.instBEqL'
 /--
@@ -150,7 +150,7 @@ private structure PrivStruct where
 deriving BEq
 
 -- Instance and spec should be private
-/-- info: @[instance_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
+/-- info: @[implicit_reducible] private def instBEqPrivStruct : BEq PrivStruct -/
 #guard_msgs in
 #print sig instBEqPrivStruct
 

tests/lean/run/derivingDelta.lean

@@ -62,7 +62,7 @@ def MyNat := Nat
 deriving OfNat
 
 /--
-info: @[instance_reducible] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
+info: @[implicit_reducible] def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
 fun _x_1 => instOfNatNat _x_1
 -/
 #guard_msgs in #print instOfNatMyNat
@@ -72,7 +72,7 @@ Explicit parameterization
 -/
 deriving instance (n : Nat) → OfNat _ n for MyNat
 /--
-info: @[instance_reducible] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
+info: @[implicit_reducible] def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
 fun n => instOfNatNat n
 -/
 #guard_msgs in #print instOfNatMyNat_1
@@ -85,7 +85,7 @@ variable (m : Nat)
 deriving instance OfNat _ m for MyNat
 end
 /--
-info: @[instance_reducible] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
+info: @[implicit_reducible] def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
 fun m => instOfNatNat m
 -/
 #guard_msgs in #print instOfNatMyNat_2
@@ -132,7 +132,7 @@ def MyFin'' := Fin
 deriving C1
 
 /--
-info: @[instance_reducible] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
+info: @[implicit_reducible] def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
 instC1NatFin
 -/
 #guard_msgs in set_option pp.explicit true in #print instC1NatMyFin''
@@ -164,12 +164,12 @@ instance (n : Nat) : OfNat' n Int := {}
 def MyInt := Int
 deriving OfNat', OfNat
 /--
-info: @[instance_reducible] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
+info: @[implicit_reducible] def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
 fun _x_1 => instOfNat'Int _x_1
 -/
 #guard_msgs in #print instOfNat'MyInt
 /--
-info: @[instance_reducible] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
+info: @[implicit_reducible] def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
 fun _x_1 => instOfNat
 -/
 #guard_msgs in #print instOfNatMyInt
@@ -201,7 +201,7 @@ def NewRing (R : Type _) [Semiring R] := R
 deriving Module R
 
 /--
-info: @[instance_reducible] def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
+info: @[implicit_reducible] def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
 fun R [Semiring R] => instModule R
 -/
 #guard_msgs in #print instModuleNewRing
@@ -221,7 +221,7 @@ def NewRing' (R : Type _) := R
 deriving instance Module R for NewRing' R
 
 /--
-info: @[instance_reducible] def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
+info: @[implicit_reducible] def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
 fun R [Semiring R] => instModule R
 -/
 #guard_msgs in #print instModuleNewRing'
@@ -236,7 +236,7 @@ instance : C2 Type Prop := {}
 def Prop' := Prop
 deriving C2
 /--
-info: @[instance_reducible] def instC2TypeProp' : C2 Type Prop' :=
+info: @[implicit_reducible] def instC2TypeProp' : C2 Type Prop' :=
 instC2TypeProp
 -/
 #guard_msgs in #print instC2TypeProp'

tests/lean/run/derivingInhabited.lean

@@ -54,7 +54,7 @@ structure A where
 deriving Inhabited
 
 /--
-info: @[instance_reducible] private def instInhabitedA : Inhabited A :=
+info: @[implicit_reducible] private def instInhabitedA : Inhabited A :=
 { default := instInhabitedA.default }
 -/
 #guard_msgs in

tests/lean/run/derivingRepr.lean

@@ -146,7 +146,7 @@ public structure Public where
 deriving Repr
 
 /--
-info: @[instance_reducible, expose] def instReprPublic : Repr Public :=
+info: @[implicit_reducible, expose] def instReprPublic : Repr Public :=
 { reprPrec := instReprPublic.repr }
 -/
 #guard_msgs in

tests/lean/run/deriving_diamond_defeq.lean

@@ -81,7 +81,7 @@ set_option pp.all true in
 #check @instMyHigherMyAlias
 
 /--
-info: @[instance_reducible] def instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
+info: @[implicit_reducible] def instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
 instHigherNat
 -/
 #guard_msgs in

tests/lean/run/instanceReducibility.lean

@@ -5,7 +5,7 @@ module
 instance i1 : Inhabited Nat := inferInstance
 
 /--
-info: @[instance_reducible] private def i1 : Inhabited Nat :=
+info: @[implicit_reducible] private def i1 : Inhabited Nat :=
 inferInstance
 -/
 #guard_msgs in
@@ -21,7 +21,7 @@ inferInstance
 #print i2
 
 /--
-warning: instance `_private.lean.run.instanceReducibility.0.i3` must be marked with `@[reducible]` or `@[instance_reducible]`
+warning: instance `_private.lean.run.instanceReducibility.0.i3` must be marked with `@[reducible]` or `@[implicit_reducible]`
 -/
 #guard_msgs in
 @[irreducible] instance i3 : Inhabited Nat := inferInstance

tests/lean/run/instanceReducible.lean

@@ -8,18 +8,18 @@ public def unexposed : Inhabited Nat := inferInstance
 #guard_msgs in
 attribute [instance] unexposed
 
-/-- warning: instance `unexposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+/-- warning: instance `unexposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
 #guard_msgs in
 attribute [local instance] unexposed
 
 @[expose]
 public def exposed : Inhabited Nat := inferInstance
 
-/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
 #guard_msgs in
 attribute [instance] exposed
 
-/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
 #guard_msgs in
 attribute [local instance] exposed
 

tests/lean/run/issue10678.lean

@@ -9,7 +9,7 @@ deriving Lean.ToExpr, Inhabited
 -- same namespace for instance and aux decls
 
 /--
-info: @[instance_reducible] def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) :=
+info: @[implicit_reducible] def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprA.toExpr inst_1, toTypeExpr := (Lean.Expr.const `A.A [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
@@ -17,7 +17,7 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
 
 
 /--
-info: @[instance_reducible] def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) :=
+info: @[implicit_reducible] def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) :=
 fun {a} [Inhabited a] => { default := instInhabitedA.default }
 -/
 #guard_msgs in #print A.instInhabitedA
@@ -35,14 +35,14 @@ deriving Lean.ToExpr, Inhabited
 end
 
 /--
-info: @[instance_reducible] def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) :=
+info: @[implicit_reducible] def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprB.toExpr_1 inst_1, toTypeExpr := (Lean.Expr.const `B [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
 #guard_msgs in
 #print instToExprB
 /--
-info: @[instance_reducible] def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) :=
+info: @[implicit_reducible] def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) :=
 fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
   { toExpr := instToExprB.toExpr_2 inst_1, toTypeExpr := (Lean.Expr.const `C [Lean.toLevel]).app (Lean.toTypeExpr α) }
 -/
@@ -51,14 +51,14 @@ fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
 
 
 /--
-info: @[instance_reducible] def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) :=
+info: @[implicit_reducible] def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) :=
 fun {a} => { default := instInhabitedB.default_1 }
 -/
 #guard_msgs in
 #print instInhabitedB
 
 /--
-info: @[instance_reducible] def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) :=
+info: @[implicit_reducible] def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) :=
 fun {a} => { default := instInhabitedC.default_1 }
 -/
 #guard_msgs in

tests/lean/run/reduceBEqSimproc.lean

@@ -54,7 +54,7 @@ end Linear
 namespace A
 inductive L where | nil  : L | cons : Nat → L → L deriving BEq
 -- NB: Instance, op and theorem are private
-/-- info: @[instance_reducible] private def A.instBEqL : BEq L -/
+/-- info: @[implicit_reducible] private def A.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: private def A.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq
@@ -66,7 +66,7 @@ end A
 namespace B
 public inductive L where | nil  : L | cons : Nat → L → L deriving BEq
 -- NB: Instance is public and exposed, op and theorem are private
-/-- info: @[instance_reducible, expose] def B.instBEqL : BEq L -/
+/-- info: @[implicit_reducible, expose] def B.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: def B.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq
@@ -79,7 +79,7 @@ end B
 namespace C
 public inductive L where | nil  : L | cons : Nat → L → L deriving @[expose] BEq
 -- NB: Public exposed instances, implementation and public theorem
-/-- info: @[instance_reducible, expose] def C.instBEqL : BEq L -/
+/-- info: @[implicit_reducible, expose] def C.instBEqL : BEq L -/
 #guard_msgs in #print sig instBEqL
 /-- info: @[expose] def C.instBEqL.beq : L → L → Bool -/
 #guard_msgs in #print sig instBEqL.beq

tests/lean/run/reducibilityAttrValidation.lean

@@ -25,7 +25,7 @@ attribute [semireducible] f
 attribute [irreducible] f
 
 /--
-error: failed to set `[irreducible]`, `f` is not currently `[semireducible]` nor `[instance_reducible]`, but `[irreducible]`
+error: failed to set `[irreducible]`, `f` is not currently `[semireducible]` nor `[implicit_reducible]`, but `[irreducible]`
 
 Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
@@ -45,7 +45,7 @@ attribute [local semireducible] f
 attribute [local irreducible] f
 
 /--
-error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` nor `[instance_reducible]` expected
+error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` nor `[implicit_reducible]` expected
 
 Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/

tests/lean/run/structInst.lean

@@ -274,7 +274,7 @@ instance : B where
 instance : C where
 
 /--
-info: @[instance_reducible] def Issue6046.instC : C :=
+info: @[implicit_reducible] def Issue6046.instC : C :=
 { b := B.b }
 -/
 #guard_msgs in #print Issue6046.instC
@@ -342,7 +342,7 @@ class Bar extends Foo where
 instance instBar : Bar where
 
 /--
-info: @[instance_reducible] def Ex6769_1.instBar : Bar :=
+info: @[implicit_reducible] def Ex6769_1.instBar : Bar :=
 { x := 0 }
 -/
 #guard_msgs in #print instBar
@@ -361,7 +361,7 @@ instance instBar : Bar where
   x := 0
 
 /--
-info: @[instance_reducible] def Ex6769_2.instBar : Bar :=
+info: @[implicit_reducible] def Ex6769_2.instBar : Bar :=
 { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 }
 -/
 #guard_msgs in #print instBar
@@ -380,7 +380,7 @@ instance instBar : Bar where
   x := 0
 
 /--
-info: @[instance_reducible] def Ex6769_3.instBar : Bar :=
+info: @[implicit_reducible] def Ex6769_3.instBar : Bar :=
 { x := 0, hx := Mathlib12129.bar._proof_1, hx' := Mathlib12129.bar._proof_1 }
 -/
 #guard_msgs in #print instBar

tests/pkg/module/Module/Basic.lean

@@ -423,7 +423,7 @@ meta structure Foo where
 deriving TypeName
 
 /--
-info: @[instance_reducible] private meta def instTypeNameFoo : TypeName Foo :=
+info: @[implicit_reducible] private meta def instTypeNameFoo : TypeName Foo :=
 inst✝
 -/
 #guard_msgs in