From 41bd081f61becb7301836e061463183d480bcd33 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 1 May 2026 15:49:06 +0000
Subject: [PATCH 1/5] feat: `deprecated` warnings do not fire inside of
 definitions and theorems marked as `deprecated`

---
 src/Lean/Elab/DeclModifiers.lean            | 11 +++++++++++
 src/Lean/Elab/MutualDef.lean                | 13 +++++++++----
 tests/elab/redundantDeprecatedWarnings.lean | 15 +++++++++++++++
 3 files changed, 35 insertions(+), 4 deletions(-)
 create mode 100644 tests/elab/redundantDeprecatedWarnings.lean

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index ad43c494ee72..3378f10dea0c 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -345,4 +345,15 @@ def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : S
 
 end Methods
 
+namespace Term
+
+@[inline] def withConditionalCheckDeprecated [MonadWithReaderOf Term.Context m]
+    (attrs : Array Attribute) : m α → m α :=
+  if attrs.any (·.name == `deprecated) then
+    withTheReader Term.Context (fun ctx => { ctx with checkDeprecated := false })
+  else
+    id
+
+end Term
+
 end Lean.Elab
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 328d22c79936..47d36f400892 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -253,7 +253,8 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
         withRestoreOrSaveFull reusableResult? none do
         withReuseContext view.headerRef do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
-        withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
+        withConditionalCheckDeprecated view.modifiers.attrs <|
+          withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
             let mut type ← match view.type? with
@@ -528,7 +529,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
     let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
       withReuseContext header.value do
       withTraceNode `Elab.definition.value (fun _ => pure header.declName) do
-      withDeclName header.declName <| withLevelNames header.levelNames do
+      withConditionalCheckDeprecated header.modifiers.attrs <| withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← declValToTerm header.value header.type
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       withLCtx' ((← getLCtx).modifyLocalDecls fun decl => decl.setType decl.type.cleanupAnnotations) do
@@ -669,7 +670,8 @@ private def ExprWithHoles.getHoles (e : ExprWithHoles) : TermElabM (Array MVarId
   let goals ← goals.mapM fun goal => return ((← goal.getDecl).index, goal)
   return goals.insertionSort (·.fst < ·.fst) |>.map (·.snd)
 
-private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (whereFinally : WhereFinallyView) : TermElabM PUnit := do
+private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (whereFinally : WhereFinallyView)
+    (attrs : Array Attribute) : TermElabM PUnit := do
   if whereFinally.isNone then return
   let goals := (← es.mapM fun e => e.getHoles).flatten
 
@@ -689,6 +691,7 @@ private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (
 
   withExporting (isExporting := wasExporting && !isNoLongerExporting) do
   Lean.Elab.Term.TermElabM.run' do
+  Term.withConditionalCheckDeprecated attrs do
   Term.withDeclName name do
   withRef whereFinally.ref do
     unless goals.isEmpty do
@@ -1293,6 +1296,7 @@ where
       async.commitSignature { name := header.declName, levelParams, type }
 
     -- attributes should be applied on the main thread; see below
+    let oldAttrs := header.modifiers.attrs
     let header := { header with modifiers.attrs := #[] }
 
     -- insert a hole for the proof info trees in the main info tree
@@ -1308,6 +1312,7 @@ where
     let act ←
       -- NOTE: We must set the decl name before going async to ensure that the `auxDeclNGen` is
       -- forked correctly.
+      withConditionalCheckDeprecated oldAttrs do
       withDeclName header.declName do
       wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
@@ -1405,7 +1410,7 @@ where
     for header in headers, value in values do
       let whereFinally ← declValToWhereFinally header.value
       let exprsWithHoles := (exprsWithHoles.getD header.declName #[]).push { ref := header.ref, expr := value }
-      fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally
+      fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally header.modifiers.attrs
     -- Compilation should take place without unused section vars, but all section vars should be
     -- present when elaborating documentation.
     let docCtx := (← getLCtx, ← getLocalInstances)
diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean
new file mode 100644
index 000000000000..5f234a7c9c8b
--- /dev/null
+++ b/tests/elab/redundantDeprecatedWarnings.lean
@@ -0,0 +1,15 @@
+set_option trace.Elab true
+set_option linter.deprecated true
+
+def foo (x : Nat) := x + 1
+
+@[deprecated foo (since:="2025-06-23")]
+def baz (x : Nat) := x + 1
+
+@[deprecated foo (since:="2025-06-23")]
+def baz' (x : Nat) := baz x
+
+@[deprecated foo (since:="2025-06-23")]
+theorem quux (x : Nat) : foo x = baz x := by
+  have hyp : baz x = x + 1 := by rfl
+  rw [foo, baz]

From 00cedf667de248d08beaa4cb2f3ee0edc26a6da9 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 1 May 2026 16:07:38 +0000
Subject: [PATCH 2/5] chore: add test cases

---
 src/Lean/Elab/DeclModifiers.lean            |  2 +-
 src/Lean/Elab/MutualDef.lean                |  8 ++---
 tests/elab/redundantDeprecatedWarnings.lean | 36 +++++++++++++++++----
 3 files changed, 34 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 3378f10dea0c..4a88b3ee0078 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -347,7 +347,7 @@ end Methods
 
 namespace Term
 
-@[inline] def withConditionalCheckDeprecated [MonadWithReaderOf Term.Context m]
+@[inline] def withDeprecationContextFromAttrs [MonadWithReaderOf Term.Context m]
     (attrs : Array Attribute) : m α → m α :=
   if attrs.any (·.name == `deprecated) then
     withTheReader Term.Context (fun ctx => { ctx with checkDeprecated := false })
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 47d36f400892..3c90aa20f956 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -253,7 +253,7 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
         withRestoreOrSaveFull reusableResult? none do
         withReuseContext view.headerRef do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
-        withConditionalCheckDeprecated view.modifiers.attrs <|
+        withDeprecationContextFromAttrs view.modifiers.attrs <|
           withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
@@ -529,7 +529,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
     let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
       withReuseContext header.value do
       withTraceNode `Elab.definition.value (fun _ => pure header.declName) do
-      withConditionalCheckDeprecated header.modifiers.attrs <| withDeclName header.declName <| withLevelNames header.levelNames do
+      withDeprecationContextFromAttrs header.modifiers.attrs <| withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← declValToTerm header.value header.type
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       withLCtx' ((← getLCtx).modifyLocalDecls fun decl => decl.setType decl.type.cleanupAnnotations) do
@@ -691,7 +691,7 @@ private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (
 
   withExporting (isExporting := wasExporting && !isNoLongerExporting) do
   Lean.Elab.Term.TermElabM.run' do
-  Term.withConditionalCheckDeprecated attrs do
+  withDeprecationContextFromAttrs attrs do
   Term.withDeclName name do
   withRef whereFinally.ref do
     unless goals.isEmpty do
@@ -1312,7 +1312,7 @@ where
     let act ←
       -- NOTE: We must set the decl name before going async to ensure that the `auxDeclNGen` is
       -- forked correctly.
-      withConditionalCheckDeprecated oldAttrs do
+      withDeprecationContextFromAttrs oldAttrs do
       withDeclName header.declName do
       wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean
index 5f234a7c9c8b..b3cc00c9829b 100644
--- a/tests/elab/redundantDeprecatedWarnings.lean
+++ b/tests/elab/redundantDeprecatedWarnings.lean
@@ -1,15 +1,37 @@
-set_option trace.Elab true
 set_option linter.deprecated true
 
 def foo (x : Nat) := x + 1
 
+theorem bar (x : Nat) : foo x = x + 1 := rfl
+
 @[deprecated foo (since:="2025-06-23")]
 def baz (x : Nat) := x + 1
 
-@[deprecated foo (since:="2025-06-23")]
-def baz' (x : Nat) := baz x
+@[deprecated bar (since:="2025-06-23")]
+theorem qux (x : Nat) : foo x = baz x := rfl
 
-@[deprecated foo (since:="2025-06-23")]
-theorem quux (x : Nat) : foo x = baz x := by
-  have hyp : baz x = x + 1 := by rfl
-  rw [foo, baz]
+@[deprecated bar (since:="2025-06-23")]
+theorem quux (x : Nat) : foo x = x + 1 := by
+  rw [qux x]
+  rfl
+
+inductive Hello : Prop where
+  | mk (n : Nat) : baz n = 7 → Hello
+
+@[deprecated "test" (since:="2025-06-23")]
+inductive Hello2 (h : baz n = 7) where
+
+@[deprecated "test" (since:="2025-06-23")]
+axiom ax : baz n = 7
+
+@[deprecated "test" (since:="2025-06-23")]
+structure MyStruct where
+  n : Nat
+  hp : baz n = 7
+
+@[deprecated "test" (since:="2025-06-23")]
+structure MyStruct2 (n : Nat) (hp : baz n = 7) where
+
+@[deprecated "test" (since:="2025-06-23")]
+def myFun (n : Nat) : Nat := Id.run do
+  return baz n

From 32fe172ad4c4e730ad122e8315ee8fc65d7570d4 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Tue, 5 May 2026 10:33:10 +0000
Subject: [PATCH 3/5] feat: add support for silencing linters in axioms and
 inductives

---
 src/Lean/Elab/Declaration.lean              |  2 +-
 src/Lean/Elab/MutualInductive.lean          |  2 ++
 tests/elab/redundantDeprecatedWarnings.lean | 11 ++++++++++-
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 38ecb9c28550..1034f13fa1a1 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -108,7 +108,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
     addDeclarationRangesForBuiltin declName modifiers.stx stx
     Term.withAutoBoundImplicit do
     Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
-    Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
+    Term.withDeprecationContextFromAttrs modifiers.attrs <| Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
       let type ← Term.elabType typeStx
       Term.synthesizeSyntheticMVarsNoPostponing
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 9ec41f655a08..442a0b794ced 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -1561,6 +1561,7 @@ def updateViewWithFunctorName (view : InductiveView) : InductiveView :=
 private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
   let view0 := elabs[0]!.view
   let ref := view0.ref
+  Term.withDeprecationContextFromAttrs view0.modifiers.attrs <|
   Term.withDeclName view0.declName do withRef ref do
   withExporting (isExporting := !isPrivateName view0.declName) do
     let res ← mkInductiveDecl vars elabs
@@ -1581,6 +1582,7 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS
 private def elabFlatInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM Unit := do
   let view0 := elabs[0]!.view
   let ref := view0.ref
+  Term.withDeprecationContextFromAttrs view0.modifiers.attrs <|
   Term.withDeclName view0.declName do withRef ref do
   withExporting (isExporting := !isPrivateName view0.declName) do
     withElaboratedHeaders vars elabs <| mkInductiveDeclCore (fun context =>
diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean
index b3cc00c9829b..5045694400c1 100644
--- a/tests/elab/redundantDeprecatedWarnings.lean
+++ b/tests/elab/redundantDeprecatedWarnings.lean
@@ -15,11 +15,16 @@ theorem quux (x : Nat) : foo x = x + 1 := by
   rw [qux x]
   rfl
 
+@[deprecated "test" (since:="2025-06-23")]
 inductive Hello : Prop where
   | mk (n : Nat) : baz n = 7 → Hello
 
 @[deprecated "test" (since:="2025-06-23")]
-inductive Hello2 (h : baz n = 7) where
+coinductive Hello2 : Prop where
+  | mk (n : Nat) : baz n = 7 → Hello2
+
+@[deprecated "test" (since:="2025-06-23")]
+inductive Hello3 (h : baz n = 7) where
 
 @[deprecated "test" (since:="2025-06-23")]
 axiom ax : baz n = 7
@@ -35,3 +40,7 @@ structure MyStruct2 (n : Nat) (hp : baz n = 7) where
 @[deprecated "test" (since:="2025-06-23")]
 def myFun (n : Nat) : Nat := Id.run do
   return baz n
+
+@[deprecated "test" (since:="2025-06-23")]
+instance : BEq Nat where
+  beq m n := m == baz n

From 3c0cf9750983be854090023aa43efe895a91face Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Tue, 5 May 2026 12:31:28 +0000
Subject: [PATCH 4/5] chore: fix the mutual recursion case

---
 src/Lean/Elab/MutualInductive.lean          |  8 ++++----
 tests/elab/redundantDeprecatedWarnings.lean | 13 +++++++++++++
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 442a0b794ced..2991bae5f1e6 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -324,7 +324,8 @@ private def elabHeadersAux (views : Array InductiveView) (i : Nat) (acc : Array
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
       let view := views[i]
-      let acc ← withRef view.ref <| Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
+      let acc ← withRef view.ref <| Term.withDeprecationContextFromAttrs view.modifiers.attrs <|
+          Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
         let (type, _) ← Term.withAutoBoundImplicit do
           let typeStx ← view.type?.getDM `(Sort _)
           let type ← Term.elabType typeStx
@@ -1458,7 +1459,8 @@ private def mkInductiveDeclCore
     for h : i in *...views.size do
       Term.addLocalVarInfo views[i].declId indFVars[i]!
       let r     := rs[i]!
-      let elab' ← elabs[i]!.elabCtors rs r params
+      let elab' ← Term.withDeprecationContextFromAttrs views[i].modifiers.attrs <|
+        elabs[i]!.elabCtors rs r params
       elabs'    := elabs'.push elab'
       indTypesArray := indTypesArray.push { name := r.view.declName, type := r.type, ctors := elab'.ctors }
     Term.synthesizeSyntheticMVarsNoPostponing
@@ -1561,7 +1563,6 @@ def updateViewWithFunctorName (view : InductiveView) : InductiveView :=
 private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
   let view0 := elabs[0]!.view
   let ref := view0.ref
-  Term.withDeprecationContextFromAttrs view0.modifiers.attrs <|
   Term.withDeclName view0.declName do withRef ref do
   withExporting (isExporting := !isPrivateName view0.declName) do
     let res ← mkInductiveDecl vars elabs
@@ -1582,7 +1583,6 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS
 private def elabFlatInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM Unit := do
   let view0 := elabs[0]!.view
   let ref := view0.ref
-  Term.withDeprecationContextFromAttrs view0.modifiers.attrs <|
   Term.withDeclName view0.declName do withRef ref do
   withExporting (isExporting := !isPrivateName view0.declName) do
     withElaboratedHeaders vars elabs <| mkInductiveDeclCore (fun context =>
diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean
index 5045694400c1..f8981547d114 100644
--- a/tests/elab/redundantDeprecatedWarnings.lean
+++ b/tests/elab/redundantDeprecatedWarnings.lean
@@ -7,6 +7,9 @@ theorem bar (x : Nat) : foo x = x + 1 := rfl
 @[deprecated foo (since:="2025-06-23")]
 def baz (x : Nat) := x + 1
 
+@[deprecated foo (since:="2025-06-23")]
+def baz2 (x : Nat) := x + 1
+
 @[deprecated bar (since:="2025-06-23")]
 theorem qux (x : Nat) : foo x = baz x := rfl
 
@@ -44,3 +47,13 @@ def myFun (n : Nat) : Nat := Id.run do
 @[deprecated "test" (since:="2025-06-23")]
 instance : BEq Nat where
   beq m n := m == baz n
+
+/-- warning: `baz` has been deprecated: Use `foo` instead -/
+#guard_msgs in
+mutual
+  inductive NotDep : Prop where
+    | mk : baz 0 = 0 → NotDep → DepInd → NotDep
+  @[deprecated "test" (since:="2025-06-23")]
+  inductive DepInd : Prop where
+    | mk : baz2 0 = 0 → NotDep → DepInd → DepInd
+end

From 4acfd5c881f19675ec69506086e2887fab691d0f Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Tue, 5 May 2026 13:11:26 +0000
Subject: [PATCH 5/5] chore: add comments and minor refactor

---
 src/Lean/Elab/DeclModifiers.lean            | 14 ++++++++++----
 src/Lean/Elab/MutualDef.lean                | 10 ++++++----
 tests/elab/redundantDeprecatedWarnings.lean |  5 ++++-
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 4a88b3ee0078..465e302d0caf 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -347,12 +347,18 @@ end Methods
 
 namespace Term
 
+/--
+If `attrs` contains an `@[deprecated]` attribute, runs the action with `Term.Context.checkDeprecated`
+disabled, suppressing the `linter.deprecated` warning that would otherwise fire when a deprecated
+constant is referenced. Otherwise, runs the action unchanged.
+
+This implements the suppression rule from RFC #8942: deprecation warnings should not fire inside
+the body of a declaration that is itself marked `@[deprecated]`, since the references will go away
+along with the declaration.
+-/
 @[inline] def withDeprecationContextFromAttrs [MonadWithReaderOf Term.Context m]
     (attrs : Array Attribute) : m α → m α :=
-  if attrs.any (·.name == `deprecated) then
-    withTheReader Term.Context (fun ctx => { ctx with checkDeprecated := false })
-  else
-    id
+  if attrs.any (·.name == `deprecated) then withoutCheckDeprecated else id
 
 end Term
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 3c90aa20f956..e5ff695706fd 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -252,9 +252,9 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
         withTraceNode `Elab.definition.header (fun _ => pure declName) do
         withRestoreOrSaveFull reusableResult? none do
         withReuseContext view.headerRef do
+        withDeprecationContextFromAttrs view.modifiers.attrs do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
-        withDeprecationContextFromAttrs view.modifiers.attrs <|
-          withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
+        withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
             let mut type ← match view.type? with
@@ -1296,6 +1296,7 @@ where
       async.commitSignature { name := header.declName, levelParams, type }
 
     -- attributes should be applied on the main thread; see below
+    -- save before clearing so the deprecation-silencing wrap below can still see `@[deprecated]`
     let oldAttrs := header.modifiers.attrs
     let header := { header with modifiers.attrs := #[] }
 
@@ -1334,8 +1335,9 @@ where
     Core.logSnapshotTask { stx? := none, cancelTk? := none, task := (← getEnv).checked.map fun _ =>
       default
     }
-    applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
-    applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
+    withDeprecationContextFromAttrs view.modifiers.attrs do
+      applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
+      applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
   finishElab headers := withFunLocalDecls headers fun funFVars => do
     let env ← getEnv
     let inExposeSection := sc.attrs.any (· matches `(attrInstance| expose))
diff --git a/tests/elab/redundantDeprecatedWarnings.lean b/tests/elab/redundantDeprecatedWarnings.lean
index f8981547d114..d16f7ede570b 100644
--- a/tests/elab/redundantDeprecatedWarnings.lean
+++ b/tests/elab/redundantDeprecatedWarnings.lean
@@ -10,7 +10,7 @@ def baz (x : Nat) := x + 1
 @[deprecated foo (since:="2025-06-23")]
 def baz2 (x : Nat) := x + 1
 
-@[deprecated bar (since:="2025-06-23")]
+@[simp,deprecated bar (since:="2025-06-23")]
 theorem qux (x : Nat) : foo x = baz x := rfl
 
 @[deprecated bar (since:="2025-06-23")]
@@ -18,6 +18,9 @@ theorem quux (x : Nat) : foo x = x + 1 := by
   rw [qux x]
   rfl
 
+@[simp, deprecated bar (since:="2025-06-23")]
+theorem qux2 (x : Nat) : foo x = baz x := rfl
+
 @[deprecated "test" (since:="2025-06-23")]
 inductive Hello : Prop where
   | mk (n : Nat) : baz n = 7 → Hello