From 37f10435a93de79922503ea5506a8c414601ba7d Mon Sep 17 00:00:00 2001
From: fiforeach <249703130+fiforeach@users.noreply.github.com>
Date: Mon, 9 Mar 2026 16:12:02 +0100
Subject: [PATCH] fix: make option `linter.unusedSimpArgs` respect `linter.all`
 (#12560)

This PR changes the way the linting for `linter.unusedSimpArgs` gets the
value from the environment. This is achieved by using the appropriate
helper functions defined in `Lean.Linter.Basic`.

The following now compiles without warning

```lean4
set_option linter.all false in
example : True := by simp [False]
```

Fixes #12559
---
 src/Lean/Elab/Tactic/Simp.lean                |  4 +-
 src/Lean/Linter/UnusedSimpArgs.lean           |  2 +-
 tests/elab/1184.lean.out.expected             |  7 --
 tests/elab/12559.lean                         | 43 ++++++++++
 tests/elab/3705.lean.out.expected             | 14 ----
 tests/elab/4947.lean.out.expected             |  7 --
 tests/elab/5755.lean.out.expected             |  7 --
 .../6123_cat_adjunction.lean.out.expected     | 30 -------
 tests/elab/860.lean.out.expected              | 42 ----------
 tests/elab/968.lean.out.expected              | 14 ----
 tests/elab/972.lean.out.expected              | 21 -----
 tests/elab/ac_expr.lean.out.expected          |  7 --
 tests/elab/bv_uninterpreted.lean.out.expected |  7 --
 tests/elab/constProp.lean.out.expected        | 21 -----
 ...eq_some_iff_get_eq_issue.lean.out.expected |  7 --
 tests/elab/funInduction.lean.out.expected     | 21 -----
 .../elab/funinduction_ident.lean.out.expected | 21 -----
 tests/elab/grind_qsort.lean.out.expected      |  7 --
 tests/elab/gring_11543.lean.out.expected      |  7 --
 tests/elab/issue11181.lean.out.expected       | 84 -------------------
 tests/elab/issue7318.lean.out.expected        |  7 --
 ...azyListRotateUnfoldProof.lean.out.expected |  7 --
 tests/elab/lazylistThunk.lean.out.expected    | 14 ----
 tests/elab/mutualDefThms.lean.out.expected    |  7 --
 tests/elab/simpDecide.lean.out.expected       |  7 --
 .../elab/simpDischargeLoop.lean.out.expected  | 14 ----
 tests/elab/simpMatch.lean.out.expected        |  7 --
 tests/elab/simpRwBug.lean.out.expected        |  7 --
 tests/elab/simpStarHyp.lean.out.expected      |  7 --
 tests/elab/splitIssue2.lean.out.expected      |  7 --
 tests/elab/treeNode.lean.out.expected         | 14 ----
 .../wfOverapplicationIssue.lean.out.expected  |  7 --
 32 files changed, 46 insertions(+), 432 deletions(-)
 delete mode 100644 tests/elab/1184.lean.out.expected
 create mode 100644 tests/elab/12559.lean
 delete mode 100644 tests/elab/4947.lean.out.expected
 delete mode 100644 tests/elab/860.lean.out.expected
 delete mode 100644 tests/elab/968.lean.out.expected
 delete mode 100644 tests/elab/972.lean.out.expected
 delete mode 100644 tests/elab/bv_uninterpreted.lean.out.expected
 delete mode 100644 tests/elab/eq_some_iff_get_eq_issue.lean.out.expected
 delete mode 100644 tests/elab/funInduction.lean.out.expected
 delete mode 100644 tests/elab/funinduction_ident.lean.out.expected
 delete mode 100644 tests/elab/issue11181.lean.out.expected
 delete mode 100644 tests/elab/issue7318.lean.out.expected
 delete mode 100644 tests/elab/lazylistThunk.lean.out.expected
 delete mode 100644 tests/elab/mutualDefThms.lean.out.expected
 delete mode 100644 tests/elab/simpDecide.lean.out.expected
 delete mode 100644 tests/elab/simpMatch.lean.out.expected
 delete mode 100644 tests/elab/simpRwBug.lean.out.expected
 delete mode 100644 tests/elab/simpStarHyp.lean.out.expected
 delete mode 100644 tests/elab/treeNode.lean.out.expected
 delete mode 100644 tests/elab/wfOverapplicationIssue.lean.out.expected

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 8ee39cf915..3e6308c7cf 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -690,7 +690,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
       simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx stats.usedTheorems
-  else if linter.unusedSimpArgs.get (← getOptions) then
+  else if Linter.getLinterValue linter.unusedSimpArgs (← Linter.getLinterOptions) then
     withRef stx do
       warnUnusedSimpArgs simpArgs stats.usedTheorems
   return stats.diag
@@ -707,7 +707,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
   | some mvarId => replaceMainGoal [mvarId]
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx stats.usedTheorems
-  else if linter.unusedSimpArgs.get (← getOptions) then
+  else if Linter.getLinterValue linter.unusedSimpArgs (← Linter.getLinterOptions) then
     withRef stx do
       warnUnusedSimpArgs simpArgs stats.usedTheorems
   return stats.diag
diff --git a/src/Lean/Linter/UnusedSimpArgs.lean b/src/Lean/Linter/UnusedSimpArgs.lean
index 442caf3ffe..1c8f04bef6 100644
--- a/src/Lean/Linter/UnusedSimpArgs.lean
+++ b/src/Lean/Linter/UnusedSimpArgs.lean
@@ -42,7 +42,7 @@ private def warnUnused (stx : Syntax) (i : Nat) : CoreM Unit := do
 
 def unusedSimpArgs : Linter where
   run cmdStx := do
-    if !Tactic.linter.unusedSimpArgs.get (← getOptions) then return
+    if !getLinterValue Tactic.linter.unusedSimpArgs (← getLinterOptions) then return
     let some cmdStxRange := cmdStx.getRange?  | return
 
     let infoTrees := (← get).infoState.trees.toArray
diff --git a/tests/elab/1184.lean.out.expected b/tests/elab/1184.lean.out.expected
deleted file mode 100644
index 48847a8981..0000000000
--- a/tests/elab/1184.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-1184.lean:4:30-4:31: warning: This simp argument is unused:
-  h
-
-Hint: Omit it from the simp argument list.
-  simp (disch := assumption) ̵[̵h̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/12559.lean b/tests/elab/12559.lean
new file mode 100644
index 0000000000..7dd8f27e35
--- /dev/null
+++ b/tests/elab/12559.lean
@@ -0,0 +1,43 @@
+/-!
+  # Make `linter.all` option also control the `linter.unusedSimpArgs` linter
+
+  https://github.com/leanprover/lean4/issues/12559 -/
+
+section
+
+set_option linter.unusedSimpArgs true
+
+/--
+warning: This simp argument is unused:
+  False
+
+Hint: Omit it from the simp argument list.
+  simp ̵[̵F̵a̵l̵s̵e̵]̵
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
+-/
+#guard_msgs in
+example : True := by simp [False]
+
+end
+
+section
+
+set_option linter.all true
+
+/--
+warning: This simp argument is unused:
+  False
+
+Hint: Omit it from the simp argument list.
+  simp ̵[̵F̵a̵l̵s̵e̵]̵
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
+-/
+#guard_msgs in
+example : True := by simp [False]
+
+set_option linter.all false in
+example : True := by simp [False]
+
+end
diff --git a/tests/elab/3705.lean.out.expected b/tests/elab/3705.lean.out.expected
index c4b57da547..9088fe3923 100644
--- a/tests/elab/3705.lean.out.expected
+++ b/tests/elab/3705.lean.out.expected
@@ -1,18 +1,4 @@
 3705.lean:17:9-17:29: warning: declaration uses `sorry`
 3705.lean:17:9-17:29: warning: declaration uses `sorry`
 3705.lean:23:0-23:7: warning: declaration uses `sorry`
-3705.lean:27:54-27:62: warning: This simp argument is unused:
-  mul_comm
-
-Hint: Omit it from the simp argument list.
-  simp (config := { failIfUnchanged := false }) only ̵[̵m̵u̵l̵_̵c̵o̵m̵m̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 3705.lean:30:8-30:11: warning: declaration uses `sorry`
-3705.lean:33:13-33:21: warning: This simp argument is unused:
-  mul_comm
-
-Hint: Omit it from the simp argument list.
-  simp only ̵[̵m̵u̵l̵_̵c̵o̵m̵m̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/4947.lean.out.expected b/tests/elab/4947.lean.out.expected
deleted file mode 100644
index 404f88cb0b..0000000000
--- a/tests/elab/4947.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-4947.lean:6:41-6:54: warning: This simp argument is unused:
-  Nat.reducePow
-
-Hint: Omit it from the simp argument list.
-  simp only ̵[̵N̵a̵t̵.̵r̵e̵d̵u̵c̵e̵P̵o̵w̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/5755.lean.out.expected b/tests/elab/5755.lean.out.expected
index 5cab6d9631..9ea9ce60d4 100644
--- a/tests/elab/5755.lean.out.expected
+++ b/tests/elab/5755.lean.out.expected
@@ -1,10 +1,3 @@
 5755.lean:15:8-15:25: warning: declaration uses `sorry`
 5755.lean:25:0-25:7: warning: declaration uses `sorry`
 5755.lean:46:0-46:7: warning: declaration uses `sorry`
-5755.lean:47:8-47:9: warning: This simp argument is unused:
-  f
-
-Hint: Omit it from the simp argument list.
-  simp ̵[̵f̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/6123_cat_adjunction.lean.out.expected b/tests/elab/6123_cat_adjunction.lean.out.expected
index 133bd2f629..e07e74f8a4 100644
--- a/tests/elab/6123_cat_adjunction.lean.out.expected
+++ b/tests/elab/6123_cat_adjunction.lean.out.expected
@@ -11,35 +11,5 @@
 6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
-6123_cat_adjunction.lean:481:67-481:71: warning: This simp argument is unused:
-  of_α
-
-Hint: Omit it from the simp argument list.
-  simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-6123_cat_adjunction.lean:481:73-481:78: warning: This simp argument is unused:
-  id_eq
-
-Hint: Omit it from the simp argument list.
-  simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α,̵ ̵i̵d̵_̵e̵q̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
 6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
-6123_cat_adjunction.lean:496:45-496:49: warning: This simp argument is unused:
-  of_α
-
-Hint: Omit it from the simp argument list.
-  simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
-              Functor.comp_map, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-6123_cat_adjunction.lean:496:51-496:56: warning: This simp argument is unused:
-  id_eq
-
-Hint: Omit it from the simp argument list.
-  simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
-              Functor.comp_map, typeToCat_map, of_α,̵ ̵i̵d̵_̵e̵q̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/860.lean.out.expected b/tests/elab/860.lean.out.expected
deleted file mode 100644
index fb274e1779..0000000000
--- a/tests/elab/860.lean.out.expected
+++ /dev/null
@@ -1,42 +0,0 @@
-860.lean:26:12-26:20: warning: This simp argument is unused:
-  invImage
-
-Hint: Omit it from the simp argument list.
-  simp [i̵n̵v̵Im̵a̵g̵e̵,̵ ̵I̵nvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-860.lean:26:22-26:30: warning: This simp argument is unused:
-  InvImage
-
-Hint: Omit it from the simp argument list.
-  simp [invImage, I̵n̵v̵I̵m̵a̵g̵e̵,̵ ̵Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-860.lean:26:32-26:40: warning: This simp argument is unused:
-  Prod.lex
-
-Hint: Omit it from the simp argument list.
-  simp [invImage, InvImage, P̵r̵o̵d̵.̵l̵e̵x̵,̵ ̵sizeOfWFRel, measure, Nat.lt_wfRel]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-860.lean:26:42-26:53: warning: This simp argument is unused:
-  sizeOfWFRel
-
-Hint: Omit it from the simp argument list.
-  simp [invImage, InvImage, Prod.lex, s̵i̵z̵e̵O̵f̵W̵F̵R̵e̵l̵,̵ ̵measure, Nat.lt_wfRel]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-860.lean:26:55-26:62: warning: This simp argument is unused:
-  measure
-
-Hint: Omit it from the simp argument list.
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, m̵e̵a̵s̵u̵r̵e̵,̵ ̵Nat.lt_wfRel]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-860.lean:26:64-26:76: warning: This simp argument is unused:
-  Nat.lt_wfRel
-
-Hint: Omit it from the simp argument list.
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure,̵ ̵N̵a̵t̵.̵l̵t̵_̵w̵f̵R̵e̵l̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/968.lean.out.expected b/tests/elab/968.lean.out.expected
deleted file mode 100644
index 04a969354d..0000000000
--- a/tests/elab/968.lean.out.expected
+++ /dev/null
@@ -1,14 +0,0 @@
-968.lean:3:39-3:48: warning: This simp argument is unused:
-  and_assoc
-
-Hint: Omit it from the simp argument list.
-  simp only [and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-968.lean:7:39-7:48: warning: This simp argument is unused:
-  and_assoc
-
-Hint: Omit it from the simp argument list.
-  simp only [and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/972.lean.out.expected b/tests/elab/972.lean.out.expected
deleted file mode 100644
index 1867f42e1f..0000000000
--- a/tests/elab/972.lean.out.expected
+++ /dev/null
@@ -1,21 +0,0 @@
-972.lean:19:38-19:47: warning: This simp argument is unused:
-  mul_assoc
-
-Hint: Omit it from the simp argument list.
-  simp only [mul_left_comm, mul_comm,̵ ̵m̵u̵l̵_̵a̵s̵s̵o̵c̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-972.lean:22:28-22:36: warning: This simp argument is unused:
-  mul_comm
-
-Hint: Omit it from the simp argument list.
-  simp only [mul_left_comm, mul_c̵o̵m̵m̵,̵ ̵m̵u̵l̵_̵assoc]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-972.lean:22:38-22:47: warning: This simp argument is unused:
-  mul_assoc
-
-Hint: Omit it from the simp argument list.
-  simp only [mul_left_comm, mul_comm,̵ ̵m̵u̵l̵_̵a̵s̵s̵o̵c̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/ac_expr.lean.out.expected b/tests/elab/ac_expr.lean.out.expected
index cd6ba4163c..4656d4917a 100644
--- a/tests/elab/ac_expr.lean.out.expected
+++ b/tests/elab/ac_expr.lean.out.expected
@@ -1,10 +1,3 @@
-ac_expr.lean:95:16-95:22: warning: This simp argument is unused:
-  denote
-
-Hint: Omit it from the simp argument list.
-  simp [d̵e̵n̵o̵t̵e̵,̵ ̵ih]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 theorem ex₂ : ∀ (x₁ x₂ x₃ x₄ : Nat), x₁ + x₂ + (x₃ + x₄) = x₃ + x₁ + x₂ + x₄ :=
 fun x₁ x₂ x₃ x₄ =>
   Expr.eq_of_sort_flat
diff --git a/tests/elab/bv_uninterpreted.lean.out.expected b/tests/elab/bv_uninterpreted.lean.out.expected
deleted file mode 100644
index f36ed5cd9c..0000000000
--- a/tests/elab/bv_uninterpreted.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-bv_uninterpreted.lean:9:8-9:9: warning: This simp argument is unused:
-  h
-
-Hint: Omit it from the simp argument list.
-  simp ̵[̵h̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/constProp.lean.out.expected b/tests/elab/constProp.lean.out.expected
index 1f220e1919..b7c8655657 100644
--- a/tests/elab/constProp.lean.out.expected
+++ b/tests/elab/constProp.lean.out.expected
@@ -1,24 +1,3 @@
 Val.bool true : Val
 0 : Val
-constProp.lean:389:22-389:25: warning: This simp argument is unused:
-  hnp
-
-Hint: Omit it from the simp argument list.
-  simp [̵h̵n̵p̵]̵ ̵at ih₂
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-constProp.lean:542:8-542:11: warning: This simp argument is unused:
-  hxy
-
-Hint: Omit it from the simp argument list.
-  simp [h̵x̵y̵,̵ ̵Ne.symm hxy] at hf
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-constProp.lean:595:10-595:13: warning: This simp argument is unused:
-  heq
-
-Hint: Omit it from the simp argument list.
-  simp [̵h̵e̵q̵]̵ ̵at ih₄
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 constProp.lean:659:0-659:5: warning: using 'exit' to interrupt Lean
diff --git a/tests/elab/eq_some_iff_get_eq_issue.lean.out.expected b/tests/elab/eq_some_iff_get_eq_issue.lean.out.expected
deleted file mode 100644
index f65527a836..0000000000
--- a/tests/elab/eq_some_iff_get_eq_issue.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-eq_some_iff_get_eq_issue.lean:6:8-6:19: warning: This simp argument is unused:
-  exists_prop
-
-Hint: Omit it from the simp argument list.
-  simp ̵[̵e̵x̵i̵s̵t̵s̵_̵p̵r̵o̵p̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/funInduction.lean.out.expected b/tests/elab/funInduction.lean.out.expected
deleted file mode 100644
index 20d08b8556..0000000000
--- a/tests/elab/funInduction.lean.out.expected
+++ /dev/null
@@ -1,21 +0,0 @@
-funInduction.lean:378:47-378:55: warning: This simp argument is unused:
-  Finn.min
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-funInduction.lean:381:48-381:57: warning: This simp argument is unused:
-  Finn.min'
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-funInduction.lean:384:49-384:59: warning: This simp argument is unused:
-  Finn.min''
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵'̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/funinduction_ident.lean.out.expected b/tests/elab/funinduction_ident.lean.out.expected
deleted file mode 100644
index ad623ac71d..0000000000
--- a/tests/elab/funinduction_ident.lean.out.expected
+++ /dev/null
@@ -1,21 +0,0 @@
-funinduction_ident.lean:312:39-312:47: warning: This simp argument is unused:
-  Finn.min
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-funinduction_ident.lean:315:40-315:49: warning: This simp argument is unused:
-  Finn.min'
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-funinduction_ident.lean:318:41-318:51: warning: This simp argument is unused:
-  Finn.min''
-
-Hint: Omit it from the simp argument list.
-  simp_all [Finn.m̵i̵n̵'̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/grind_qsort.lean.out.expected b/tests/elab/grind_qsort.lean.out.expected
index e1928a2d19..c4bcdc44d0 100644
--- a/tests/elab/grind_qsort.lean.out.expected
+++ b/tests/elab/grind_qsort.lean.out.expected
@@ -18,13 +18,6 @@ Try this:
 grind_qsort.lean:55:8-55:40: warning: declaration uses `sorry`
 grind_qsort.lean:62:8-62:40: warning: declaration uses `sorry`
 grind_qsort.lean:68:8-68:34: warning: declaration uses `sorry`
-grind_qsort.lean:74:39-74:60: warning: This simp argument is unused:
-  List.getElem?_toArray
-
-Hint: Omit it from the simp argument list.
-  simp_all only [perm_iff_toList_perm, L̵i̵s̵t̵.̵g̵e̵t̵E̵l̵e̵m̵?̵_̵t̵o̵A̵r̵r̵a̵y̵,̵ ̵List.extract_toArray, List.extract_eq_take_drop]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 Try these:
   [apply] [grind .] for pattern: [@Perm #7 (@extract _ #6 #3 #2) (@extract _ #5 #3 #2)]
   [apply] [grind =>] for pattern: [@Perm #7 #6 #5, @Perm _ (@extract _ #6 #3 #2) (@extract _ #5 #3 #2)]
diff --git a/tests/elab/gring_11543.lean.out.expected b/tests/elab/gring_11543.lean.out.expected
index 3f5939dac6..f11d5e0063 100644
--- a/tests/elab/gring_11543.lean.out.expected
+++ b/tests/elab/gring_11543.lean.out.expected
@@ -7,10 +7,3 @@ gring_11543.lean:65:9-65:30: warning: declaration uses `sorry`
 gring_11543.lean:74:8-74:20: warning: declaration uses `sorry`
 gring_11543.lean:91:8-91:22: warning: declaration uses `sorry`
 gring_11543.lean:123:8-123:28: warning: declaration uses `sorry`
-gring_11543.lean:173:52-173:66: warning: This simp argument is unused:
-  add_sub_cancel
-
-Hint: Omit it from the simp argument list.
-  simp only [mul_sub_left_distrib, ← add_sub_assoc, a̵d̵d̵_̵s̵u̵b̵_̵c̵a̵n̵c̵e̵l̵,̵ ̵tsub_le_iff_right] at this
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/issue11181.lean.out.expected b/tests/elab/issue11181.lean.out.expected
deleted file mode 100644
index d49356748a..0000000000
--- a/tests/elab/issue11181.lean.out.expected
+++ /dev/null
@@ -1,84 +0,0 @@
-issue11181.lean:6:26-6:35: warning: This simp argument is unused:
-  instXorOp
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, i̵n̵s̵t̵X̵o̵r̵O̵p̵,̵ ̵xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:6:37-6:40: warning: This simp argument is unused:
-  xor
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, x̵o̵r̵,̵ ̵bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:6:42-6:49: warning: This simp argument is unused:
-  bitwise
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, b̵i̵t̵w̵i̵s̵e̵,̵ ̵Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:6:51-6:64: warning: This simp argument is unused:
-  Bool.bne_true
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, B̵o̵o̵l̵.̵b̵n̵e̵_̵t̵r̵u̵e̵,̵ ̵Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:6:66-6:80: warning: This simp argument is unused:
-  Bool.not_false
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, B̵o̵o̵l̵.̵n̵o̵t̵_̵f̵a̵l̵s̵e̵,̵ ̵↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:6:82-6:92: warning: This simp argument is unused:
-  ↓reduceIte
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false,̵ ̵↓̵r̵e̵d̵u̵c̵e̵I̵t̵e̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:24-10:33: warning: This simp argument is unused:
-  instXorOp
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, i̵n̵s̵t̵X̵o̵r̵O̵p̵,̵ ̵xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:35-10:38: warning: This simp argument is unused:
-  xor
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, x̵o̵r̵,̵ ̵bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:40-10:47: warning: This simp argument is unused:
-  bitwise
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, b̵i̵t̵w̵i̵s̵e̵,̵ ̵Bool.bne_true, Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:49-10:62: warning: This simp argument is unused:
-  Bool.bne_true
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, B̵o̵o̵l̵.̵b̵n̵e̵_̵t̵r̵u̵e̵,̵ ̵Bool.not_false, ↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:64-10:78: warning: This simp argument is unused:
-  Bool.not_false
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, B̵o̵o̵l̵.̵n̵o̵t̵_̵f̵a̵l̵s̵e̵,̵ ̵↓reduceIte]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-issue11181.lean:10:80-10:90: warning: This simp argument is unused:
-  ↓reduceIte
-
-Hint: Omit it from the simp argument list.
-  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false,̵ ̵↓̵r̵e̵d̵u̵c̵e̵I̵t̵e̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/issue7318.lean.out.expected b/tests/elab/issue7318.lean.out.expected
deleted file mode 100644
index ec89f463a9..0000000000
--- a/tests/elab/issue7318.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-issue7318.lean:27:38-27:50: warning: This simp argument is unused:
-  Q_of_decide'
-
-Hint: Omit it from the simp argument list.
-  simp (discharger := native_decide) [Q_of_decide'̵,̵ ̵Q̵_̵o̵f̵_̵d̵e̵c̵i̵d̵e̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/lazyListRotateUnfoldProof.lean.out.expected b/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
index 35f439ecbf..c24afa2782 100644
--- a/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
+++ b/tests/elab/lazyListRotateUnfoldProof.lean.out.expected
@@ -1,11 +1,4 @@
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
 lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
-lazyListRotateUnfoldProof.lean:21:44-21:59: warning: This simp argument is unused:
-  LazyList.length
-
-Hint: Omit it from the simp argument list.
-  simp +arith [̵L̵a̵z̵y̵L̵i̵s̵t̵.̵l̵e̵n̵g̵t̵h̵]̵ ̵at h
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 lazyListRotateUnfoldProof.lean:27:8-27:18: warning: declaration uses `sorry`
diff --git a/tests/elab/lazylistThunk.lean.out.expected b/tests/elab/lazylistThunk.lean.out.expected
deleted file mode 100644
index a384a53ab0..0000000000
--- a/tests/elab/lazylistThunk.lean.out.expected
+++ /dev/null
@@ -1,14 +0,0 @@
-lazylistThunk.lean:28:17-28:30: warning: This simp argument is unused:
-  length_toList
-
-Hint: Omit it from the simp argument list.
-  simp ̵[̵l̵e̵n̵g̵t̵h̵_̵t̵o̵L̵i̵s̵t̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-lazylistThunk.lean:41:30-41:50: warning: This simp argument is unused:
-  toList_force_none as
-
-Hint: Omit it from the simp argument list.
-  simp [force,̵ ̵t̵o̵L̵i̵s̵t̵_̵f̵o̵r̵c̵e̵_̵n̵o̵n̵e̵ ̵a̵s̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/mutualDefThms.lean.out.expected b/tests/elab/mutualDefThms.lean.out.expected
deleted file mode 100644
index 2834bd734e..0000000000
--- a/tests/elab/mutualDefThms.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-mutualDefThms.lean:47:74-47:76: warning: This simp argument is unused:
-  ih
-
-Hint: Omit it from the simp argument list.
-  simp +arith [foldl_init x.length, foldl_init (_ + _),̵ ̵i̵h̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/simpDecide.lean.out.expected b/tests/elab/simpDecide.lean.out.expected
deleted file mode 100644
index 9d54bdc769..0000000000
--- a/tests/elab/simpDecide.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-simpDecide.lean:16:44-16:51: warning: This simp argument is unused:
-  fib_two
-
-Hint: Omit it from the simp argument list.
-  simp (config := { decide := true }) only ̵[̵f̵i̵b̵_̵t̵w̵o̵]̵
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/simpDischargeLoop.lean.out.expected b/tests/elab/simpDischargeLoop.lean.out.expected
index feccdff29e..ef9ef74510 100644
--- a/tests/elab/simpDischargeLoop.lean.out.expected
+++ b/tests/elab/simpDischargeLoop.lean.out.expected
@@ -1,15 +1 @@
-simpDischargeLoop.lean:38:12-38:14: warning: This simp argument is unused:
-  ih
-
-Hint: Omit it from the simp argument list.
-  simp [i̵h̵,̵ ̵double]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-simpDischargeLoop.lean:38:16-38:22: warning: This simp argument is unused:
-  double
-
-Hint: Omit it from the simp argument list.
-  simp [ih,̵ ̵d̵o̵u̵b̵l̵e̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 simpDischargeLoop.lean:42:8-42:21: warning: declaration uses `sorry`
diff --git a/tests/elab/simpMatch.lean.out.expected b/tests/elab/simpMatch.lean.out.expected
deleted file mode 100644
index 390c4413d2..0000000000
--- a/tests/elab/simpMatch.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-simpMatch.lean:10:26-10:29: warning: This simp argument is unused:
-  hnp
-
-Hint: Omit it from the simp argument list.
-  simp [̵h̵n̵p̵]̵ ̵at h
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/simpRwBug.lean.out.expected b/tests/elab/simpRwBug.lean.out.expected
deleted file mode 100644
index 50db08aa33..0000000000
--- a/tests/elab/simpRwBug.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-simpRwBug.lean:4:100-4:102: warning: This simp argument is unused:
-  ih
-
-Hint: Omit it from the simp argument list.
-  simp [Nat.add_assoc,̵ ̵i̵h̵]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/simpStarHyp.lean.out.expected b/tests/elab/simpStarHyp.lean.out.expected
deleted file mode 100644
index 027e79b24b..0000000000
--- a/tests/elab/simpStarHyp.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-simpStarHyp.lean:2:12-2:14: warning: This simp argument is unused:
-  h₂
-
-Hint: Omit it from the simp argument list.
-  simp [h₁,̵ ̵h̵₂̵] at h₁ h₂
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/splitIssue2.lean.out.expected b/tests/elab/splitIssue2.lean.out.expected
index 2ba4390273..bf90cc5d22 100644
--- a/tests/elab/splitIssue2.lean.out.expected
+++ b/tests/elab/splitIssue2.lean.out.expected
@@ -11,10 +11,3 @@ splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
 splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
 splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
 splitIssue2.lean:48:0-57:41: warning: declaration uses `sorry`
-splitIssue2.lean:64:20-64:39: warning: This simp argument is unused:
-  Array.length_toList
-
-Hint: Omit it from the simp argument list.
-  simp only [rootD, A̵r̵r̵a̵y̵.̵l̵e̵n̵g̵t̵h̵_̵t̵o̵L̵i̵s̵t̵,̵ ̵parent_lt]
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/treeNode.lean.out.expected b/tests/elab/treeNode.lean.out.expected
deleted file mode 100644
index 89be5dc126..0000000000
--- a/tests/elab/treeNode.lean.out.expected
+++ /dev/null
@@ -1,14 +0,0 @@
-treeNode.lean:35:18-35:30: warning: This simp argument is unused:
-  List.flatten
-
-Hint: Omit it from the simp argument list.
-  simp [̵L̵i̵s̵t̵.̵f̵l̵a̵t̵t̵e̵n̵,̵ ̵n̵u̵m̵N̵a̵m̵e̵s̵L̵s̵t̵]̵[̲n̲u̲m̲N̲a̲m̲e̲s̲L̲s̲t̲]̲
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-treeNode.lean:36:22-36:34: warning: This simp argument is unused:
-  List.flatten
-
-Hint: Omit it from the simp argument list.
-  simp [List.f̵l̵a̵t̵t̵e̵n̵,̵ ̵L̵i̵s̵t̵.̵map, numNamesLst, length_treeToList_eq_numNames c, helper cs']
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
diff --git a/tests/elab/wfOverapplicationIssue.lean.out.expected b/tests/elab/wfOverapplicationIssue.lean.out.expected
deleted file mode 100644
index 3fe1195498..0000000000
--- a/tests/elab/wfOverapplicationIssue.lean.out.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-wfOverapplicationIssue.lean:2:8-2:22: warning: This simp argument is unused:
-  Membership.mem
-
-Hint: Omit it from the simp argument list.
-  simp [M̵e̵m̵b̵e̵r̵s̵h̵i̵p̵.̵m̵e̵m̵,̵ ̵contains, any, Id.run, BEq.beq, anyM] at h
-
-Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`