From 3461abee61ad2865c7de9ef45ece704a9daf47f9 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Sat, 19 Oct 2024 20:28:48 +0200
Subject: [PATCH] Fixup

---
 Mathlib/Computability/Halting.lean                | 2 +-
 Mathlib/Computability/TuringMachine.lean          | 6 +++---
 Mathlib/Data/Fintype/Card.lean                    | 6 +++---
 Mathlib/Data/MLList/Split.lean                    | 2 +-
 Mathlib/Logic/Basic.lean                          | 6 +++---
 Mathlib/Logic/Encodable/Basic.lean                | 4 ++--
 Mathlib/Order/Heyting/Regular.lean                | 2 +-
 Mathlib/Tactic/Linter/UnusedAssumptionInType.lean | 2 +-
 8 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean
index b6bef6e0f7adb..4c9ebd13c4791 100644
--- a/Mathlib/Computability/Halting.lean
+++ b/Mathlib/Computability/Halting.lean
@@ -236,7 +236,7 @@ theorem halting_problem (n) : ¬ComputablePred fun c => (eval c n).Dom
 -- Post's theorem on the equivalence of r.e., co-r.e. sets and
 -- computable sets. The assumption that p is decidable is required
 -- unless we assume Markov's principle or LEM.
-@[nolint decidableClassical]
+@[nolint allOfThem]
 theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
     ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a :=
   ⟨fun h => ⟨h.to_re, h.not.to_re⟩, fun ⟨h₁, h₂⟩ =>
diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index ba8d701772f64..88c93f4dc0986 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -925,7 +925,7 @@ instance Stmt.inhabited [Inhabited Γ] : Inhabited Stmt₀ :=
   Both `Λ` and `Γ` are required to be inhabited; the default value
   for `Γ` is the "blank" tape value, and the default value of `Λ` is
   the initial state. -/
-@[nolint inhabitedNonempty unusedArguments] -- this is a deliberate addition, see comment
+@[nolint allOfThem unusedArguments] -- this is a deliberate addition, see comment
 def Machine [Inhabited Λ] :=
   Λ → Γ → Option (Λ × Stmt₀)
 
@@ -1019,7 +1019,7 @@ variable (M : Machine Γ Λ) (f₁ : PointedMap Γ Γ') (f₂ : PointedMap Γ' 
 /-- Because the state transition function uses the alphabet and machine states in both the input
 and output, to map a machine from one alphabet and machine state space to another we need functions
 in both directions, essentially an `Equiv` without the laws. -/
-@[nolint inhabitedNonempty]
+@[nolint allOfThem ]
 def Machine.map : Machine Γ' Λ'
   | q, l => (M (g₂ q) (f₂ l)).map (Prod.map g₁ (Stmt.map f₁))
 
@@ -1329,7 +1329,7 @@ def trAux (s : Γ) : Stmt₁ → σ → Λ'₁₀ × Stmt₀
 local notation "Cfg₁₀" => TM0.Cfg Γ Λ'₁₀
 
 /-- The translated TM0 machine (given the TM1 machine input). -/
-@[nolint inhabitedNonempty]
+@[nolint allOfThem ]
 def tr : TM0.Machine Γ Λ'₁₀
   | (none, _), _ => none
   | (some q, v), s => some (trAux M s q v)
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index cfc10a97f749a..bb1b15cb66ce4 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -373,13 +373,13 @@ In this section we prove that `α : Type*` is `Finite` if and only if `Fintype 
 -/
 
 
-@[nolint finiteFintype]
+@[nolint allOfThem]
 protected theorem Fintype.finite {α : Type*} (_inst : Fintype α) : Finite α :=
   ⟨Fintype.equivFin α⟩
 
 /-- For efficiency reasons, we want `Finite` instances to have higher
 priority than ones coming from `Fintype` instances. -/
-@[nolint finiteFintype]
+@[nolint allOfThem]
 instance (priority := 900) Finite.of_fintype (α : Type*) [Fintype α] : Finite α :=
   Fintype.finite ‹_›
 
@@ -838,7 +838,7 @@ instance (priority := 10) LinearOrder.isWellOrder_gt [LinearOrder α] : IsWellOr
 
 end Finite
 
-@[nolint finiteFintype]
+@[nolint allOfThem]
 protected theorem Fintype.false [Infinite α] (_h : Fintype α) : False :=
   not_finite α
 
diff --git a/Mathlib/Data/MLList/Split.lean b/Mathlib/Data/MLList/Split.lean
index caad6d95d63f7..7c3ea5f917474 100644
--- a/Mathlib/Data/MLList/Split.lean
+++ b/Mathlib/Data/MLList/Split.lean
@@ -83,7 +83,7 @@ Return a lazy lists of pairs, consisting of a value under that function,
 and a maximal list of elements having that value.
 -/
 @[deprecated "See deprecation note in module documentation." (since := "2024-08-22"),
-  nolint decidableClassical]
+  nolint allOfThem]
 partial def groupByM [DecidableEq β] (L : MLList m α) (f : α → m β) : MLList m (β × List α) :=
   L.cases (fun _ => nil) fun a t => squash fun _ => do
     let b ← f a
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index ffaccd97d010a..342531d7c2956 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -151,10 +151,10 @@ protected theorem Function.mt {a b : Prop} : (a → b) → ¬b → ¬a := mt
 
 /-! ### Declarations about `not` -/
 
-@[nolint decidableClassical]
+@[nolint allOfThem]
 alias dec_em := Decidable.em
 
-@[nolint decidableClassical]
+@[nolint allOfThem]
 theorem dec_em' (p : Prop) [Decidable p] : ¬p ∨ p := (dec_em p).symm
 
 alias em := Classical.em
@@ -211,7 +211,7 @@ theorem not_ne_iff {α : Sort*} {a b : α} : ¬a ≠ b ↔ a = b := not_not
 
 theorem of_not_imp : ¬(a → b) → a := Decidable.of_not_imp
 
-@[nolint decidableClassical]
+@[nolint allOfThem]
 alias Not.decidable_imp_symm := Decidable.not_imp_symm
 
 theorem Not.imp_symm : (¬a → b) → ¬b → a := Not.decidable_imp_symm
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index bb21fb68a7e19..4ab86b475a46f 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -507,13 +507,13 @@ theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
 end FindA
 
 /-- A constructive version of `Classical.axiom_of_choice` for `Encodable` types. -/
-@[nolint decidableClassical]
+@[nolint allOfThem]
 theorem axiom_of_choice {α : Type*} {β : α → Type*} {R : ∀ x, β x → Prop} [∀ a, Encodable (β a)]
     [∀ x y, Decidable (R x y)] (H : ∀ x, ∃ y, R x y) : ∃ f : ∀ a, β a, ∀ x, R x (f x) :=
   ⟨fun x => choose (H x), fun x => choose_spec (H x)⟩
 
 /-- A constructive version of `Classical.skolem` for `Encodable` types. -/
-@[nolint decidableClassical]
+@[nolint allOfThem]
 theorem skolem {α : Type*} {β : α → Type*} {P : ∀ x, β x → Prop} [∀ a, Encodable (β a)]
     [∀ x y, Decidable (P x y)] : (∀ x, ∃ y, P x y) ↔ ∃ f : ∀ a, β a, ∀ x, P x (f x) :=
   ⟨axiom_of_choice, fun ⟨_, H⟩ x => ⟨_, H x⟩⟩
diff --git a/Mathlib/Order/Heyting/Regular.lean b/Mathlib/Order/Heyting/Regular.lean
index 9696c23d7bd77..e0d9932010c39 100644
--- a/Mathlib/Order/Heyting/Regular.lean
+++ b/Mathlib/Order/Heyting/Regular.lean
@@ -227,7 +227,7 @@ theorem isRegular_of_boolean : ∀ a : α, IsRegular a :=
   compl_compl
 
 /-- A decidable proposition is intuitionistically Heyting-regular. -/
-@[nolint decidableClassical]
+@[nolint allOfThem]
 theorem isRegular_of_decidable (p : Prop) [Decidable p] : IsRegular p :=
   propext <| Decidable.not_not
 
diff --git a/Mathlib/Tactic/Linter/UnusedAssumptionInType.lean b/Mathlib/Tactic/Linter/UnusedAssumptionInType.lean
index 4c71217cfea34..1217df107e8da 100644
--- a/Mathlib/Tactic/Linter/UnusedAssumptionInType.lean
+++ b/Mathlib/Tactic/Linter/UnusedAssumptionInType.lean
@@ -61,7 +61,7 @@ def checkUnusedAssumptionInType (declInfo : ConstantInfo) (typesToAvoid : Array
     let names := #[`Decidable, `DecidableEq, `DecidablePred, `Inhabited, `Fintype, `Encodable]
     return ← checkUnusedAssumptionInType (← getConstInfo declName) names
 
-/--/
+/-
 /--
 Linter that checks for theorems that assume `[Decidable p]`
 but don't use this assumption in the type.