diff --git a/src/Init/BinderNameHint.lean b/src/Init/BinderNameHint.lean
index db8af694c3..2dd7ca66ed 100644
--- a/src/Init/BinderNameHint.lean
+++ b/src/Init/BinderNameHint.lean
@@ -42,5 +42,5 @@ This gadget is supported by
 It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
-@[simp ↓, expose]
+@[simp ↓, expose, implicit_reducible]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e
diff --git a/src/Lean/DefEqAttrib.lean b/src/Lean/DefEqAttrib.lean
index 698db073a0..c9f443566b 100644
--- a/src/Lean/DefEqAttrib.lean
+++ b/src/Lean/DefEqAttrib.lean
@@ -16,6 +16,14 @@ public section
 namespace Lean
 open Meta
 
+register_builtin_option backward.defeqAttrib.useBackward : Bool := {
+  defValue := false
+  descr    := "When true, `dsimp` also uses theorems tagged `@[backward_defeq]`, i.e. \
+    theorems inferred to be rfl only at default (not instance) transparency. Set this \
+    locally (e.g. `set_option backward.defeqAttrib.useBackward true in ...`) to restore the \
+    pre-stricter-inference behavior for a specific proof."
+}
+
 /--
 There are defeq theorems that only hold at transparency `.all`, but also others that hold
 (from the kernel's point of view) but where the defeq checker here will run out of cycles.
@@ -26,48 +34,88 @@ private def isDefEqCareful (e1 e2 : Expr) : MetaM Bool := do
   withOptions (smartUnfolding.set · false) <| do
     withDefault (isDefEq e1 e2) <||> withTransparency .all (isDefEq e1 e2)
 
-def validateDefEqAttr (declName : Name) : AttrM Unit := do
-  let info ← getConstVal declName
-  MetaM.run' do
-    withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq`
-      forallTelescopeReducing info.type fun _ type => do
-        let type ← whnf type
-        -- NB: The warning wording should work both for explicit uses of `@[defeq]` as well as the implicit `:= rfl`.
-        let some (_, lhs, rhs) := type.eq? |
-          throwError m!"Not a definitional equality: the conclusion should be an equality, but is{inlineExpr type}"
-        let ok ← isDefEqCareful lhs rhs
-        unless ok do
-          let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
-            let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-            let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
-              not definitionally equal to the right-hand side{indentExpr rhs}"
-            if (← getEnv).isExporting then
-              let okPrivately ← withoutExporting <| isDefEqCareful lhs rhs
-              if okPrivately then
-                msg := msg ++ .note m!"This theorem is exported from the current module. \
-                  This requires that all definitions that need to be unfolded to prove this \
-                  theorem must be exposed."
-            pure msg
-          throwError explanation
+private def withEqLhsRhs (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
+  withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq`
+    forallTelescopeReducing type fun _ type => do
+      let type ← whnf type
+      -- NB: The warning wording should work both for explicit uses of `@[defeq]` as well as the implicit `:= rfl`.
+      let some (_, lhs, rhs) := type.eq? |
+        throwError m!"Not a definitional equality: the conclusion should be an equality, but is{inlineExpr type}"
+      k lhs rhs
 
 /--
-Marks the theorem as a definitional equality.
+Validates that `declName` is a definitional equality at `.default`/`.all` transparency
+(the legacy permissive check). Throws a diagnostic error if not. This is used both as
+the validator for the `@[defeq]` and `@[backward_defeq]` attributes and as a building
+block for `inferDefEqAttr`.
+-/
+def validateDefEqAttr (declName : Name) : AttrM Unit := do
+  let info ← getConstVal declName
+  MetaM.run' do withEqLhsRhs info.type fun lhs rhs => do
+    let ok ← isDefEqCareful lhs rhs
+    unless ok do
+      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+        let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+        let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
+          not definitionally equal to the right-hand side{indentExpr rhs}"
+        if (← getEnv).isExporting then
+          let okPrivately ← withoutExporting <| isDefEqCareful lhs rhs
+          if okPrivately then
+            msg := msg ++ .note m!"This theorem is exported from the current module. \
+              This requires that all definitions that need to be unfolded to prove this \
+              theorem must be exposed."
+        pure msg
+      throwError explanation
 
-The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
-when rewriting.
+/--
+Marks a theorem as a definitional equality under the permissive transparency rules that
+predated the stricter `@[defeq]` inference (i.e. an equality that holds at `.default` or
+`.all` transparency, but possibly not at `.instances` transparency as required by `dsimp`).
 
-A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
-To avoid this behavior, write `:= (rfl)` instead.
+Such theorems are inferred automatically by `inferDefEqAttr`: any theorem that the old
+`:= rfl` inference would have accepted is tagged `@[backward_defeq]`, and additionally
+tagged `@[defeq]` when it also passes the stricter check at instance transparency.
+
+`dsimp` ignores `@[backward_defeq]` theorems by default. Setting
+`set_option backward.defeqAttrib.useBackward true` (typically scoped to a single proof
+with `set_option ... in`) makes `dsimp` treat them like `@[defeq]` theorems, which
+provides a local backwards-compatibility escape hatch for proofs broken by the stricter
+inference.
+-/
+@[builtin_doc]
+builtin_initialize backwardDefeqAttr : TagAttribute ←
+  registerTagAttribute `backward_defeq
+    "mark theorem as a definitional equality under the permissive pre-stricter-inference \
+      rules, used by `dsimp` when `set_option backward.defeqAttrib.useBackward true`"
+    (validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
+    (asyncMode := .async .mainEnv)
+
+/--
+Marks the theorem as a definitional equality that can be used by `dsimp`.
+
+The theorem must be an equality that holds at `.instances` transparency. A theorem
+with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`
+(and also `@[backward_defeq]`, since the latter is a superset); write `:= (rfl)`
+instead to suppress this.
 
 The attribute should be given before a `@[simp]` attribute to have effect.
 
-When using the module system, an exported theorem can only be `@[defeq]` if all definitions that
-need to be unfolded to prove the theorem are exported and exposed.
+When using the module system, an exported theorem can only be `@[defeq]` if all
+definitions that need to be unfolded to prove the theorem are exported and exposed.
+
+Tagging a theorem with `@[defeq]` automatically also tags it with `@[backward_defeq]`,
+maintaining the invariant that `@[defeq]` theorems form a subset of `@[backward_defeq]`
+theorems.
 -/
 @[builtin_doc]
 builtin_initialize defeqAttr : TagAttribute ←
   registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`"
-    (validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
+    (validate := fun declName => do
+      -- Validate via the same check as `@[backward_defeq]`, then maintain the invariant
+      -- `defeq ⊆ backward_defeq` by also tagging `backward_defeq`.
+      validateDefEqAttr declName
+      backwardDefeqAttr.setTag declName)
+    (applicationTime := .afterTypeChecking)
     (asyncMode := .async .mainEnv)
 
 private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
@@ -85,17 +133,28 @@ private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool :=
         -- `Eq.symm` of rfl proof is a rfl proof
         isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
       else if proof.getAppFn.isConst then
-        -- The application of a `defeq` theorem is a `rfl` proof
-        return defeqAttr.hasTag (← getEnv) proof.getAppFn.constName!
+        -- The application of a `defeq` or `backward_defeq` theorem is a `rfl` proof
+        let env ← getEnv
+        let c := proof.getAppFn.constName!
+        return defeqAttr.hasTag env c || backwardDefeqAttr.hasTag env c
       else
         return false
     else
       return false
 
 /--
-For automatically generated theorems (equational theorems etc.), we want to set the `defeq` attribute
-if the proof is `rfl`, essentially reproducing the behavior before the introduction of the `defeq`
-attribute. This function infers the `defeq` attribute based on the declaration value.
+For automatically generated theorems (equational theorems etc.), we tag the theorem with
+the `defeq`/`backward_defeq` attributes based on its `rfl` proof:
+
+* If the equation holds at `.instances` transparency (matching the transparency at which
+  `dsimp` operates), we tag it with `@[defeq]`.
+* Independently, if the equation holds under the more permissive legacy check (equivalent
+  to `validateDefEqAttr`, i.e. at `.default` or `.all` transparency), we tag it with
+  `@[backward_defeq]`.
+
+In particular, every theorem that would have been tagged `@[defeq]` before the stricter
+inference rules were introduced is now tagged `@[backward_defeq]`. Local backwards
+compatibility can be restored with `set_option backward.defeqAttrib.useBackward true`.
 -/
 def inferDefEqAttr (declName : Name) : MetaM Unit := do
   withoutExporting do
@@ -105,11 +164,25 @@ def inferDefEqAttr (declName : Name) : MetaM Unit := do
         isRflProofCore info.type value
       else
         pure false
-    if isRfl then
-      try
-        withExporting (isExporting := !isPrivateName declName) do
-          validateDefEqAttr declName -- sanity-check: would we have accepted `@[defeq]` on this?
-      catch e =>
-        logError m!"Theorem {declName} has a `rfl`-proof and was thus inferred to be `@[defeq]`, \
-          but validating that attribute failed:{indentD e.toMessageData}"
+    unless isRfl do return
+    -- Strict check: defeq at instance transparency (as used by `dsimp`).
+    let strict ← withEqLhsRhs info.type fun lhs rhs =>
+      withReducibleAndInstances (isDefEq lhs rhs)
+    -- Sanity-check: is the theorem also defeq at the permissive (`.default`/`.all`)
+    -- transparency we use for `@[backward_defeq]`? If not, log the error that the
+    -- legacy inference would have emitted — but still proceed to tag
+    -- `@[backward_defeq]` unconditionally. The legacy (pre-PR) behavior tagged
+    -- `@[defeq]` unconditionally whenever `isRflProofCore` returned true,
+    -- regardless of whether the validation check passed, and we want to preserve
+    -- exactly that set under `backward_defeq` so that `useBackward=true` reliably
+    -- restores the old behavior.
+    try
+      withExporting (isExporting := !isPrivateName declName) do
+        validateDefEqAttr declName
+    catch e =>
+      unless strict do
+        logError m!"Theorem {declName} has a `rfl`-proof but could not be validated \
+          as a definitional equality:{indentD e.toMessageData}"
+    if strict then
       defeqAttr.setTag declName
+    backwardDefeqAttr.setTag declName
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 8c546ac9a9..7ec7114efa 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -129,7 +129,9 @@ structure DefView where
 def DefView.isInstance (view : DefView) : Bool :=
   view.modifiers.attrs.any fun attr => attr.name == `instance
 
-/-- Prepends the `defeq` attribute, removing existing ones if there are any -/
+/-- Prepends the `defeq` attribute, removing existing ones if there are any.
+The `defeq` attribute's validator also tags `backward_defeq` on success, so the
+superset invariant `defeq ⊆ backward_defeq` is preserved. -/
 def DefView.markDefEq (view : DefView) : DefView :=
   { view with modifiers :=
       view.modifiers.filterAttrs (·.name != `defeq) |>.addFirstAttr { name := `defeq } }
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index d9743c9911..3572cc8c8d 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -37,6 +37,8 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
 
   if defeqAttr.hasTag (← getEnv) id then
     attrs := attrs.push m!"defeq"
+  else if backwardDefeqAttr.hasTag (← getEnv) id then
+    attrs := attrs.push m!"backward_defeq"
 
   let mut m : MessageData := m!""
   unless attrs.isEmpty do
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 2233a6ec76..91d528caae 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -40,7 +40,8 @@ value at definition time, not realization time, should matter.
 This is implemented by storing their values at definition time (when non-default) in an environment
 extension, and restoring them when the equations are lazily realized.
 -/
-def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
+def eqnAffectingOptions : Array (Lean.Option Bool) :=
+  #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit, backward.defeqAttrib.useBackward]
 
 /-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
 keyed by declaration name. Only populated when at least one option has a non-default value.
diff --git a/src/Lean/Meta/Tactic/AuxLemma.lean b/src/Lean/Meta/Tactic/AuxLemma.lean
index 4bebeb31e0..fc8a5bf2eb 100644
--- a/src/Lean/Meta/Tactic/AuxLemma.lean
+++ b/src/Lean/Meta/Tactic/AuxLemma.lean
@@ -18,6 +18,8 @@ structure AuxLemmaKey where
   -- When an aux lemma is created in a private context and thus has a private name, we must not
   -- reuse it in an exported context.
   isPrivate : Bool
+  -- Whether the theorem should be tagged with `[defeq]` (needs to happen before caching)
+  defeq : Bool
 deriving BEq, Hashable
 
 structure AuxLemmas where
@@ -39,10 +41,10 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
   users. For example, `simp` preprocessor may convert a lemma into multiple ones.
 -/
 def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none)
-    (cache := true) (inferRfl := false) (forceExpose := false) : MetaM Name := do
+    (cache := true) (inferRfl := false) (forceExpose := false) (defeq := false) : MetaM Name := do
   let env ← getEnv
   let s := auxLemmasExt.getState env
-  let key := { type, isPrivate := !env.isExporting }
+  let key := { type, isPrivate := !env.isExporting, defeq }
   let mkNewAuxLemma := do
     let auxName ← mkAuxDeclName (kind := kind?.getD `_proof)
     let decl :=
@@ -60,6 +62,7 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
           levelParams, type, value
         }
     addDecl (forceExpose := forceExpose) decl
+    if defeq then defeqAttr.setTag auxName
     if inferRfl then
       inferDefEqAttr auxName
     modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert key (auxName, levelParams)⟩
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 1ef7505199..14b4ab958f 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -107,7 +107,7 @@ where
       return false
 
 private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
-  if thm.rfl then
+  if thm.rfl || (thm.backwardRfl && backward.defeqAttrib.useBackward.get (← getOptions)) then
     return (← getConfig).implicitDefEqProofs
   else
     return false
@@ -218,11 +218,12 @@ where
       return none
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
+      let useBackward := backward.defeqAttrib.useBackward.get (← getOptions)
       for (thm, numExtraArgs) in candidates do
         checkSystem "simp"
         if inErasedSet thm then continue
         if rflOnly then
-          unless thm.rfl do
+          unless thm.rfl || (useBackward && thm.backwardRfl) do
             if debug.tactic.simp.checkDefEqAttr.get (← getOptions) &&
                backward.dsimp.useDefEqAttr.get (← getOptions) then
               let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do
@@ -246,9 +247,10 @@ where
       return none
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
+      let useBackward := backward.defeqAttrib.useBackward.get (← getOptions)
       for thm in candidates do
         checkSystem "simp"
-        unless inErasedSet thm || (rflOnly && !thm.rfl) do
+        unless inErasedSet thm || (rflOnly && !(thm.rfl || (useBackward && thm.backwardRfl))) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue
             let type ← inferType val
@@ -360,7 +362,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
 def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
   for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq), backwardRfl := (← isBackwardRflTheorem matchEq) }) with
     | none   => pure ()
     | some r => return .visit r
   return .continue
@@ -441,7 +443,7 @@ def sevalGround : Simproc := fun e => do
     -- `declName` has equation theorems associated with it.
     for eqn in eqns do
       -- TODO: cache SimpTheorem to avoid calls to `isRflTheorem`
-      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then
+      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn), backwardRfl := (← isBackwardRflTheorem eqn) } then
         trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}"
         return .visit result
     return .continue
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 2fd9503ea2..e042c84c00 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -174,14 +174,20 @@ structure SimpTheorem where
   `rfl` is true if `proof` is by `Eq.refl`, `rfl` or a `@[defeq]` theorem.
   -/
   rfl         : Bool
+  /--
+  `backwardRfl` is true if `proof` is by a `@[backward_defeq]` theorem (i.e. rfl at default,
+  but not instance, transparency). Honored by `dsimp` only when
+  `backward.defeqAttrib.useBackward` is set.
+  -/
+  backwardRfl : Bool := false
   deriving Inhabited
 
 mutual
-  private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+  private partial def isRflProofCore (includeBackward : Bool) (type : Expr) (proof : Expr) : CoreM Bool := do
     match type with
     | .forallE _ _ type _ =>
       if let .lam _ _ proof _ := proof then
-        isRflProofCore type proof
+        isRflProofCore includeBackward type proof
       else
         return false
     | _ =>
@@ -190,23 +196,25 @@ mutual
           return true
         else if proof.isAppOfArity ``Eq.symm 4 then
           -- `Eq.symm` of rfl theorem is a rfl theorem
-          isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
+          isRflProofCore includeBackward type proof.appArg! -- small hack: we don't need to set the exact type
         else if proof.getAppFn.isConst then
           -- The application of a `rfl` theorem is a `rfl` theorem
           -- A constant which is a `rfl` theorem is a `rfl` theorem
-          isRflTheoremCore proof.getAppFn.constName!
+          isRflTheoremCore includeBackward proof.getAppFn.constName!
         else
           return false
       else
         return false
 
-  private partial def isRflTheoremCore (declName : Name) : CoreM Bool := do
+  private partial def isRflTheoremCore (includeBackward : Bool) (declName : Name) : CoreM Bool := do
     if backward.dsimp.useDefEqAttr.get (← getOptions) then
-      return defeqAttr.hasTag (← getEnv) declName
+      let env ← getEnv
+      return defeqAttr.hasTag env declName ||
+        (includeBackward && backwardDefeqAttr.hasTag env declName)
     else
       let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
       let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
-      isRflProofCore info.type info.value
+      isRflProofCore includeBackward info.type info.value
 end
 
 def isRflTheorem (declName : Name) : CoreM Bool :=
@@ -214,7 +222,12 @@ def isRflTheorem (declName : Name) : CoreM Bool :=
   -- for the ultimate application of a rfl theorem, only that the theorem type's LHS and RHS are
   -- defeq.
   withoutExporting do
-    isRflTheoremCore declName
+    isRflTheoremCore (includeBackward := false) declName
+
+/-- Like `isRflTheorem`, but also returns `true` for `@[backward_defeq]` theorems. -/
+def isBackwardRflTheorem (declName : Name) : CoreM Bool :=
+  withoutExporting do
+    isRflTheoremCore (includeBackward := true) declName
 
 def isRflProof (proof : Expr) : MetaM Bool := do
   -- Make theorem body available if `declName` is from the current module; the body does not matter
@@ -222,9 +235,18 @@ def isRflProof (proof : Expr) : MetaM Bool := do
   -- defeq.
   withoutExporting do
     if let .const declName .. := proof then
-      isRflTheoremCore declName
+      isRflTheoremCore (includeBackward := false) declName
     else
-      isRflProofCore (← inferType proof) proof
+      isRflProofCore (includeBackward := false) (← inferType proof) proof
+
+/-- Like `isRflProof`, but also returns `true` for proofs that are rfl only at default
+transparency (via `@[backward_defeq]`). -/
+def isBackwardRflProof (proof : Expr) : MetaM Bool := do
+  withoutExporting do
+    if let .const declName .. := proof then
+      isRflTheoremCore (includeBackward := true) declName
+    else
+      isRflProofCore (includeBackward := true) (← inferType proof) proof
 
 instance : ToFormat SimpTheorem where
   format s :=
@@ -405,6 +427,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
   let type ← instantiateMVars (← inferType e)
   let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs checkLhs
   let rfl ← isRflProof proof
+  let backwardRfl ← if rfl then pure true else isBackwardRflProof proof
   if rfl && simp.rfl.checkTransparency.get (← getOptions) then
     forallTelescopeReducing type fun _ type => do
       let checkDefEq (lhs rhs : Expr) := do
@@ -419,7 +442,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
       | Iff lhs rhs => checkDefEq lhs rhs
       | _ =>
         logWarning m!"'{origin.key}' is a 'rfl' simp theorem, unexpected resulting type{indentExpr type}"
-  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl }
+  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl, backwardRfl }
 
 /--
 Creates a `SimpTheorem` from a global theorem.
@@ -440,6 +463,8 @@ def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
         let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true)
           (forceExpose := true)  -- These kinds of theorems are small and `to_additive` may need to
                                  -- unfold them.
+          -- The `[defeq]` attribute transfers (should only matter for `[← thm]`)
+          (defeq := inv && defeqAttr.hasTag (← getEnv) declName)
         r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs))
       return r
     else
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 336e2676db..926a29ced1 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -57,6 +57,7 @@ where
         origin := .decl matchEqDeclName
         proof := mkConst matchEqDeclName
         rfl := (← isRflTheorem matchEqDeclName)
+        backwardRfl := (← isBackwardRflTheorem matchEqDeclName)
       }
       match (← withReducible <| Simp.tryTheorem? e simpTheorem) with
       | none => return .continue
diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index 6bcd842f09..e7beb248d5 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -23,7 +23,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm), backwardRfl := (← isBackwardRflTheorem unfoldThm) }) with
     | none   => pure ()
     | some r => match (← reduceMatcher? r.expr) with
       | .reduced e' => return .done { r with expr := e' }
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index 9ea6577b8f..5739c4b108 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -538,10 +538,10 @@ theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (
 
 theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
     (f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f := by
-    dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
+    simp only [alter, alterₘ, containsₘ, ← bucket_eq]
     split
     · congr 2
-      · simp only [withComputedSize, bucket_updateBucket]
+      · simp only [withComputedSize, bucket_updateBucket, AssocList.contains_eq]
       · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
     · congr
 
@@ -568,10 +568,10 @@ variable {β : Type v}
 
 theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
     (f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f := by
-    dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
+    simp only [alter, alterₘ, containsₘ, ← bucket_eq]
     split
     · congr 2
-      · simp only [withComputedSize, bucket_updateBucket]
+      · simp only [withComputedSize, bucket_updateBucket, AssocList.contains_eq]
       · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
     · congr
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e444447049..f7585a448b 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// please update stage0
 #include "util/options.h"
 
 namespace lean {
diff --git a/tests/elab/5667.lean b/tests/elab/5667.lean
index cbc88450a7..78cbc1663c 100644
--- a/tests/elab/5667.lean
+++ b/tests/elab/5667.lean
@@ -24,7 +24,7 @@ info: optimize.eq_def (x✝ : Expr) :
 
 /--
 info: equations:
-@[defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
+@[backward_defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
 theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32),
   optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0)
 theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit),
@@ -44,8 +44,8 @@ def optimize2 : Expr → Expr
 
 /--
 info: equations:
-@[defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
-@[defeq] theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
+@[backward_defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
+@[backward_defeq] theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
   optimize2 (Expr.op bop e1) =
     match optimize2 e1 with
     | Expr.const i => Expr.op bop (Expr.const 0)
@@ -65,8 +65,8 @@ def optimize3 : Expr → Expr
 
 /--
 info: equations:
-@[defeq] theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
-@[defeq] theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32),
+@[backward_defeq] theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
+@[backward_defeq] theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32),
   optimize3 (Expr.op bop (Expr.const i)) = Expr.op bop (optimize3 (Expr.const i))
 theorem optimize3.eq_3 : ∀ (bop : Unit) (e1 : Expr),
   (∀ (i : BitVec 32), e1 = Expr.const i → False) → optimize3 (Expr.op bop e1) = Expr.const 0
diff --git a/tests/elab/6789.lean b/tests/elab/6789.lean
index a0ecc1172e..f6877e71ca 100644
--- a/tests/elab/6789.lean
+++ b/tests/elab/6789.lean
@@ -36,7 +36,7 @@ theorem Extension.recOn'.eq_1.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ
   (zero : {Γ : Con} → motive Γ Γ Extension.zero)
   (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x : Con),
   Extension.recOn' zero succ Extension.zero = zero
-@[defeq] theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v}
+@[backward_defeq] theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v}
   (zero : {Γ : Con} → motive Γ Γ Extension.zero)
   (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x Δ : Con)
   (A : Nat) (xt : Extension x Δ),
@@ -53,10 +53,10 @@ def Extension.pullback_con
 
 /--
 info: equations:
-@[defeq] theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B),
+@[backward_defeq] theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B),
   Extension.zero.pullback_con x = B'
-@[defeq] theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B) (Δ_2 : Con)
-  (xt : Extension B Δ_2) (A : Nat), (xt.succ A).pullback_con x = (xt.pullback_con x).ext A
+@[backward_defeq] theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B)
+  (Δ_2 : Con) (xt : Extension B Δ_2) (A : Nat), (xt.succ A).pullback_con x = (xt.pullback_con x).ext A
 -/
 #guard_msgs in
 #print equations Extension.pullback_con
diff --git a/tests/elab/defeqAttrib.lean b/tests/elab/defeqAttrib.lean
index 6b7289091d..821c294c6e 100644
--- a/tests/elab/defeqAttrib.lean
+++ b/tests/elab/defeqAttrib.lean
@@ -82,8 +82,13 @@ def e3 := a
 -- are transported out
 def f := a
 #guard_msgs in example (h : P a) : P f := by dsimp [f]; exact h
+-- `f.eq_1` etc. are only `[backward_defeq]` (not `[defeq]`) since `f` is semireducible;
+-- so we need to opt into the backward behavior for `dsimp` to use them.
+set_option backward.defeqAttrib.useBackward true in
 #guard_msgs in example (h : P a) : P f := by dsimp [f.eq_1]; exact h
+set_option backward.defeqAttrib.useBackward true in
 #guard_msgs in example (h : P a) : P f := by dsimp [f.eq_def]; exact h
+set_option backward.defeqAttrib.useBackward true in
 #guard_msgs in example (h : P a) : P f := by dsimp [f.eq_unfold]; exact h
 
 
diff --git a/tests/elab/defeqAttribStrictOnly.lean b/tests/elab/defeqAttribStrictOnly.lean
new file mode 100644
index 0000000000..ba2661d0e7
--- /dev/null
+++ b/tests/elab/defeqAttribStrictOnly.lean
@@ -0,0 +1,65 @@
+module
+
+prelude
+
+public import Lean.DefEqAttrib
+import Init.Data.Nat.Basic
+
+/-!
+# Can `@[defeq]` inference have `strict=true` while `validateDefEqAttr` throws?
+
+The algorithm in `inferDefEqAttr` swallows `validateDefEqAttr` errors when
+`strict` passed:
+
+```
+try withExporting ... validateDefEqAttr declName
+catch e =>
+  unless strict do logError m!"..."
+```
+
+This guards a theoretical case where the strict check (`.instances` transparency,
+smart-unfolding ON, under `withoutExporting`) passes but the permissive check
+(`.default`/`.all`, smart-unfolding OFF, under `withExporting` for public decls)
+fails. The two differ along three axes: transparency, export-view, smart-unfolding.
+
+Trying to construct a case:
+
+1. Public `@[reducible] def hidden := 42` + public `theorem h = 42 := rfl`:
+   Both strict and permissive fail. The `@[reducible]` marker apparently attaches
+   to the exported view and does not make `hidden` instance-reducible under
+   `withoutExporting`. Not a counterexample.
+
+2. The same pair as private: strict=true, permissive=true. Both pass.
+
+3. Recursive `@[reducible]` def relying on smart unfolding: same pattern — public
+   fails both, private passes both.
+
+Under the module system, it seems the `withoutExporting` in `inferDefEqAttr` does
+not give the strict check a strictly-bigger view than the permissive check has.
+Every case where strict succeeds, permissive succeeds too. The `unless strict do
+logError` branch is therefore a defensive guard that (as far as this demonstrates)
+is unreachable in practice.
+-/
+
+@[reducible] public def hidden : Nat := 42
+
+-- Public version: error message from `validateDefEqAttr` surfaces via
+-- `unless strict do logError` because strict=false (reducibility of the exported
+-- view is gone under `withoutExporting`).
+/--
+error: Not a definitional equality: the left-hand side
+  hidden
+is not definitionally equal to the right-hand side
+  42
+
+Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
+-/
+#guard_msgs in
+public theorem test_public : hidden = 42 := rfl
+
+-- Private version: both strict and permissive checks pass, tagged `@[defeq]`.
+theorem test_private : hidden = 42 := rfl
+
+/-- info: @[defeq] private theorem test_private : hidden = 42 -/
+#guard_msgs in
+#print sig test_private
diff --git a/tests/elab/dsimp1.lean b/tests/elab/dsimp1.lean
index 99527bb280..4a0ef894db 100644
--- a/tests/elab/dsimp1.lean
+++ b/tests/elab/dsimp1.lean
@@ -27,6 +27,7 @@ trace: x : Nat
 ⊢ P false
 -/
 #guard_msgs in
+set_option backward.defeqAttrib.useBackward true in
 example (x : Nat) : P (id x.succ.succ).isZero := by
   dsimp [Nat.isZero.eq_2]
   trace_state
diff --git a/tests/elab/eqnOptions.lean b/tests/elab/eqnOptions.lean
index a98d4d141b..9436624a1f 100644
--- a/tests/elab/eqnOptions.lean
+++ b/tests/elab/eqnOptions.lean
@@ -8,8 +8,8 @@ def nonrecfun : Bool → Nat
 
 /--
 info: equations:
-@[defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
-@[defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
+@[backward_defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
+@[backward_defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
 -/
 #guard_msgs in
 #print equations nonrecfun
@@ -25,7 +25,7 @@ def nonrecfun : Bool → Nat
 
 /--
 info: equations:
-@[defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
+@[backward_defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
   nonrecfun x =
     match x with
     | false => 0
@@ -47,8 +47,8 @@ set_option backward.eqns.nonrecursive false
 
 /--
 info: equations:
-@[defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
-@[defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
+@[backward_defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
+@[backward_defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
 -/
 #guard_msgs in
 #print equations nonrecfun
diff --git a/tests/elab/issue10651.lean b/tests/elab/issue10651.lean
index ab2d66da80..5808b401ab 100644
--- a/tests/elab/issue10651.lean
+++ b/tests/elab/issue10651.lean
@@ -10,9 +10,9 @@ termination_by x
 
 /--
 info: equations:
-@[defeq] theorem f.eq_1 : f 0 = 1
-@[defeq] theorem f.eq_2 : f 100 = 2
-@[defeq] theorem f.eq_3 : f 1000 = 3
+@[backward_defeq] theorem f.eq_1 : f 0 = 1
+@[backward_defeq] theorem f.eq_2 : f 100 = 2
+@[backward_defeq] theorem f.eq_3 : f 1000 = 3
 theorem f.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → f x_2.succ = f x_2
 -/
 #guard_msgs(pass trace, all) in
@@ -27,9 +27,9 @@ def g (x : Nat) : Nat :=
 
 /--
 info: equations:
-@[defeq] theorem g.eq_1 : g 0 = 1
-@[defeq] theorem g.eq_2 : g 100 = 2
-@[defeq] theorem g.eq_3 : g 1000 = 3
+@[backward_defeq] theorem g.eq_1 : g 0 = 1
+@[backward_defeq] theorem g.eq_2 : g 100 = 2
+@[backward_defeq] theorem g.eq_3 : g 1000 = 3
 theorem g.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → g x_2.succ = x_2
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/elab/issue2962.lean b/tests/elab/issue2962.lean
index 4ed83945aa..9b81e44020 100644
--- a/tests/elab/issue2962.lean
+++ b/tests/elab/issue2962.lean
@@ -12,12 +12,12 @@ def replace (f : N → Option N) (t : N) : N :=
 
 /--
 info: equations:
-@[defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
+@[backward_defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
   replace f N.zero =
     match f N.zero with
     | some u => u
     | none => N.zero
-@[defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
+@[backward_defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
   replace f t'.succ =
     match f t'.succ with
     | some u => u
@@ -36,12 +36,12 @@ def replace2 (f : N → Option N) (t1 t2 : N) : N :=
 
 /--
 info: equations:
-@[defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
+@[backward_defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
   replace2 f t1 N.zero =
     match f t1 with
     | some u => u
     | none => N.zero
-@[defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
+@[backward_defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
   replace2 f t1 t'.succ =
     match f t1 with
     | some u => u
diff --git a/tests/elab/issue6592.lean b/tests/elab/issue6592.lean
index 05ca187c50..07f641bff4 100644
--- a/tests/elab/issue6592.lean
+++ b/tests/elab/issue6592.lean
@@ -99,9 +99,9 @@ def del [Ord α] (d : α) : Raw α → Raw α
 
 /--
 info: equations:
-@[defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
-@[defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (left_1 : Raw α)
-  (data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
+@[backward_defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
+@[backward_defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color)
+  (left_1 : Raw α) (data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
   del d ((left_1.node data Color.black right).node d_1 color (left_3.node data_1 Color.black right_1)) =
     match compare d d_1 with
     | Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) (left_3.node data_1 Color.black right_1)
diff --git a/tests/elab/printEqns.lean b/tests/elab/printEqns.lean
index 68d2dd3a03..151472bf5f 100644
--- a/tests/elab/printEqns.lean
+++ b/tests/elab/printEqns.lean
@@ -1,7 +1,7 @@
 /--
 info: equations:
-@[defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
-@[defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
+@[backward_defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
+@[backward_defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
   (a :: as).append x = a :: as.append x
 -/
 #guard_msgs in
@@ -9,8 +9,8 @@ info: equations:
 
 /--
 info: equations:
-@[defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
-@[defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
+@[backward_defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
+@[backward_defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
   (a :: as).append x = a :: as.append x
 -/
 #guard_msgs in
diff --git a/tests/elab/structuralEqn6.lean b/tests/elab/structuralEqn6.lean
index 1acb9df7b5..0336c5142e 100644
--- a/tests/elab/structuralEqn6.lean
+++ b/tests/elab/structuralEqn6.lean
@@ -10,7 +10,7 @@ where
 
 /--
 info: equations:
-@[defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
+@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
   (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
 -/
@@ -55,10 +55,11 @@ where
 
 /--
 info: equations:
-@[defeq] theorem trailingZeros2.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
+@[backward_defeq] theorem trailingZeros2.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat)
+  (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros2.aux k_2.succ i hi hk_2 acc =
     if h : i % 2 = 0 then trailingZeros2.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
-@[defeq] theorem trailingZeros2.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
+@[backward_defeq] theorem trailingZeros2.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
   trailingZeros2.aux 0 i hi hk_2 acc = acc
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/elab/structuralOverNested.lean b/tests/elab/structuralOverNested.lean
index 6f269537b4..8f439ebbeb 100644
--- a/tests/elab/structuralOverNested.lean
+++ b/tests/elab/structuralOverNested.lean
@@ -31,8 +31,8 @@ def RTree.simple_size : RTree α → Nat
   | .node _x t _ts => 1 + (t true).simple_size + (t false).simple_size
 
 /--
-info: @[defeq] theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α) (_ts : List (RTree α)),
-  (RTree.node _x t _ts).simple_size = 1 + (t true).simple_size + (t false).simple_size :=
+info: @[backward_defeq] theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α)
+  (_ts : List (RTree α)), (RTree.node _x t _ts).simple_size = 1 + (t true).simple_size + (t false).simple_size :=
 fun {α} _x t _ts => Eq.refl (RTree.node _x t _ts).simple_size
 -/
 #guard_msgs in
@@ -51,7 +51,7 @@ def RTree.aux_size : List (RTree α) → Nat
 end
 
 /--
-info: @[defeq] theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)),
+info: @[backward_defeq] theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)),
   RTree.aux_size (t :: ts) = t.size + RTree.aux_size ts :=
 fun {α} t ts => Eq.refl (RTree.aux_size (t :: ts))
 -/
@@ -67,7 +67,7 @@ def RTree.map_aux (f : α → β) : List (RTree α) → List (RTree β)
 end
 
 /--
-info: @[defeq] theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α)
+info: @[backward_defeq] theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α)
   (ts : List (RTree α)), RTree.map_aux f (t :: ts) = RTree.map f t :: RTree.map_aux f ts :=
 fun {α} {β} f t ts => Eq.refl (RTree.map_aux f (t :: ts))
 -/
@@ -95,7 +95,7 @@ def VTree.vec_size : Vec (VTree α true 5) n b → Nat
 end
 
 /--
-info: @[defeq] theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α)
+info: @[backward_defeq] theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α)
   (f : List Bool → List Nat → Vec (VTree α true 5) n_2 b_2),
   (VTree.node b_2 n_2 a f).size = 1 + VTree.vec_size (f [] []) :=
 fun {α} b_2 n_2 a f => Eq.refl (VTree.node b_2 n_2 a f).size
diff --git a/tests/elab/unfoldLemma.lean b/tests/elab/unfoldLemma.lean
index 1a89adc870..bb776df4c9 100644
--- a/tests/elab/unfoldLemma.lean
+++ b/tests/elab/unfoldLemma.lean
@@ -4,8 +4,9 @@ def Option_map (f : α → β) : Option α → Option β
 
 /--
 info: equations:
-@[defeq] theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option_map f none = none
-@[defeq] theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α),
+@[backward_defeq] theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
+  Option_map f none = none
+@[backward_defeq] theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α),
   Option_map f (some x_1) = some (f x_1)
 -/
 #guard_msgs in
diff --git a/tests/elab/wfEqns5.lean b/tests/elab/wfEqns5.lean
index 4248b6a6b1..787ca11d1d 100644
--- a/tests/elab/wfEqns5.lean
+++ b/tests/elab/wfEqns5.lean
@@ -88,9 +88,9 @@ termination_by structural n => n
 
 /--
 info: equations:
-@[defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0
+@[backward_defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0
 theorem Structural.foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
-@[defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
+@[backward_defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 -/
 #guard_msgs in
 #print equations foo
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 7edd9972b6..5f88ffbee0 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -227,19 +227,19 @@ public def f.eq_def := 1
 #guard_msgs in
 public def fexp.eq_def := 1
 
-/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
+/-- info: @[backward_defeq] private theorem f.eq_def : f = 1 -/
 #guard_msgs in #print sig f.eq_def
 
-/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/
+/-- info: @[backward_defeq] private theorem f.eq_unfold : f = 1 -/
 #guard_msgs in #print sig f.eq_unfold
 
-/-- info: @[defeq] theorem fexp.eq_def : fexp = 1 -/
+/-- info: @[backward_defeq] theorem fexp.eq_def : fexp = 1 -/
 #guard_msgs in #print sig fexp.eq_def
 
-/-- info: @[defeq] theorem fexp.eq_unfold : fexp = 1 -/
+/-- info: @[backward_defeq] theorem fexp.eq_unfold : fexp = 1 -/
 #guard_msgs in #print sig fexp.eq_unfold
 
-/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
+/-- info: @[backward_defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
 #guard_msgs in #print sig f_struct.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean
index c453a70f32..8be526b89e 100644
--- a/tests/pkg/module/Module/ImportedAll.lean
+++ b/tests/pkg/module/Module/ImportedAll.lean
@@ -51,13 +51,13 @@ example : P fexp := by dsimp only [fexp_trfl]; exact hP1
 example : P fexp := by dsimp only [fexp_trfl']; exact hP1
 
 
-/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
+/-- info: @[backward_defeq] private theorem f.eq_def : f = 1 -/
 #guard_msgs in #print sig f.eq_def
 
-/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/
+/-- info: @[backward_defeq] private theorem f.eq_unfold : f = 1 -/
 #guard_msgs in #print sig f.eq_unfold
 
-/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
+/-- info: @[backward_defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
 #guard_msgs in #print sig f_struct.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean
index 48bfa62e2b..bad706c389 100644
--- a/tests/pkg/module/Module/NonModule.lean
+++ b/tests/pkg/module/Module/NonModule.lean
@@ -1,13 +1,13 @@
 import Module.Basic
 import Lean
 
-/-- info: @[defeq] theorem f.eq_def : f = 1 -/
+/-- info: @[backward_defeq] theorem f.eq_def : f = 1 -/
 #guard_msgs in #print sig f.eq_def
 
-/-- info: @[defeq] theorem f.eq_unfold : f = 1 -/
+/-- info: @[backward_defeq] theorem f.eq_unfold : f = 1 -/
 #guard_msgs in #print sig f.eq_unfold
 
-/-- info: @[defeq] theorem f_struct.eq_1 : f_struct 0 = 0 -/
+/-- info: @[backward_defeq] theorem f_struct.eq_1 : f_struct 0 = 0 -/
 #guard_msgs in #print sig f_struct.eq_1
 /--
 info: theorem f_struct.eq_def : ∀ (x : Nat),