feat: enable implicit argument transparency bump (part 2) (#12572)

This PR is part 2 of the `implicit_reducible` refactoring (part 1:
#12567).

**Background.** When Lean checks definitional equality of function
applications
`f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a
transparency level determined by the binder type. Previously, only
instance-implicit (`[C]`) arguments received a transparency bump to
`.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit
arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that
definitions marked `[implicit_reducible]` unfold when comparing implicit
arguments. This is important because implicit arguments often carry type
information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in
non-proof positions (Sort arguments to `cast`) — proof irrelevance does
not
help here, so the relevant definitions must actually unfold.

**`[implicit_reducible]`** (renamed from `[instance_reducible]` in part
1) marks
definitions that should unfold at `TransparencyMode.instances` — between
`[reducible]` (unfolds at `.reducible` and above) and the default
`[semireducible]` (unfolds only at `.default` and above). This is the
right
level for core arithmetic operations that appear in type indices.

## Changes

- **Enable `backward.isDefEq.implicitBump` by default** and set it in
  `stage0/src/stdlib_flags.h` so stage0 also compiles with it
- **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as
`[implicit_reducible]`**
so they unfold when comparing implicit arguments at `.instances`
transparency
- **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`,
  `n * 0 =?= 0`) that are now handled by `[implicit_reducible]`
- **Rename all remaining `[instance_reducible]` attribute usages** to
`[implicit_reducible]` across the codebase (the old name remains as an
alias)
- **Remove 28 `set_option backward.isDefEq.respectTransparency false
in`**
  workarounds that are no longer needed

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Classical.lean

@@ -142,7 +142,7 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
-@[instance_reducible]
+@[implicit_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control/Lawful/Instances.lean

@@ -258,7 +258,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
   rw [← bind_pure_comp]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) :
     OptionT.run (controlAt m f) = f fun x => x.run := by
   simp [controlAt, Option.elimM, Option.elim]
@@ -346,10 +345,9 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
     ReaderT.run (liftWith f) ctx = (f fun x => x.run ctx) :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (controlAt m f) ctx = f fun x => x.run ctx := by
-  simp [controlAt]
+  simp [controlAt]; exact bind_pure _
 
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (control f) ctx = f fun x => x.run ctx := run_controlAt f ctx
@@ -447,7 +445,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by
   simp [liftWith, MonadControl.liftWith, Function.comp_def]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) :
     StateT.run (controlAt m f) s = f fun x => x.run s := by
   simp [controlAt]

src/Init/Control/MonadAttach.lean

@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Data/Array/Basic.lean

@@ -93,7 +93,7 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp only [getElem?_def, getElem_toList]
-  simp only [Array.size]; rfl
+  simp only [Array.size]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma

src/Init/Data/Array/Find.lean

@@ -723,7 +723,6 @@ theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array
     xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
   cases xs
   simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
-  rfl
 
 theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
     xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by

src/Init/Data/Array/Lemmas.lean

@@ -896,7 +896,7 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]; rfl
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
 @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
     (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
@@ -2855,7 +2855,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
   · intro n h₁ h₂
-    simp; rfl
+    simp
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by
   apply ext

src/Init/Data/Array/MapIdx.lean

@@ -72,7 +72,6 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     (xs.mapFinIdx f).toList = xs.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
   apply List.ext_getElem <;> simp
@@ -106,7 +105,6 @@ theorem mapIdx_spec {f : Nat → α → β} {xs : Array α}
       xs[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapIdx {f : Nat → α → β} {xs : Array α} :
     (xs.mapIdx f).toList = xs.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp

src/Init/Data/Array/OfFn.lean

@@ -41,7 +41,6 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     intro h₃
     simp only [show i = n by omega]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
   induction m with
@@ -108,7 +107,6 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, Fin.foldlM_succ_last]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))

src/Init/Data/BitVec/Lemmas.lean

@@ -1198,7 +1198,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
       (decide (0 < len) &&
       (decide (start + len ≤ w) &&
       x.getMsbD (w - (start + len)))) := by
-  simp [BitVec.msb, getMsbD_extractLsb']; rfl
+  simp [BitVec.msb, getMsbD_extractLsb']
 
 @[simp, grind =] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -1234,7 +1234,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp, grind =] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by
-  simp [BitVec.msb]; rfl
+  simp [BitVec.msb]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -2784,9 +2784,8 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
   ext i ih
   rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
-  simp; rfl
+  simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
@@ -5292,7 +5291,6 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =]
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
@@ -5344,7 +5342,6 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w
 theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
     (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by simp [append_assoc]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem replicate_append_self {x : BitVec w} :
     x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
   induction n with

src/Init/Data/Bool.lean

@@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose, implicit_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/Char/Lemmas.lean

@@ -50,7 +50,7 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·)
   trans := Char.lt_trans
 
 -- This instance is useful while setting up instances for `String`.
-@[instance_reducible]
+@[implicit_reducible]
 def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
   trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
 

src/Init/Data/Fin/Fold.lean

@@ -164,7 +164,7 @@ theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldlM_succ_last, ← Nat.add_assoc, ih]; rfl
+    simp [foldlM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldrM -/
 
@@ -222,7 +222,7 @@ theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldrM_succ_last, ← Nat.add_assoc, ih]; rfl
+    simp [foldrM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldl -/
 
@@ -268,7 +268,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) :
         (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
   induction m with
   | zero => simp
-  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]; rfl
+  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
@@ -321,7 +321,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) :
         (foldr m (fun i => f (i.natAdd n)) x) := by
   induction m generalizing x with
   | zero => simp
-  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]; rfl
+  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by

src/Init/Data/Fin/Iterate.lean

@@ -69,7 +69,7 @@ private theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i →
     have g : ¬ (i < n) := by simp at p; simp [p]
     have r : Q n (_root_.cast (congrArg P p) s) :=
       @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p
-    simp only [g, r, dite_false]
+    simp only [g, dite_false]; exact r
   | succ j inv =>
     unfold hIterateFrom
     have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p

src/Init/Data/Fin/Lemmas.lean

@@ -123,7 +123,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -145,7 +145,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 

src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean

@@ -750,7 +750,6 @@ theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
   simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 -- There is hope to generalize the following theorem as soon there is a `Shrink` type.
 /--
 This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.

src/Init/Data/Iterators/Lemmas/Producers/List.lean

@@ -23,7 +23,6 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
@@ -32,7 +31,7 @@ theorem List.step_iter_nil :
 @[simp]
 theorem List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
-  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]; rfl
+  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]
 
 @[simp, grind =]
 theorem List.toArray_iter {l : List β} :

src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -31,7 +31,7 @@ theorem List.step_iterM_nil :
 @[simp]
 theorem List.step_iterM_cons {x : β} {xs : List β} :
     ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  simp only [List.iterM, IterM.step, Iterator.step]; rfl
+  simp only [List.iterM, IterM.step, Iterator.step]
 
 theorem List.step_iterM {l : List β} :
     (l.iterM m).step = match l with

src/Init/Data/List/Lemmas.lean

@@ -3525,7 +3525,7 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} :
   · split
     · rfl
     · have h' : i - 1 < l.length := Nat.lt_of_le_of_lt (Nat.pred_le _) h
-      simp [h']; rfl
+      simp [h']
 
 theorem head?_insert {l : List α} {a : α} :
     (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a) := by

src/Init/Data/List/MapIdx.lean

@@ -350,7 +350,6 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
   | [], acc, i => by
     simp only [mapIdx.go, getElem?_def, Array.length_toList,
       ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none]
-    rfl
   | a :: l, acc, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]

src/Init/Data/List/OfFn.lean

@@ -99,7 +99,6 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
   induction m with
   | zero => simp
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [-ofFn_succ, ofFn_succ_last, ih]
 
 @[simp]
@@ -157,7 +156,6 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
   induction k with
   | zero => simp
   | succ k ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [ofFnM_succ_last, ih]
 
 end List

src/Init/Data/List/ToArray.lean

@@ -589,7 +589,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
 @[simp, grind =] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
-  simp; rfl
+  simp
 
 @[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
     l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
@@ -644,8 +644,8 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
       drop_append_of_le_length (by simp; omega)]
     simp only [append_assoc, cons_append, nil_append]
     cases i with
-    | zero => simp; rfl
-    | succ i => rw [take_set_of_le (by omega)]; rfl
+    | zero => simp
+    | succ i => rw [take_set_of_le (by omega)]
   · simp only [Nat.not_lt] at h'
     have : i = j := by omega
     subst this

src/Init/Data/Nat/Fold.lean

@@ -400,7 +400,6 @@ theorem dfold_add
   induction m with
   | zero => simp; rfl
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [dfold_congr (Nat.add_assoc n m 1).symm, ih]
 
 @[simp] theorem dfoldRev_zero
@@ -436,7 +435,6 @@ theorem dfoldRev_add
   induction m with
   | zero => simp; rfl
   | succ m ih =>
-    set_option backward.isDefEq.respectTransparency false in
     simp [← Nat.add_assoc, ih]
 
 end Nat

src/Init/Data/Option/Attach.lean

@@ -444,7 +444,6 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
-set_option backward.isDefEq.respectTransparency false in
 public instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
@@ -456,7 +455,6 @@ end Option
 
 namespace OptionT
 
-set_option backward.isDefEq.respectTransparency false in
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by

src/Init/Data/Ord/Basic.lean

@@ -619,7 +619,7 @@ protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} :
 end List
 
 /-- The lexicographic order on pairs. -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
@@ -627,14 +627,14 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where
 Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.eq`.
 -/
-@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where
+@[expose, implicit_reducible] def beqOfOrd [Ord α] : BEq α where
   beq a b := (compare a b).isEq
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where
+@[expose, implicit_reducible] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 @[inline]
@@ -645,7 +645,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
 Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
-@[expose, instance_reducible] def leOfOrd [Ord α] : LE α where
+@[expose, implicit_reducible] def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
 @[inline]
@@ -677,7 +677,7 @@ Inverts the order of an `Ord` instance.
 The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
 and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
 -/
-@[expose, instance_reducible] protected def opposite (ord : Ord α) : Ord α where
+@[expose, implicit_reducible] protected def opposite (ord : Ord α) : Ord α where
   compare x y := ord.compare y x
 
 /--
@@ -688,7 +688,7 @@ In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` acco
 The function `compareOn` can be used to perform this comparison without constructing an intermediate
 `Ord` instance.
 -/
-@[expose, instance_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where
+@[expose, implicit_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -707,7 +707,7 @@ The function `compareLex` can be used to perform this comparison without constru
 intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
 comparisons.
 -/
-@[expose, instance_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
+@[expose, implicit_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
 end Ord

src/Init/Data/Order/Factories.lean

@@ -23,7 +23,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMin α` instance.
 -/
-@[inline, instance_reducible]
+@[inline, implicit_reducible]
 public def _root_.Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α where
   min a b := if a ≤ b then a else b
 
@@ -33,7 +33,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMax α` instance.
 -/
-@[inline, instance_reducible]
+@[inline, implicit_reducible]
 public def _root_.Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α where
   max a b := if b ≤ a then a else b
 

src/Init/Data/Order/FactoriesExtra.lean

@@ -19,7 +19,7 @@ Creates an `LE α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where
   le a b := (compare a b).isLE
 
@@ -39,7 +39,7 @@ Creates an `LT α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.LT.ofOrd (α : Type u) [Ord α] :
     LT α where
   lt a b := compare a b = .lt
@@ -104,7 +104,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf
 
 /--
 Creates a `BEq α` instance from an `Ord α` instance. -/
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def _root_.BEq.ofOrd (α : Type u) [Ord α] :
     BEq α where
   beq a b := compare a b = .eq

src/Init/Data/Order/Opposite.lean

@@ -52,7 +52,7 @@ def max' [LE α] [DecidableLE α] (a b : α) : α :=
 Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α`
 instance for the opposite order.
 -/
-@[instance_reducible] def LE.opposite (le : LE α) : LE α where
+@[implicit_reducible] def LE.opposite (le : LE α) : LE α where
   le a b := b ≤ a
 
 theorem LE.opposite_def {le : LE α} :

src/Init/Data/Order/PackageFactories.lean

@@ -169,7 +169,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans`
   instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def PreorderPackage.ofLE (α : Type u)
     (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where
   toLE := args.le
@@ -254,7 +254,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl`, `le_trans` and `le_antisymm`, can be omitted if `Refl`,
   `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def PartialOrderPackage.ofLE (α : Type u)
     (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -383,7 +383,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans`
   instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def LinearPreorderPackage.ofLE (α : Type u)
     (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -485,7 +485,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if
   `Total`, `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def LinearOrderPackage.ofLE (α : Type u)
     (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where
   toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -102,7 +102,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]; rfl
+  simp [Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : Iter (α := Rxc.Iterator α) α} {step} :
@@ -680,7 +680,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]; rfl
+  simp [Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : Iter (α := Rxo.Iterator α) α} {step} :
@@ -1244,7 +1244,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Std.Iterator.step]; rfl
+  simp [IterM.step, Std.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} {step} :

src/Init/Data/SInt/Basic.lean

@@ -409,7 +409,7 @@ Examples:
  * `(if (5 : Int8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int8) < 7) by decide`
 -/
-@[extern "lean_int8_dec_lt", instance_reducible]
+@[extern "lean_int8_dec_lt", implicit_reducible]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -425,7 +425,7 @@ Examples:
  * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int8) ≤ 7 by decide`
 -/
-@[extern "lean_int8_dec_le", instance_reducible]
+@[extern "lean_int8_dec_le", implicit_reducible]
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -778,7 +778,7 @@ Examples:
  * `(if (5 : Int16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int16) < 7) by decide`
 -/
-@[extern "lean_int16_dec_lt", instance_reducible]
+@[extern "lean_int16_dec_lt", implicit_reducible]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -794,7 +794,7 @@ Examples:
  * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int16) ≤ 7 by decide`
 -/
-@[extern "lean_int16_dec_le", instance_reducible]
+@[extern "lean_int16_dec_le", implicit_reducible]
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1163,7 +1163,7 @@ Examples:
  * `(if (5 : Int32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int32) < 7) by decide`
 -/
-@[extern "lean_int32_dec_lt", instance_reducible]
+@[extern "lean_int32_dec_lt", implicit_reducible]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1179,7 +1179,7 @@ Examples:
  * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int32) ≤ 7 by decide`
 -/
-@[extern "lean_int32_dec_le", instance_reducible]
+@[extern "lean_int32_dec_le", implicit_reducible]
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1568,7 +1568,7 @@ Examples:
  * `(if (5 : Int64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int64) < 7) by decide`
 -/
-@[extern "lean_int64_dec_lt", instance_reducible]
+@[extern "lean_int64_dec_lt", implicit_reducible]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 /--
@@ -1583,7 +1583,7 @@ Examples:
  * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int64) ≤ 7 by decide`
 -/
-@[extern "lean_int64_dec_le", instance_reducible]
+@[extern "lean_int64_dec_le", implicit_reducible]
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1958,7 +1958,7 @@ Examples:
  * `(if (5 : ISize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : ISize) < 7) by decide`
 -/
-@[extern "lean_isize_dec_lt", instance_reducible]
+@[extern "lean_isize_dec_lt", implicit_reducible]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1974,7 +1974,7 @@ Examples:
  * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : ISize) ≤ 7 by decide`
 -/
-@[extern "lean_isize_dec_le", instance_reducible]
+@[extern "lean_isize_dec_le", implicit_reducible]
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -55,7 +55,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
 
 instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 def Subarray.instToIterator :=
   ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (⟨⟨·⟩⟩)
 attribute [instance] Subarray.instToIterator

src/Init/Data/Slice/Array/Lemmas.lean

@@ -278,7 +278,7 @@ public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.
 
 public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} :
     xs.toList[i]'h = xs[i]'(by simpa using h) := by
-  simp [getElem_eq_getElem_array, toList_eq_drop_take]; rfl
+  simp [getElem_eq_getElem_array, toList_eq_drop_take]
 
 public theorem Subarray.getElem_eq_getElem_toList {xs : Subarray α} {h : i < xs.size} :
     xs[i]'h = xs.toList[i]'(by simpa using h) := by

src/Init/Data/Slice/List/Iterator.lean

@@ -22,7 +22,7 @@ open Std Slice PRange Iterators
 
 variable {α : Type u}
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 def ListSlice.instToIterator :=
   ToIterator.of (γ := Slice (Internal.ListSliceData α)) _ (fun s => match s.internalRepresentation.stop with
       | some n => s.internalRepresentation.list.iter.take n

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -296,7 +296,6 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel p
     [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
   isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList
 
-set_option backward.isDefEq.respectTransparency false in
 theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat]
     [ForwardPatternModel pat] [LawfulForwardPatternModel pat] :
     letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation

src/Init/Data/String/Lemmas/Pattern/Split.lean

@@ -197,7 +197,6 @@ theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ)
     · exact h' p hp₁ hp
     · exact rej _ (Std.not_lt.1 hp) hp₂
 
-set_option backward.isDefEq.respectTransparency false in
 theorem SplitIterator.toList_eq_splitFromSteps {ρ : Type} {pat : ρ} {σ : Slice → Type}
     [ToForwardSearcher pat σ]
     [∀ s, Std.Iterator (σ s) Id (SearchStep s)] [∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice}

src/Init/Data/UInt/Basic.lean

@@ -372,7 +372,7 @@ Examples:
  * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt16) < 7) by decide`
 -/
-@[extern "lean_uint16_dec_lt", instance_reducible]
+@[extern "lean_uint16_dec_lt", implicit_reducible]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -389,7 +389,7 @@ Examples:
  * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt16) ≤ 7 by decide`
 -/
-@[extern "lean_uint16_dec_le", instance_reducible]
+@[extern "lean_uint16_dec_le", implicit_reducible]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
@@ -736,7 +736,7 @@ Examples:
  * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt64) < 7) by decide`
 -/
-@[extern "lean_uint64_dec_lt", instance_reducible]
+@[extern "lean_uint64_dec_lt", implicit_reducible]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -752,7 +752,7 @@ Examples:
  * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt64) ≤ 7 by decide`
 -/
-@[extern "lean_uint64_dec_le", instance_reducible]
+@[extern "lean_uint64_dec_le", implicit_reducible]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/UInt/BasicAux.lean

@@ -399,7 +399,7 @@ Examples:
  * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : USize) < 7) by decide`
 -/
-@[extern "lean_usize_dec_lt", instance_reducible]
+@[extern "lean_usize_dec_lt", implicit_reducible]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -415,7 +415,7 @@ Examples:
  * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : USize) ≤ 7 by decide`
 -/
-@[extern "lean_usize_dec_le", instance_reducible]
+@[extern "lean_usize_dec_le", implicit_reducible]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/Vector/Algebra.lean

@@ -75,7 +75,7 @@ def mul [Mul α] (xs ys : Vector α n) : Vector α n :=
 Pointwise multiplication of vectors.
 This is not a global instance as in some applications different multiplications may be relevant.
 -/
-@[instance_reducible]
+@[implicit_reducible]
 def instMul [Mul α] : Mul (Vector α n) := ⟨mul⟩
 
 section mul

src/Init/Data/Vector/Extract.lean

@@ -132,7 +132,6 @@ theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} :
   rcases ys with ⟨ys, rfl⟩
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).extract 0 n = (xs.extract 0 n).cast (by omega) := by
   ext i h
@@ -179,7 +178,7 @@ theorem mem_extract_iff_getElem {xs : Vector α n} {a : α} {i j : Nat} :
 theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < n) {a : α} :
     xs.set i a = ((xs.extract 0 i).push a ++ (xs.extract (i + 1) n)).cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
-  simp [Array.set_eq_push_extract_append_extract]; rfl
+  simp [Array.set_eq_push_extract_append_extract]
 
 theorem extract_reverse {xs : Vector α n} {i j : Nat} :
     xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by

src/Init/Data/Vector/Lemmas.lean

@@ -528,7 +528,7 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} :
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
-  simp; rfl
+  simp
 
 @[simp] theorem getElem?_toList {xs : Vector α n} {i : Nat} :
     xs.toList[i]? = xs[i]? := by

src/Init/Data/Vector/OfFn.lean

@@ -119,7 +119,6 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, ofFnM_go_succ]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM (fun i => f (i.castLE (Nat.le_add_right n k)))

src/Init/Grind/Module/Basic.lean

@@ -60,7 +60,7 @@ class NatModule (M : Type u) extends AddCommMonoid M where
   /-- Scalar multiplication by a successor. -/
   add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) • a = n • a + a
 
-attribute [instance_reducible] NatModule.nsmul
+attribute [implicit_reducible] NatModule.nsmul
 attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
 /--
@@ -83,7 +83,7 @@ class IntModule (M : Type u) extends AddCommGroup M where
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
   zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) • a = n • a
 
-attribute [instance_reducible] IntModule.zsmul
+attribute [implicit_reducible] IntModule.zsmul
 attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
 namespace IntModule

src/Init/Grind/Module/Envelope.lean

@@ -204,7 +204,7 @@ theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul
   induction a using Q.ind with | _ a
   rcases a with ⟨a₁, a₂⟩; simp; omega
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofNatModule : IntModule (Q α) := {
   nsmul := ⟨nsmul⟩,
   zsmul := ⟨zsmul⟩,

src/Init/Grind/Ring/Basic.lean

@@ -94,7 +94,7 @@ class Semiring (α : Type u) extends Add α, Mul α where
   -/
   nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl
 
-attribute [instance_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
+attribute [implicit_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
 
 /--
 A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
@@ -120,7 +120,7 @@ class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
   /-- The canonical map from the integers is consistent with negation. -/
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
-attribute [instance_reducible] Ring.intCast Ring.zsmul
+attribute [implicit_reducible] Ring.intCast Ring.zsmul
 
 /--
 A commutative semiring, i.e. a semiring with commutative multiplication.
@@ -184,7 +184,7 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by
 
 theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by
   induction b with
-  | zero => simp [Nat.mul_zero, mul_zero]; rfl
+  | zero => simp [Nat.mul_zero, mul_zero]
   | succ a ih => rw [Nat.mul_succ, ofNat_add, ih, ofNat_add, left_distrib, mul_one]
 
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by

src/Init/Grind/Ring/Envelope.lean

@@ -245,7 +245,7 @@ theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by
     · have : i = 0 := by omega
       simp [this]
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofSemiring : Ring (Q α) := {
   nsmul := ⟨nsmul⟩
   zsmul := ⟨zsmul⟩
@@ -506,7 +506,7 @@ theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b
   obtain ⟨⟨b₁, b₂⟩⟩ := b
   apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl
 
-@[instance_reducible]
+@[implicit_reducible]
 def ofCommSemiring : CommRing (OfSemiring.Q α) :=
   { OfSemiring.ofSemiring with
     mul_comm := mul_comm }

src/Init/Grind/Ring/Field.lean

@@ -38,7 +38,7 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where
   /-- Raising to a negative power is the inverse of raising to the positive power. -/
   zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹
 
-attribute [instance_reducible] Field.zpow
+attribute [implicit_reducible] Field.zpow
 attribute [instance 100] Field.toInv Field.toDiv Field.zpow
 
 namespace Field

src/Init/GrindInstances/Ring/SInt.lean

@@ -20,11 +20,11 @@ public section
 
 namespace Lean.Grind
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int8.natCast : NatCast Int8 where
   natCast x := Int8.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int8.intCast : IntCast Int8 where
   intCast x := Int8.ofInt x
 
@@ -75,11 +75,11 @@ example : ToInt.Sub Int8 (.sint 8) := inferInstance
 
 instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int16.natCast : NatCast Int16 where
   natCast x := Int16.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int16.intCast : IntCast Int16 where
   intCast x := Int16.ofInt x
 
@@ -130,11 +130,11 @@ example : ToInt.Sub Int16 (.sint 16) := inferInstance
 
 instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int32.natCast : NatCast Int32 where
   natCast x := Int32.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int32.intCast : IntCast Int32 where
   intCast x := Int32.ofInt x
 
@@ -185,11 +185,11 @@ example : ToInt.Sub Int32 (.sint 32) := inferInstance
 
 instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int64.natCast : NatCast Int64 where
   natCast x := Int64.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def Int64.intCast : IntCast Int64 where
   intCast x := Int64.ofInt x
 
@@ -240,11 +240,11 @@ example : ToInt.Sub Int64 (.sint 64) := inferInstance
 
 instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp)
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def ISize.natCast : NatCast ISize where
   natCast x := ISize.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def ISize.intCast : IntCast ISize where
   intCast x := ISize.ofInt x
 

src/Init/GrindInstances/Ring/UInt.lean

@@ -20,11 +20,11 @@ namespace UInt8
 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/
 theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def natCast : NatCast UInt8 where
   natCast x := UInt8.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def intCast : IntCast UInt8 where
   intCast x := UInt8.ofInt x
 
@@ -51,11 +51,11 @@ namespace UInt16
 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/
 theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def natCast : NatCast UInt16 where
   natCast x := UInt16.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def intCast : IntCast UInt16 where
   intCast x := UInt16.ofInt x
 
@@ -82,11 +82,11 @@ namespace UInt32
 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/
 theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def natCast : NatCast UInt32 where
   natCast x := UInt32.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def intCast : IntCast UInt32 where
   intCast x := UInt32.ofInt x
 
@@ -113,11 +113,11 @@ namespace UInt64
 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/
 theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def natCast : NatCast UInt64 where
   natCast x := UInt64.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def intCast : IntCast UInt64 where
   intCast x := UInt64.ofInt x
 
@@ -141,11 +141,11 @@ end UInt64
 
 namespace USize
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def natCast : NatCast USize where
   natCast x := USize.ofNat x
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 def intCast : IntCast USize where
   intCast x := USize.ofInt x
 

src/Init/Hints.lean

@@ -14,11 +14,3 @@ public section
 unif_hint (p : Prop) where
   ⊢ Not p =?= p → False
 
-unif_hint (n : Nat) where
-  ⊢ n - 0 =?= n
-
-unif_hint (n : Nat) where
-  ⊢ n + 0 =?= n
-
-unif_hint (n : Nat) where
-  ⊢ n * 0 =?= 0

src/Init/Prelude.lean

@@ -1726,7 +1726,7 @@ Addition of natural numbers, typically used via the `+` operator.
 This function is overridden in both the kernel and the compiler to efficiently evaluate using the
 arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
-@[extern "lean_nat_add"]
+@[extern "lean_nat_add", implicit_reducible]
 protected def Nat.add : (@& Nat) → (@& Nat) → Nat
   | a, Nat.zero   => a
   | a, Nat.succ b => Nat.succ (Nat.add a b)
@@ -1745,7 +1745,7 @@ Multiplication of natural numbers, usually accessed via the `*` operator.
 This function is overridden in both the kernel and the compiler to efficiently evaluate using the
 arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
-@[extern "lean_nat_mul"]
+@[extern "lean_nat_mul", implicit_reducible]
 protected def Nat.mul : (@& Nat) → (@& Nat) → Nat
   | _, 0          => 0
   | a, Nat.succ b => Nat.add (Nat.mul a b) a
@@ -2076,7 +2076,7 @@ Examples:
 * `8 - 8 = 0`
 * `8 - 20 = 0`
 -/
-@[extern "lean_nat_sub"]
+@[extern "lean_nat_sub", implicit_reducible]
 protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
   | a, 0      => a
   | a, succ b => pred (Nat.sub a b)
@@ -2478,7 +2478,7 @@ Examples:
  * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt8) < 7) by decide`
 -/
-@[extern "lean_uint8_dec_lt", instance_reducible]
+@[extern "lean_uint8_dec_lt", implicit_reducible]
 def UInt8.decLt (a b : UInt8) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2494,7 +2494,7 @@ Examples:
  * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt8) ≤ 7 by decide`
 -/
-@[extern "lean_uint8_dec_le", instance_reducible]
+@[extern "lean_uint8_dec_le", implicit_reducible]
 def UInt8.decLe (a b : UInt8) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
@@ -2638,7 +2638,7 @@ Examples:
  * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt32) < 7) by decide`
 -/
-@[extern "lean_uint32_dec_lt", instance_reducible]
+@[extern "lean_uint32_dec_lt", implicit_reducible]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2654,7 +2654,7 @@ Examples:
  * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt32) ≤ 7 by decide`
 -/
-@[extern "lean_uint32_dec_le", instance_reducible]
+@[extern "lean_uint32_dec_le", implicit_reducible]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
@@ -3208,7 +3208,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar
 its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
 internal detail that's not observable by Lean code.
 -/
-@[extern "lean_array_get_size", tagged_return]
+@[extern "lean_array_get_size", tagged_return, implicit_reducible]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 

src/Init/WF.lean

@@ -144,7 +144,7 @@ end WellFounded
 open WellFounded
 
 -- Empty relation is well-founded
-@[instance_reducible]
+@[implicit_reducible]
 def emptyWf {α : Sort u} : WellFoundedRelation α where
   rel := emptyRelation
   wf  := by
@@ -218,7 +218,7 @@ theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
 namespace Nat
 
 -- less-than is well-founded
-@[instance_reducible]
+@[implicit_reducible]
 def lt_wfRel : WellFoundedRelation Nat where
   rel := (· < ·)
   wf  := by
@@ -363,7 +363,7 @@ theorem RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.L
   | intro h₁ h₂ => exact Prod.Lex.left _ _ h₁
 
 -- The relational product of well founded relations is well-founded
-@[instance_reducible]
+@[implicit_reducible]
 def rprod (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
   rel := RProd ha.rel hb.rel
   wf  := by
@@ -456,7 +456,7 @@ section
 def SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (fun _ => β) → @PSigma α (fun _ => β) → Prop :=
   RevLex emptyRelation s
 
-@[instance_reducible]
+@[implicit_reducible]
 def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation (PSigma fun _ : α => β) where
   rel := SkipLeft α hb.rel
   wf  := revLex emptyWf.wf hb.wf

src/Lean/Meta/ExprDefEq.lean

@@ -64,7 +64,7 @@ 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
+  defValue := true
   descr    := "if true, bump transparency to `.instances` for all implicit arguments, \
   not just instance-implicit ones"
 }

src/Std/Data/DHashMap/IteratorLemmas.lean

@@ -22,12 +22,12 @@ open Std.Iterators
 @[simp]
 public theorem step_iter_nil {α : Type u} {β : α → Type v} :
     ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ := by
-  simp [Iter.step_eq, iter]; rfl
+  simp [Iter.step_eq, iter]
 
 @[simp]
 public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} :
     ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by
-  simp [Iter.step_eq, iter]; rfl
+  simp [Iter.step_eq, iter]
 
 @[simp]
 public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} :

src/Std/Data/DHashMap/Lemmas.lean

@@ -4549,7 +4549,7 @@ end Const
 end Equiv
 
 /-- Internal implementation detail of the hash map. -/
-@[instance_reducible]
+@[implicit_reducible]
 def isSetoid (α β) [BEq α] [Hashable α] : Setoid (DHashMap α β) where
   r := Equiv
   iseqv := {

src/Std/Data/DTreeMap/Internal/Zipper.lean

@@ -373,7 +373,7 @@ public def Zipper.iter (t : Zipper α β) : Iter (α := Zipper α β) ((a : α)
 public def Zipper.iterOfTree (t : Impl α β) : Iter (α := Zipper α β) ((a : α) × β a) :=
   Zipper.iter <| Zipper.done.prependMap t
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def Zipper.instToIterator :=
   ToIterator.of (γ := Zipper α β) _ (fun z => z.iter)
 attribute [instance] Zipper.instToIterator
@@ -688,7 +688,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Ric.Sliceable (Impl α β) α (RicSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RicSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (Internal.RicSliceData α β)) (β := ((a : α) × β a)) _
     (fun s => ⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩)
@@ -718,7 +718,7 @@ public abbrev RicSlice α [Ord α] := Slice (RicSliceData α)
 public instance {α : Type u} [Ord α] : Ric.Sliceable (Impl α (fun _ => Unit)) α (Unit.RicSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RicSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RicSliceData α)) (β := α) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -753,7 +753,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Ric.Sliceable (Impl α (fun _ => β)) α (RicSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RicSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RicSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -788,7 +788,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rio.Sliceable (Impl α β) α (RioSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RioSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α β)) (β := (a : α) × β a) _ fun s =>
     ⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩
@@ -819,7 +819,7 @@ public abbrev RioSlice α [Ord α] := Slice (RioSliceData α)
 public instance {α : Type u} [Ord α] : Rio.Sliceable (Impl α (fun _ => Unit)) α (Unit.RioSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RioSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -854,7 +854,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rio.Sliceable (Impl α (fun _ => β)) α (RioSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RioSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -922,7 +922,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rcc.Sliceable (Impl α β) α (RccSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RccSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α β)) (β := (a : α) × β a) _ fun s =>
     (rccIterator s.1.treeMap s.1.range.lower s.1.range.upper)
@@ -950,7 +950,7 @@ public abbrev RccSlice α [Ord α] := Slice (RccSliceData α)
 public instance {α : Type u} [Ord α] : Rcc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RccSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RccSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -987,7 +987,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rcc.Sliceable (Impl α (fun _ => β)) α (RccSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RccSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1059,7 +1059,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rco.Sliceable (Impl α β) α (RcoSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RcoSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rcoIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1087,7 +1087,7 @@ public abbrev RcoSlice α [Ord α] := Slice (RcoSliceData α)
 public instance {α : Type u} [Ord α] : Rco.Sliceable (Impl α (fun _ => Unit)) α (Unit.RcoSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RcoSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1124,7 +1124,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rco.Sliceable (Impl α (fun _ => β)) α (RcoSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RcoSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1195,7 +1195,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roo.Sliceable (Impl α β) α (RooSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RooSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rooIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1223,7 +1223,7 @@ public abbrev RooSlice α [Ord α] := Slice (RooSliceData α)
 public instance {α : Type u} [Ord α] : Roo.Sliceable (Impl α (fun _ => Unit)) α (Unit.RooSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RooSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1260,7 +1260,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roo.Sliceable (Impl α (fun _ => β)) α (RooSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RooSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1332,7 +1332,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roc.Sliceable (Impl α β) α (RocSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RocSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rocIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1360,7 +1360,7 @@ public abbrev RocSlice α [Ord α] := Slice (RocSliceData α)
 public instance {α : Type u} [Ord α] : Roc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RocSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RocSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1397,7 +1397,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roc.Sliceable (Impl α (fun _ => β)) α (RocSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RocSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1454,7 +1454,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rci.Sliceable (Impl α β) α (RciSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RciSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rciIterator s.1.treeMap s.1.range.lower
@@ -1482,7 +1482,7 @@ public abbrev RciSlice α [Ord α] := Slice (RciSliceData α)
 public instance {α : Type u} [Ord α] : Rci.Sliceable (Impl α (fun _ => Unit)) α (Unit.RciSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RciSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α)) _ fun s =>
     (⟨Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
@@ -1522,7 +1522,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rci.Sliceable (Impl α (fun _ => β)) α (RciSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RciSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α β)) _ fun s =>
     (⟨(Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1580,7 +1580,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roi.Sliceable (Impl α β) α (RoiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RoiSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α β)) (β := (a : α) × β a) _ fun s =>
     roiIterator s.1.treeMap s.1.range.lower
@@ -1608,7 +1608,7 @@ public abbrev RoiSlice α [Ord α] := Slice (RoiSliceData α)
 public instance {α : Type u} [Ord α] : Roi.Sliceable (Impl α (fun _ => Unit)) α (Unit.RoiSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RoiSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α)) _ fun s =>
     (⟨Zipper.prependMapGT s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
@@ -1648,7 +1648,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roi.Sliceable (Impl α (fun _ => β)) α (RoiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RoiSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α β)) _ fun s =>
     (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1700,7 +1700,7 @@ public abbrev RiiSlice α β := Slice (RiiSliceData α β)
 public instance {α : Type u} {β : α → Type v} : Rii.Sliceable (Impl α β) α (RiiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RiiSlice.instToIterator {β : α → Type v} :=
   ToIterator.of (γ := Slice (RiiSliceData α β)) (β := (a : α) × β a) _ fun s =>
     riiIterator s.1.treeMap
@@ -1726,7 +1726,7 @@ public abbrev RiiSlice α  := Slice (RiiSliceData α)
 public instance {α : Type u} : Rii.Sliceable (Impl α (fun _ => Unit)) α (Unit.RiiSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RiiSlice.instToIterator {α : Type u} :=
   ToIterator.of (γ := Slice (RiiSliceData α)) _ fun s =>
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter _ ).map fun e => (e.1)
@@ -1759,7 +1759,7 @@ public abbrev RiiSlice α β  := Slice (RiiSliceData α β)
 public instance {α : Type u} {β : Type v} : Rii.Sliceable (Impl α (fun _ => β)) α (Const.RiiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def RiiSlice.instToIterator {α : Type u} {β : Type v} :=
   ToIterator.of (γ := Slice (RiiSliceData α β)) _ fun s =>
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)

src/Std/Data/DTreeMap/Lemmas.lean

@@ -5882,7 +5882,7 @@ end Equiv
 section Equiv
 
 /-- Implementation detail of the tree map -/
-@[instance_reducible]
+@[implicit_reducible]
 def isSetoid (α : Type u) (β : α → Type v) (cmp : α → α → Ordering := by exact compare) :
     Setoid (Std.DTreeMap α β cmp) where
   r := Equiv

src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean

@@ -53,7 +53,6 @@ theorem Array.step_iterM {array : Array β} :
 
 section Equivalence
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM [LawfulMonad m] {array : Array β}
     {pos : Nat} :
     (array.iterFromIdxM m pos).stepAsHetT = (if _ : pos < array.size then

src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -16,7 +16,6 @@ open Std.Internal Std.Iterators Std.Iterators.Types
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
 -- We don't want to pollute `List` with this rarely used lemma.
-set_option backward.isDefEq.respectTransparency false in
 public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).stepAsHetT = (match l with
       | [] => pure .done

src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean

@@ -19,7 +19,6 @@ open Std.Iterators
 
 variable {α : Type w} {f : α → α} {init : α}
 
-set_option backward.isDefEq.respectTransparency false in
 theorem Iter.step_repeat :
     (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, rfl⟩ := by
   simp [Iter.«repeat», Iter.step, Iter.toIterM, IterM.step, Iterator.step, IterM.toIter]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean

@@ -52,7 +52,6 @@ theorem aux4 {a b c : Nat} (hidx : a < b * c) (h : c ≤ n) : a < b * n := by
   | inl h => apply aux3 <;> assumption
   | inr h => simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
     ∀ (idx : Nat) (hidx : idx < w * curr),
@@ -73,7 +72,6 @@ theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     simp
 termination_by n - curr
 
-set_option backward.isDefEq.respectTransparency false in
 theorem go_get (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
     ∀ (idx : Nat) (hidx1 : idx < w * n),

src/lake/Lake/Build/Data.lean

@@ -51,7 +51,7 @@ public class OptDataKind (α : Type u) where
 
 namespace OptDataKind
 
-@[instance_reducible, instance low]
+@[implicit_reducible, instance low]
 public def anonymous : OptDataKind α where
   name := .anonymous
   wf h := by simp [Name.isAnonymous_iff_eq_anonymous] at h

stage0/src/stdlib_flags.h

@@ -22,6 +22,8 @@ options get_default_options() {
     opts = opts.update({"quotPrecheck"}, true);
 
     opts = opts.update({"pp", "rawOnError"}, true);
+    // enable implicit argument transparency bump
+    opts = opts.update({"backward", "isDefEq", "implicitBump"}, true);
 #endif
     return opts;
 }

tests/lean/ppMotives.lean.expected.out

@@ -1,4 +1,4 @@
-protected def Nat.add : Nat → Nat → Nat :=
+@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat :=
 fun x x_1 =>
   Nat.brecOn x_1
     (fun x f x_2 =>
@@ -7,7 +7,7 @@ fun x x_1 =>
         | a, b.succ => fun x => (x.1 a).succ)
         f)
     x
-protected def Nat.add : Nat → Nat → Nat :=
+@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat :=
 fun x x_1 =>
   Nat.brecOn (motive := fun x => Nat → Nat) x_1
     (fun x f x_2 =>

tests/lean/run/3807.lean

@@ -1147,7 +1147,7 @@ variable [FunLike F α β]
 
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} [RingHomClass F α β]
 
-@[instance_reducible]
+@[implicit_reducible]
 def RingHomClass.toRingHom (f : F) : α →+* β :=
   { (f : α →* β), (f : α →+ β) with }
 
@@ -1175,7 +1175,7 @@ end coe
 
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} {_ : NonAssocSemiring γ}
 
-@[instance_reducible]
+@[implicit_reducible]
 def comp (g : β →+* γ) (f : α →+* β) : α →+* γ :=
   { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with
     toFun := g ∘ f
@@ -1194,41 +1194,41 @@ namespace Injective
 
 variable {M₁ : Type _} {M₂ : Type _} [Mul M₁]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) : Semigroup M₁ :=
   { ‹Mul M₁› with mul_assoc := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addSemigroup {M₁} [Add M₁] [AddSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddSemigroup M₁ :=
   { ‹Add M₁› with add_assoc := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : CommMagma M₁ where
   mul_comm x y := sorry
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addCommMagma {M₁} [Add M₁] [AddCommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommMagma M₁ where
   add_comm x y := sorry
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommSemigroup M₁ where
   toSemigroup := hf.semigroup f
   __ := hf.commMagma f
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addCommSemigroup {M₁} [Add M₁] [AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommSemigroup M₁ where
   toAddSemigroup := hf.addSemigroup f
   __ := hf.addCommMagma f
 
 variable [One M₁]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) : MulOneClass M₁ :=
   { ‹One M₁›, ‹Mul M₁› with
     one_mul := sorry,
     mul_one := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f : M₁ → M₂) (hf : Injective f) : AddZeroClass M₁ :=
   { ‹Zero M₁›, ‹Add M₁› with
     zero_add := sorry,
@@ -1236,21 +1236,21 @@ protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f
 
 variable [Pow M₁ Nat]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) : Monoid M₁ :=
   { hf.mulOneClass f, hf.semigroup f with
     npow := fun n x => x ^ n,
     npow_zero := sorry,
     npow_succ := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoid M₁ :=
   { hf.addZeroClass f, hf.addSemigroup f with
     nsmul := fun n x => n • x,
     nsmul_zero := sorry,
     nsmul_succ := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [NatCast M₁]
     [AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoidWithOne M₁ :=
   { hf.addMonoid f with
@@ -1259,19 +1259,19 @@ protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Na
     natCast_succ := sorry,
     one := 1 }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) :
     CommMonoid M₁ :=
   { hf.monoid f, hf.commSemigroup f with }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addCommMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) :
     AddCommMonoid M₁ :=
   { hf.addMonoid f, hf.addCommSemigroup f with }
 
 variable [Inv M₁] [Div M₁] [Pow M₁ Int]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : DivInvMonoid M₁ :=
   { hf.monoid f, ‹Inv M₁›, ‹Div M₁› with
     zpow := fun n x => x ^ n,
@@ -1280,7 +1280,7 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti
     zpow_neg' := sorry,
     div_eq_mul_inv := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [SubNegMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : SubNegMonoid M₁ :=
   { hf.addMonoid f, ‹Neg M₁›, ‹Sub M₁› with
@@ -1290,18 +1290,18 @@ protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M
     zsmul_neg' := sorry,
     sub_eq_add_neg := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def group [Group M₂] (f : M₁ → M₂) (hf : Injective f) : Group M₁ :=
   { hf.divInvMonoid f with
     mul_left_inv := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [AddGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroup M₁ :=
   { hf.subNegMonoid f with
     add_left_neg := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroupWithOne M₁ :=
   { hf.addGroup f,
@@ -1310,11 +1310,11 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat
     intCast_ofNat := sorry,
     intCast_negSucc := sorry }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def commGroup [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommGroup M₁ :=
   { hf.commMonoid f, hf.group f with }
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def addCommGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [AddCommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommGroup M₁ :=
   { hf.addCommMonoid f, hf.addGroup f with }
@@ -1334,7 +1334,7 @@ section MulZeroClass
 
 variable [MulZeroClass M₀] {a b : M₀}
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroClass M₀' where
   mul := (· * ·)
   zero := 0
@@ -1347,7 +1347,7 @@ section MulZeroOneClass
 
 variable [MulZeroOneClass M₀]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀)
     (hf : Injective f) :
     MulZeroOneClass M₀' :=
@@ -1357,7 +1357,7 @@ end MulZeroOneClass
 
 section SemigroupWithZero
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.semigroupWithZero [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀]
     (f : M₀' → M₀) (hf : Injective f) :
     SemigroupWithZero M₀' :=
@@ -1367,7 +1367,7 @@ end SemigroupWithZero
 
 section MonoidWithZero
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' Nat]
     [MonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) :
     MonoidWithZero M₀' :=
@@ -1379,7 +1379,7 @@ section GroupWithZero
 
 variable [GroupWithZero G₀] {a b c g h x : G₀}
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.groupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀']
     [Pow G₀' Nat] [Pow G₀' Int] (f : G₀' → G₀) (hf : Injective f) : GroupWithZero G₀' :=
   { hf.monoidWithZero f,
@@ -1399,7 +1399,7 @@ universe u v x
 
 variable {α : Type u} {β : Type v} {R : Type x}
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R → S)
     (hf : Injective f) :
     Distrib R where
@@ -1409,33 +1409,33 @@ protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R
 variable [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul Nat β] [SMul Int β] [Pow β Nat]
   [NatCast β] [IntCast β]
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.nonUnitalNonAssocSemiring {α : Type u}
     [NonUnitalNonAssocSemiring α] (f : β → α) (hf : Injective f) : NonUnitalNonAssocSemiring β where
   toAddCommMonoid := hf.addCommMonoid f
   __ := hf.distrib f
   __ := hf.mulZeroClass f
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] (f : β → α)
     (hf : Injective f) :
     NonUnitalSemiring β where
   toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f
   __ := hf.semigroupWithZero f
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.nonAssocSemiring {α : Type u} [NonAssocSemiring α] [NatCast β] (f : β → α) (hf : Injective f) : NonAssocSemiring β where
   toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f
   __ := hf.mulZeroOneClass f
   __ := hf.addMonoidWithOne f
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.semiring {α : Type u} [Semiring α] [NatCast β] (f : β → α) (hf : Injective f) : Semiring β where
   toNonUnitalSemiring := hf.nonUnitalSemiring f
   __ := hf.nonAssocSemiring f
   __ := hf.monoidWithZero f
 
-@[instance_reducible]
+@[implicit_reducible]
 protected def Function.Injective.ring [Ring α] (f : β → α) (hf : Injective f) : Ring β where
   toSemiring := hf.semiring f
   __ := hf.addGroupWithOne f

tests/lean/run/boxing_bug.lean

@@ -1,4 +1,4 @@
-@[instance_reducible]
+@[implicit_reducible]
 def myCast : NatCast UInt8 where
   natCast := UInt8.ofNat
 

tests/lean/run/diagnostics.lean

@@ -8,11 +8,10 @@ theorem f_eq : f (x + 1) = q (f x) := rfl
 
 /--
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 4):
+  [reduction] unfolded declarations (max: 15, num: 3):
     [reduction] Nat.rec ↦ 15
     [reduction] Add.add ↦ 10
     [reduction] HAdd.hAdd ↦ 10
-    [reduction] Nat.add ↦ 10
   [reduction] unfolded reducible declarations (max: 15, num: 1):
     [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
@@ -25,11 +24,10 @@ example : f (x + 5) = q (q (q (q (q (f x))))) :=
 
 /--
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 15, num: 4):
+  [reduction] unfolded declarations (max: 15, num: 3):
     [reduction] Nat.rec ↦ 15
     [reduction] Add.add ↦ 10
     [reduction] HAdd.hAdd ↦ 10
-    [reduction] Nat.add ↦ 10
   [reduction] unfolded reducible declarations (max: 15, num: 1):
     [reduction] Nat.casesOn ↦ 15
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

tests/lean/run/grind_10160.lean

@@ -28,7 +28,7 @@ theorem MyInt.natCast_eq (n : Nat) : (n : MyInt) = formalDiff n 0 := rfl
 
 theorem MyInt.natCast_inj (n m : Nat) :
   (n : MyInt) = (m : MyInt) ↔ n = m := by
-  rw [natCast_eq, natCast_eq, eq]
+  rw [natCast_eq, natCast_eq, eq]; simp
 
 example (n m : Nat) : (n : MyInt) = (m : MyInt) ↔ n = m := by
   grind [MyInt.natCast_eq, MyInt.eq]

tests/lean/run/grind_bitvec2.lean

@@ -2001,8 +2001,7 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} :
   · subst n0
     simp [BitVec.eq_nil x, BitVec.toInt]
   · by_cases m0 : m = 0
-    · subst m0
-      simp [BitVec.eq_nil y, n0]
+    · subst m0; rw [BitVec.eq_nil y, append_zero_width]; simp [n0]
     · simp only [n0, ↓reduceIte]
       by_cases x.msb
       case pos h =>
@@ -3961,7 +3960,7 @@ theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by grind
 
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
-  simp [replicate]
+  simp only [replicate]; rw [append_zero_width]
 
 theorem replicate_succ {x : BitVec w} :
     x.replicate (n + 1) =

tests/lean/run/instanceReducibility.lean

@@ -1,6 +1,6 @@
 module
 
-/-! Reducibility of instances should default to `[instance_reducible]` but be overridable. -/
+/-! Reducibility of instances should default to `[implicit_reducible]` but be overridable. -/
 
 instance i1 : Inhabited Nat := inferInstance
 

tests/lean/run/instanceReducible.lean

@@ -23,7 +23,7 @@ attribute [instance] exposed
 #guard_msgs in
 attribute [local instance] exposed
 
-@[expose, instance_reducible]
+@[expose, implicit_reducible]
 public def exposedAndReducible : Inhabited Nat := inferInstance
 
 #guard_msgs in

tests/lean/run/ofNatNormNum.lean

@@ -26,7 +26,7 @@ instance [S α] : OfNat α n where
 instance [S α] : OfNatSound α where
   ofNat_add n m := by
     induction m with
-    | zero => simp; erw [S.add_zero]; rfl
+    | zero => simp [OfNat.ofNat, S.ofNat]; erw [S.add_zero]
     | succ m ih => simp [OfNat.ofNat, S.ofNat] at *; erw [← ih]; rw [S.add_assoc]
 
 theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by

tests/lean/run/symbolFrequency_foldRelevantConsts.lean

@@ -19,7 +19,7 @@ run_meta do
   let consts ← ci.type.foldRelevantConstants (init := #[]) (fun n ns => return ns.push n)
   logInfo m!"{consts}"
 
-/-- info: [Array, Nat, LT.lt, Array.size, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/
+/-- info: [Array, Nat, LT.lt, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/
 #guard_msgs in
 run_meta do
   let ci ← getConstInfo `Array.eraseIdx.induct

tests/lean/unfold1.lean

@@ -15,11 +15,8 @@ theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   | succ x ih =>
     unfold isEven
     trace_state
-    rw [Nat.mul_succ, Nat.add_succ]
-    simp
     unfold isOdd
     trace_state
-    simp
     exact ih
 
 theorem isEven_succ_succ (x : Nat) : isEven (x + 2) = isEven x := by

tests/lean/unfold1.lean.expected.out

@@ -1,12 +1,8 @@
-unfold1.lean:22:4-22:8: error: `simp` made no progress
 case succ
 x : Nat
 ih : isEven (2 * x) = true
-⊢ (match 2 * (x + 1) with
-    | 0 => true
-    | n.succ => isOdd n) =
-    true
+⊢ isOdd (Nat.mul 2 x + 1) = true
 case succ
 x : Nat
 ih : isEven (2 * x) = true
-⊢ isEven (2 * x) = true
+⊢ isEven (Nat.mul 2 x) = true

tests/lean/whnfProj.lean.expected.out

@@ -1,6 +1,6 @@
 [Meta.debug] 1. x + 1
 [Meta.debug] 2. x + 1
-[Meta.debug] 3. x.add 1
+[Meta.debug] 3. (x.add 0).succ
 [Meta.debug] 4. (x.add 0).succ
 [Meta.debug] 1. (x, x + 1).fst
 [Meta.debug] 2. x