diff --git a/Complexitylib/Circuits/AC0/Iteration/Internal.lean b/Complexitylib/Circuits/AC0/Iteration/Internal.lean
index 49e0198c..bd102874 100644
--- a/Complexitylib/Circuits/AC0/Iteration/Internal.lean
+++ b/Complexitylib/Circuits/AC0/Iteration/Internal.lean
@@ -25,16 +25,12 @@ namespace Switching
 
 attribute [local instance] Classical.propDecidable
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private def finiteEventCount {α : Type} [Fintype α]
-    [DecidableEq α] (event : α → Prop)
+private def finiteEventCount {α : Type} [Fintype α] (event : α → Prop)
     [DecidablePred event] : ℕ :=
   (Finset.univ.filter event).card
 
 private theorem finiteEventCount_mono
-    {α : Type} [Fintype α] [DecidableEq α]
+    {α : Type} [Fintype α]
     (left right : α → Prop)
     [DecidablePred left] [DecidablePred right]
     (himp : ∀ value, left value → right value) :
@@ -62,7 +58,6 @@ private theorem finiteEventCount_or_le_add
 
 private theorem finiteEventCount_prod
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → β → Prop)
     [∀ first, DecidablePred (event first)] :
     finiteEventCount
@@ -89,7 +84,6 @@ private theorem finiteEventCount_prod
 
 private theorem finiteEventCount_prod_mul_le
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → β → Prop)
     [∀ first, DecidablePred (event first)]
     (multiplier bound : ℕ)
@@ -110,7 +104,6 @@ private theorem finiteEventCount_prod_mul_le
 
 private theorem finiteEventCount_prod_left
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → Prop) [DecidablePred event] :
     finiteEventCount
         (fun pair : α × β => event pair.1) =
@@ -133,12 +126,8 @@ private theorem finiteEventCount_prod_left
     _ = finiteEventCount event * Fintype.card β := by
           simp [finiteEventCount]
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 private theorem finiteEventCount_exists_mem_le_sum
-    {α β : Type} [Fintype α] [DecidableEq α]
-    [DecidableEq β] (values : List β)
+    {α β : Type} [Fintype α] (values : List β)
     (event : β → α → Prop)
     [∀ value, DecidablePred (event value)] :
     finiteEventCount (fun sample =>
@@ -170,7 +159,7 @@ private theorem finiteEventCount_exists_mem_le_sum
           simp
 
 private theorem exists_not_event_of_weight_sum
-    {α : Type} [Fintype α] [DecidableEq α]
+    {α : Type} [Fintype α]
     (event : α → Prop) [DecidablePred event]
     (weight : α → ℕ) (cap threshold : ℕ)
     (hcap : ∀ value, weight value ≤ cap)
diff --git a/Complexitylib/Circuits/Basic.lean b/Complexitylib/Circuits/Basic.lean
index e8383ea6..c68610e8 100644
--- a/Complexitylib/Circuits/Basic.lean
+++ b/Complexitylib/Circuits/Basic.lean
@@ -207,9 +207,6 @@ Primary input vertices are not counted, and the negation flags on gate inputs
 have zero cost. Some texts instead count input vertices and explicit NOT gates;
 those conventions agree only up to additive/linear overhead, not on exact size
 bounds. -/
--- The circuit argument is unused by design: `size` is determined by the
--- indices, and the argument exists purely to enable `c.size` dot notation.
-@[nolint unusedArguments]
 def size (_ : Circuit B N M G) : Nat := G + M
 
 end Circuit
@@ -258,16 +255,14 @@ noncomputable def sizeComplexityWithTop
     (B : Basis) (f : BitString N → Bool) : WithTop Nat :=
   sInf ((fun s : Nat => (s : WithTop Nat)) '' realizationSizes B f)
 
-/-- The minimum circuit size over a complete basis `B` computing `f`.
+/-- The minimum circuit size over a basis `B` computing `f`.
 
-This natural-valued interface requires completeness so that the set of
-realizing circuits is nonempty. Use `sizeComplexityWithTop` when the basis may
-be incomplete. -/
--- Completeness is an intentional API precondition. The infimum expression
--- itself does not inspect the selected witness.
-@[nolint unusedArguments]
+The results that identify this with an achieved size take `[CompleteBasis B]`,
+which makes the set of realizing circuits nonempty. Over an incomplete basis
+the infimum of the empty set is `0`, so an unrealizable function would be
+indistinguishable from a zero-size one; use `sizeComplexityWithTop` there. -/
 noncomputable def sizeComplexity
-    (B : Basis) [CompleteBasis B] (f : BitString N → Bool) : Nat :=
+    (B : Basis) (f : BitString N → Bool) : Nat :=
   sInf (realizationSizes B f)
 
 private theorem realizationSizes_nonempty [CompleteBasis B]
@@ -350,7 +345,7 @@ theorem sizeComplexity_pos [CompleteBasis B]
   omega
 
 /-- Any circuit computing `f` has size at least `sizeComplexity B f`. -/
-theorem sizeComplexity_le [CompleteBasis B] {G : Nat}
+theorem sizeComplexity_le {G : Nat}
     (c : Circuit B N 1 G) (f : BitString N → Bool)
     (hf : (fun x => (c.eval x) 0) = f) :
     sizeComplexity B f ≤ c.size :=
diff --git a/Complexitylib/Circuits/Encoding/Machine/Core/Defs.lean b/Complexitylib/Circuits/Encoding/Machine/Core/Defs.lean
index 6b224c14..07e549f5 100644
--- a/Complexitylib/Circuits/Encoding/Machine/Core/Defs.lean
+++ b/Complexitylib/Circuits/Encoding/Machine/Core/Defs.lean
@@ -380,7 +380,6 @@ def FamilyCorePre (codeBits inputBits : List Bool) (initialInput : Tape)
 core. Malformed codes and successful false evaluations both write zero. The
 terminal work tapes are intentionally unconstrained because rejecting parses
 halt at different code, memo, and counter cursor positions. -/
-@[nolint unusedArguments]
 def FamilyCorePost (codeBits inputBits : List Bool) (initialInput : Tape)
     (inp : Tape) (_work : Fin workTapeCount → Tape) (out : Tape) : Prop :=
   inp = initialInput ∧
@@ -402,7 +401,6 @@ def evalFamilyTime (n : ℕ) : ℕ :=
 cells retain the original encoding and the output carries the defaulted paired
 evaluation verdict with its canonical head and left-marker invariant. Terminal
 work tapes are intentionally unconstrained across valid and rejecting branches. -/
-@[nolint unusedArguments]
 def EvalFamilyPost (bits : List Bool) (inp : Tape)
     (_work : Fin workTapeCount → Tape) (out : Tape) : Prop :=
   inp.cells = (Tape.init (bits.map Γ.ofBool)).cells ∧
diff --git a/Complexitylib/Circuits/Family.lean b/Complexitylib/Circuits/Family.lean
index d4d8de9e..75ca112e 100644
--- a/Complexitylib/Circuits/Family.lean
+++ b/Complexitylib/Circuits/Family.lean
@@ -58,7 +58,7 @@ theorem Computes.sizeComplexityWithTop_le {c : Circuit B N 1 G}
 
 /-- Over a complete basis, any circuit computing `f` witnesses a natural-valued
 upper bound on its size complexity. -/
-theorem Computes.sizeComplexity_le [CompleteBasis B] {c : Circuit B N 1 G}
+theorem Computes.sizeComplexity_le {c : Circuit B N 1 G}
     {f : BitString N → Bool} (h : c.Computes f) :
     sizeComplexity B f ≤ c.size :=
   Circuit.sizeComplexity_le c f h
diff --git a/Complexitylib/Circuits/Internal/ShannonUpper.lean b/Complexitylib/Circuits/Internal/ShannonUpper.lean
index 05a71912..86c1b63c 100644
--- a/Complexitylib/Circuits/Internal/ShannonUpper.lean
+++ b/Complexitylib/Circuits/Internal/ShannonUpper.lean
@@ -657,10 +657,6 @@ theorem encodeColumn_lt (k : Nat) (col : Fin (2^k) → Bool) :
 /-- The column function of `f` at data row `y`: maps an address `a` to
     `f(a, y)`, reading the first `k` input bits from `a` and the remaining
     `q` bits from `y`. -/
--- `_hkq : k + q = N` is a documented precondition tying the address width
--- `k` and data width `q` to `N`; it is threaded by every caller but not
--- needed in the body, which is polymorphic in `k`, `q`.
-@[nolint unusedArguments]
 noncomputable def columnFunction (N : Nat) (f : BitString N → Bool)
     (k q : Nat) (_hkq : k + q = N) (y : Fin (2^q)) : Fin (2^k) → Bool :=
   fun a => f (fun idx =>
@@ -681,10 +677,7 @@ theorem columnPatternIndex_lt (N : Nat) (f : BitString N → Bool)
 
 /-! ### Shannon gate array -/
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private noncomputable def shannonGateArray (N : Nat) [NeZero N]
+private noncomputable def shannonGateArray (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) :
     (i : Fin (totalSectionGates (addrBits N) (dataBits N))) →
     { g : Gate Basis.andOr2 (N + totalSectionGates (addrBits N) (dataBits N)) //
@@ -1021,10 +1014,7 @@ private def shiftedBits (N k q : Nat) (hkq : k + q = N) (x : BitString N) :
   fun j => x ⟨k + j.val, by have := j.isLt; omega⟩
 
 /-- columnFunction at the actual bit-vector address/data values equals f(x). -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private theorem columnFunction_at_actual_bits (N : Nat) [NeZero N]
+private theorem columnFunction_at_actual_bits (N : Nat)
     (f : BitString N → Bool) (x : BitString N)
     (k q : Nat) (hkq : k + q = N) :
     let addr : BitString k := fun j => x ⟨j.val, by have := j.isLt; omega⟩
@@ -1130,10 +1120,7 @@ private theorem dataSum_lt (N : Nat) (hN : 16 ≤ N) (x : BitString N) :
   sum_cond_pow_fin_lt (dataBits N) (shiftedBits N (addrBits N) (dataBits N) (addrDataSum N hN) x)
 
 /-- andLayerSem at y is false when y ≠ dataSum. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private theorem andLayerSem_ne (N : Nat) [NeZero N]
+private theorem andLayerSem_ne (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N)
     (y : Nat) (hy : y < 2 ^ dataBits N) (hne : y ≠ dataSum N hN x) :
     andLayerSem N f hN x y hy = false := by
@@ -1141,14 +1128,14 @@ private theorem andLayerSem_ne (N : Nat) [NeZero N]
   simp only [beq_eq_false_iff_ne.mpr hne, Bool.false_and]
 
 /-- andLayerSem at dataSum gives columnFunction at actual bits. -/
-private theorem andLayerSem_eq (N : Nat) [NeZero N]
+private theorem andLayerSem_eq (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N) :
     andLayerSem N f hN x (dataSum N hN x) (dataSum_lt N hN x) = f x := by
   unfold andLayerSem dataSum
   simp only [beq_self_eq_true, Bool.true_and]
   exact columnFunction_at_actual_bits N f x (addrBits N) (dataBits N) (addrDataSum N hN)
 
-private theorem or_andLayerSem_eq_f (N : Nat) [NeZero N]
+private theorem or_andLayerSem_eq_f (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N) :
     (List.range (2 ^ dataBits N)).foldl
       (fun acc y => acc || if h : y < 2 ^ dataBits N
diff --git a/Complexitylib/Circuits/Internal/Valiant.lean b/Complexitylib/Circuits/Internal/Valiant.lean
index 765899f1..953b460c 100644
--- a/Complexitylib/Circuits/Internal/Valiant.lean
+++ b/Complexitylib/Circuits/Internal/Valiant.lean
@@ -156,10 +156,7 @@ omit [Fintype V] in
 /-- **Extending a simple path by an edge.** In an acyclic digraph, a
 simple path `p` ending at `u` followed by an edge `u → v` yields a
 simple path ending at `v` that is one longer. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private lemma extend_simple_path [DecidableEq V] (G : Digraph V) (hac : IsAcyclic G)
+private lemma extend_simple_path (G : Digraph V) (hac : IsAcyclic G)
     {u v : V} (huv : G.Adj u v) {n : ℕ} {p : Fin (n + 1) → V}
     (hsp : G.IsPath p) (hpu : p (Fin.last n) = u) :
     ∃ p' : Fin (n + 2) → V, G.IsPath p' ∧ p' (Fin.last (n + 1)) = v := by
@@ -190,7 +187,7 @@ private lemma extend_simple_path [DecidableEq V] (G : Digraph V) (hac : IsAcycli
 ending at `u` followed by the edge `(u,v)` is a strictly longer simple
 path ending at `v` (using acyclicity to ensure `v` does not already
 appear in the path). -/
-lemma canonicalLabel_isLegal [DecidableEq V] (G : Digraph V) (hac : IsAcyclic G) :
+lemma canonicalLabel_isLegal (G : Digraph V) (hac : IsAcyclic G) :
     IsLegalLabeling G G.canonicalLabel := by
   intro u v huv
   obtain ⟨p, hsp, hpu⟩ :=
@@ -362,6 +359,7 @@ noncomputable def levelEdges
   G.edgeFinset.filter (fun e =>
     firstDifferBit k (G.canonicalLabel e.1 - 1) (G.canonicalLabel e.2 - 1) = i)
 
+omit [DecidableEq V] in
 /-- For any edge `(u,v)` of an acyclic `G` with `depth ≤ 2 ^ k`, the first
 MSB-disagreement of the `k`-bit canonical labels is in `{1,...,k}`. -/
 private lemma firstDifferBit_mem_Ioc
@@ -380,6 +378,7 @@ private lemma firstDifferBit_mem_Ioc
     (canonicalLabel_sub_one_lt_two_pow G hd _)
   exact Finset.mem_Ioc.mpr ⟨hpos, hle⟩
 
+omit [DecidableEq V] in
 /-- **Partition.** When `G` is acyclic and `G.depth ≤ 2 ^ k`, every
 edge lies in exactly one level `E_i` for `i ∈ {1,...,k}`. -/
 lemma sum_card_levelEdges_eq
@@ -435,6 +434,7 @@ private lemma exists_r_subset_sum_le
       have hih_step : n' * (∑ i ∈ I, a i) ≤ r * (∑ i ∈ s', a i) := hI_le
       omega
 
+omit [DecidableEq V] in
 /-- **Averaging.** There is a choice of `r` levels whose total edge
 count is at most `r * S / k` (equivalently, `k * total ≤ r * S`). -/
 lemma exists_r_levels_small
diff --git a/Complexitylib/Circuits/Nondeterminism.lean b/Complexitylib/Circuits/Nondeterminism.lean
index cdc65675..f10a7f53 100644
--- a/Complexitylib/Circuits/Nondeterminism.lean
+++ b/Complexitylib/Circuits/Nondeterminism.lean
@@ -106,7 +106,7 @@ theorem sizeComplexity_or_le [CompleteBasis Basis.andOr2] [NeZero N]
 
 /-- Circuit complexity is invariant under propositional equality of input
     dimension. -/
-private theorem sizeComplexity_cast [CompleteBasis B] [NeZero n] [NeZero n']
+private theorem sizeComplexity_cast [NeZero n] [NeZero n']
     (h : n = n') (f : BitString n → Bool) :
     Circuit.sizeComplexity B (h ▸ f : BitString n' → Bool) =
       Circuit.sizeComplexity B f := by
@@ -200,7 +200,7 @@ theorem sizeComplexity_existsQuantify_le [CompleteBasis Basis.andOr2]
     exponential circuit complexity,
     `existsQuantify f` has complexity at most `O(2^m / m)`, which decreases
     exponentially as more variables are quantified away. -/
-theorem sizeComplexity_existsQuantify_le_shannon [CompleteBasis Basis.andOr2]
+theorem sizeComplexity_existsQuantify_le_shannon
     (f : BitString (k + m) → Bool) [NeZero m] (hm : 16 ≤ m) :
     Circuit.sizeComplexity Basis.andOr2 (existsQuantify f) ≤ 18 * 2 ^ m / m :=
   shannon_upper_bound m hm (existsQuantify f)
diff --git a/Complexitylib/Circuits/NormalForm/Defs.lean b/Complexitylib/Circuits/NormalForm/Defs.lean
index 08f6e6b2..78e2f143 100644
--- a/Complexitylib/Circuits/NormalForm/Defs.lean
+++ b/Complexitylib/Circuits/NormalForm/Defs.lean
@@ -49,8 +49,6 @@ structure Literal (N : Nat) where
   polarity : Bool
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprLiteral.repr
 
 /-- Evaluate a literal on a bit assignment. -/
 def Literal.eval (l : Literal N) (x : BitString N) : Bool :=
@@ -118,8 +116,6 @@ structure CNF (N : Nat) where
   clauses : List (List (Literal N))
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprCNF.repr
 
 namespace CNF
 
@@ -212,8 +208,6 @@ structure DNF (N : Nat) where
   terms : List (List (Literal N))
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprDNF.repr
 
 namespace DNF
 
diff --git a/Complexitylib/Circuits/Shannon.lean b/Complexitylib/Circuits/Shannon.lean
index 2c66969a..f9c121f4 100644
--- a/Complexitylib/Circuits/Shannon.lean
+++ b/Complexitylib/Circuits/Shannon.lean
@@ -79,8 +79,7 @@ theorem shannon_sizeComplexity (N : Nat) [NeZero N] (hN : 6 ≤ N)
     This is the full-column-library variant (C = 18). The tighter
     `(1 + o(1)) · 2^N / N` bound due to Lupanov (1958) uses column
     grouping and is not yet formalized. -/
-theorem shannon_upper_bound [CompleteBasis Basis.andOr2]
-    (N : Nat) (hN : 16 ≤ N) [NeZero N]
+theorem shannon_upper_bound (N : Nat) (hN : 16 ≤ N) [NeZero N]
     (f : BitString N → Bool) :
     Circuit.sizeComplexity Basis.andOr2 f ≤ 18 * 2 ^ N / N := by
   obtain ⟨G, c, heval, hsize⟩ := ShannonUpper.shannon_construction N hN f
diff --git a/Complexitylib/Circuits/Threshold/Defs.lean b/Complexitylib/Circuits/Threshold/Defs.lean
index 6822b6bb..c4037479 100644
--- a/Complexitylib/Circuits/Threshold/Defs.lean
+++ b/Complexitylib/Circuits/Threshold/Defs.lean
@@ -29,8 +29,6 @@ structure ThresholdOp where
   cutoff : ℕ
   deriving Repr, DecidableEq
 
--- This record printer intentionally ignores precedence.
-attribute [nolint unusedArguments] instReprThresholdOp.repr
 
 namespace ThresholdOp
 
diff --git a/Complexitylib/Classes/AverageCase/FiniteEnsemble.lean b/Complexitylib/Classes/AverageCase/FiniteEnsemble.lean
index 8008e95c..1f975f05 100644
--- a/Complexitylib/Classes/AverageCase/FiniteEnsemble.lean
+++ b/Complexitylib/Classes/AverageCase/FiniteEnsemble.lean
@@ -64,7 +64,7 @@ theorem uniformProbability_union_le {Ω : Type u}
 
 /-- Conditioning by a finite partition of a uniform sample space. -/
 theorem uniformProbability_eq_sum_fiberwise
-    {Ω : Type u} {ι : Type v} [Fintype Ω] [DecidableEq Ω]
+    {Ω : Type u} {ι : Type v} [Fintype Ω]
     [DecidableEq ι] (event : Finset Ω) (indices : Finset ι) (f : Ω → ι)
     (hmaps : (event : Set Ω).MapsTo f indices) :
     uniformProbability event =
@@ -74,8 +74,8 @@ theorem uniformProbability_eq_sum_fiberwise
 
 /-- Independent finite uniform seeds multiply event probabilities. -/
 theorem uniformProbability_product
-    {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω]
-    [Fintype Ξ] [DecidableEq Ξ] (P : Ω → Prop) (Q : Ξ → Prop)
+    {Ω : Type u} {Ξ : Type v} [Fintype Ω]
+    [Fintype Ξ] (P : Ω → Prop) (Q : Ξ → Prop)
     [DecidablePred P] [DecidablePred Q] :
     uniformProbability
         (Finset.univ.filter fun seed : Ω × Ξ => P seed.1 ∧ Q seed.2) =
@@ -85,16 +85,11 @@ theorem uniformProbability_product
 
 /-- Uniform probability on a product is the average of its conditional fiber
 probabilities over the first coordinate. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformProbability_product_eq_average_fibers
     {advice : Type u} {challenge : Type v}
-    [Fintype advice] [DecidableEq advice] [Nonempty advice]
-    [Fintype challenge] [DecidableEq challenge] [Nonempty challenge]
+    [Fintype advice] [Nonempty advice]
+    [Fintype challenge] [Nonempty challenge]
     (event : advice → challenge → Prop)
-    [DecidablePred fun sample : advice × challenge =>
-      event sample.1 sample.2]
     [∀ fixed, DecidablePred (event fixed)] :
     uniformProbability (Finset.univ.filter fun sample : advice × challenge =>
         event sample.1 sample.2) =
@@ -105,16 +100,11 @@ theorem uniformProbability_product_eq_average_fibers
 
 /-- Some first-coordinate fiber has probability at least the joint product
 probability. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem exists_fiber_uniformProbability_ge
     {advice : Type u} {challenge : Type v}
-    [Fintype advice] [DecidableEq advice] [Nonempty advice]
-    [Fintype challenge] [DecidableEq challenge] [Nonempty challenge]
+    [Fintype advice] [Nonempty advice]
+    [Fintype challenge] [Nonempty challenge]
     (event : advice → challenge → Prop)
-    [DecidablePred fun sample : advice × challenge =>
-      event sample.1 sample.2]
     [∀ fixed, DecidablePred (event fixed)] :
     ∃ fixed : advice,
       uniformProbability (Finset.univ.filter fun sample : advice × challenge =>
@@ -125,7 +115,7 @@ theorem exists_fiber_uniformProbability_ge
 /-- If a finite statistic is at most one, its mean is bounded by a threshold
 plus the probability of exceeding that threshold times the remaining range. -/
 theorem uniformMean_le_threshold_add_probability
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (threshold : ℚ)
     (hupper : ∀ input, value input ≤ 1) :
     uniformMean value ≤ threshold +
@@ -135,7 +125,7 @@ theorem uniformMean_le_threshold_add_probability
 
 /-- Exact reverse averaging bound for a statistic bounded above by one. -/
 theorem uniformMean_sub_div_le_probability_ge
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (lower threshold : ℚ)
     (hupper : ∀ input, value input ≤ 1)
     (hlower : lower ≤ uniformMean value) (hthreshold : threshold < 1) :
@@ -149,7 +139,7 @@ theorem uniformMean_sub_div_le_probability_ge
 `1/2 + ε` forces an `ε/2` fraction of samples to have value at least
 `1/2 + ε/2`. -/
 theorem half_epsilon_le_probability_ge_of_le_uniformMean
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (epsilon : ℚ)
     (hepsilon : 0 ≤ epsilon) (hupper : ∀ input, value input ≤ 1)
     (hmean : 1 / 2 + epsilon ≤ uniformMean value) :
@@ -207,8 +197,8 @@ theorem half_le_uniformAtLeastOneProbability_of_singleDrawLower
 /-- Relabeling a finite uniform sample space by an equivalence preserves event
 probability. -/
 theorem uniformProbability_equiv
-    {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω]
-    [Fintype Ξ] [DecidableEq Ξ] (e : Ω ≃ Ξ) (P : Ξ → Prop)
+    {Ω : Type u} {Ξ : Type v} [Fintype Ω]
+    [Fintype Ξ] (e : Ω ≃ Ξ) (P : Ξ → Prop)
     [DecidablePred P] :
     uniformProbability (Finset.univ.filter fun x : Ω => P (e x)) =
       uniformProbability (Finset.univ.filter P) :=
diff --git a/Complexitylib/Classes/AverageCase/FiniteEnsemble/Internal.lean b/Complexitylib/Classes/AverageCase/FiniteEnsemble/Internal.lean
index 77975b84..fbf50f12 100644
--- a/Complexitylib/Classes/AverageCase/FiniteEnsemble/Internal.lean
+++ b/Complexitylib/Classes/AverageCase/FiniteEnsemble/Internal.lean
@@ -72,11 +72,8 @@ theorem uniformProbability_union_le_internal {Ω : Type u}
   gcongr
   exact_mod_cast Finset.card_union_le event₁ event₂
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformProbability_eq_sum_fiberwise_internal
-    {Ω : Type u} {ι : Type v} [Fintype Ω] [DecidableEq Ω]
+    {Ω : Type u} {ι : Type v} [Fintype Ω]
     [DecidableEq ι] (event : Finset Ω) (indices : Finset ι) (f : Ω → ι)
     (hmaps : (event : Set Ω).MapsTo f indices) :
     uniformProbability event =
@@ -87,12 +84,9 @@ theorem uniformProbability_eq_sum_fiberwise_internal
   push_cast
   rw [Finset.sum_div]
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformProbability_product_internal
-    {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω]
-    [Fintype Ξ] [DecidableEq Ξ] (P : Ω → Prop) (Q : Ξ → Prop)
+    {Ω : Type u} {Ξ : Type v} [Fintype Ω]
+    [Fintype Ξ] (P : Ω → Prop) (Q : Ξ → Prop)
     [DecidablePred P] [DecidablePred Q] :
     uniformProbability
         (Finset.univ.filter fun seed : Ω × Ξ => P seed.1 ∧ Q seed.2) =
@@ -115,16 +109,11 @@ theorem uniformProbability_product_internal
     ((Finset.univ.filter P).card : ℚ) (Fintype.card Ω : ℚ)
     ((Finset.univ.filter Q).card : ℚ) (Fintype.card Ξ : ℚ)).symm
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformProbability_product_eq_average_fibers_internal
     {advice : Type u} {challenge : Type v}
-    [Fintype advice] [DecidableEq advice] [Nonempty advice]
-    [Fintype challenge] [DecidableEq challenge] [Nonempty challenge]
+    [Fintype advice] [Nonempty advice]
+    [Fintype challenge] [Nonempty challenge]
     (event : advice → challenge → Prop)
-    [DecidablePred fun sample : advice × challenge =>
-      event sample.1 sample.2]
     [∀ fixed, DecidablePred (event fixed)] :
     uniformProbability (Finset.univ.filter fun sample : advice × challenge =>
         event sample.1 sample.2) =
@@ -163,16 +152,11 @@ theorem uniformProbability_product_eq_average_fibers_internal
   intro fixed _hfixed
   field_simp [hadvice, hchallenge]
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem exists_fiber_uniformProbability_ge_internal
     {advice : Type u} {challenge : Type v}
-    [Fintype advice] [DecidableEq advice] [Nonempty advice]
-    [Fintype challenge] [DecidableEq challenge] [Nonempty challenge]
+    [Fintype advice] [Nonempty advice]
+    [Fintype challenge] [Nonempty challenge]
     (event : advice → challenge → Prop)
-    [DecidablePred fun sample : advice × challenge =>
-      event sample.1 sample.2]
     [∀ fixed, DecidablePred (event fixed)] :
     ∃ fixed : advice,
       uniformProbability (Finset.univ.filter fun sample : advice × challenge =>
@@ -197,11 +181,8 @@ theorem exists_fiber_uniformProbability_ge_internal
     (Finset.univ_nonempty : (Finset.univ : Finset advice).Nonempty) hsum
   exact ⟨fixed, hle⟩
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformMean_le_threshold_add_probability_internal
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (threshold : ℚ)
     (hupper : ∀ input, value input ≤ 1) :
     uniformMean value ≤ threshold +
@@ -252,7 +233,7 @@ theorem uniformMean_le_threshold_add_probability_internal
       ring
 
 theorem uniformMean_sub_div_le_probability_ge_internal
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (lower threshold : ℚ)
     (hupper : ∀ input, value input ≤ 1)
     (hlower : lower ≤ uniformMean value) (hthreshold : threshold < 1) :
@@ -267,7 +248,7 @@ theorem uniformMean_sub_div_le_probability_ge_internal
   linarith
 
 theorem half_epsilon_le_probability_ge_of_le_uniformMean_internal
-    {sample : Type u} [Fintype sample] [DecidableEq sample]
+    {sample : Type u} [Fintype sample]
     [Nonempty sample] (value : sample → ℚ) (epsilon : ℚ)
     (hepsilon : 0 ≤ epsilon) (hupper : ∀ input, value input ≤ 1)
     (hmean : 1 / 2 + epsilon ≤ uniformMean value) :
@@ -406,12 +387,9 @@ theorem half_le_uniformAtLeastOneProbability_of_singleDrawLower_internal
     htrials.trans <| mul_le_mul_of_nonneg_left hlower (by positivity)
   nlinarith
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 theorem uniformProbability_equiv_internal
-    {Ω : Type u} {Ξ : Type v} [Fintype Ω] [DecidableEq Ω]
-    [Fintype Ξ] [DecidableEq Ξ] (e : Ω ≃ Ξ) (P : Ξ → Prop)
+    {Ω : Type u} {Ξ : Type v} [Fintype Ω]
+    [Fintype Ξ] (e : Ω ≃ Ξ) (P : Ξ → Prop)
     [DecidablePred P] :
     uniformProbability (Finset.univ.filter fun x : Ω => P (e x)) =
       uniformProbability (Finset.univ.filter P) := by
diff --git a/Complexitylib/Classes/Containments/Internal/BlockScan.lean b/Complexitylib/Classes/Containments/Internal/BlockScan.lean
index 1175edc5..02742a2b 100644
--- a/Complexitylib/Classes/Containments/Internal/BlockScan.lean
+++ b/Complexitylib/Classes/Containments/Internal/BlockScan.lean
@@ -101,9 +101,6 @@ def markCount (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1))
 
 /-- Count the markers, saturating at two: the first component says there is at least one, the
 second that there are at least two. -/
--- The last two columns are the chunk's symbol bits, which this check ignores; the arity is
--- fixed by `Complexity.Scanner.chunkRun`.
-@[nolint unusedArguments]
 def markStep (r : Fin (j + 1)) (x : Bool × Bool)
     (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool × Bool :=
   if c1 r = Γ.one then (true, x.1 || x.2) else x
@@ -211,9 +208,6 @@ theorem agreeOk_iff (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (
 /-! ## Where the marker moves -/
 
 /-- The head stays: the markers must agree. -/
--- The last two columns are the chunk's symbol bits, which this check ignores; the arity is
--- fixed by `Complexity.Scanner.chunkRun`.
-@[nolint unusedArguments]
 def stayStep (a b : Fin (j + 1)) (x : Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool :=
   x && (decide (c1 a = Γ.one) == decide (c1 b = Γ.one))
 
@@ -240,9 +234,6 @@ def prevMark (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a : Fin (j + 1)) (
   if p = 0 then false else markOf cols off a (p - 1)
 
 /-- The head moves right: the new marker is one chunk on. -/
--- The last two columns are the chunk's symbol bits, which this check ignores; the arity is
--- fixed by `Complexity.Scanner.chunkRun`.
-@[nolint unusedArguments]
 def rightStep (a b : Fin (j + 1)) (x : Bool × Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) :
     Bool × Bool :=
   (x.1 && (decide (c1 b = Γ.one) == x.2), decide (c1 a = Γ.one))
@@ -279,9 +270,6 @@ theorem rightStep_run (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (o
 /-- The head moves left: the new marker is one chunk back, except from chunk zero, where moving
 left stays put. The fold carries the previous chunk's new marker, whether chunk zero has gone by,
 and whether the old marker was on chunk zero. -/
--- The last two columns are the chunk's symbol bits, which this check ignores; the arity is
--- fixed by `Complexity.Scanner.chunkRun`.
-@[nolint unusedArguments]
 def leftStep (a b : Fin (j + 1)) (x : Bool × Bool × Bool × Bool)
     (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool × Bool × Bool × Bool :=
   let mA := decide (c1 a = Γ.one)
diff --git a/Complexitylib/Classes/Containments/Internal/PPParts.lean b/Complexitylib/Classes/Containments/Internal/PPParts.lean
index 8c855a71..7f975e4c 100644
--- a/Complexitylib/Classes/Containments/Internal/PPParts.lean
+++ b/Complexitylib/Classes/Containments/Internal/PPParts.lean
@@ -148,7 +148,6 @@ def tallyState {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → T
 /-- The iteration count read back off the counter tape. The input and output tapes are ignored;
 they are present because `TM.loopTM_hoareTime_indexed` takes the index as a function of the whole
 tape state. -/
-@[nolint unusedArguments]
 noncomputable def tallyIdx {n : ℕ} (cIdx : Fin n) :
     Tape → (Fin n → Tape) → Tape → ℕ :=
   fun _ work _ => Classical.epsilon fun v => (work cIdx).HasBinaryNat v
diff --git a/Complexitylib/Classes/Containments/Internal/SpaceIterate.lean b/Complexitylib/Classes/Containments/Internal/SpaceIterate.lean
index 938e7bb9..8cda9d55 100644
--- a/Complexitylib/Classes/Containments/Internal/SpaceIterate.lean
+++ b/Complexitylib/Classes/Containments/Internal/SpaceIterate.lean
@@ -201,7 +201,6 @@ noncomputable def ctrValue (t : Tape) : ℕ :=
 /-- The loop's index function: how far the counter has advanced past `start`.
 The input and output tapes are ignored, but `TM.loopTM_hoareTime_indexed` takes
 the index as a function of the whole configuration, so they have to be there. -/
-@[nolint unusedArguments]
 noncomputable def loopIdx (k start : ℕ) :
     Tape → (Fin (3 + (k + 2) + 0) → Tape) → Tape → ℕ :=
   fun _ work _ => ctrValue (work rfIdx) - start
diff --git a/Complexitylib/Classes/EventProb.lean b/Complexitylib/Classes/EventProb.lean
index 1d3ca772..d6616f3a 100644
--- a/Complexitylib/Classes/EventProb.lean
+++ b/Complexitylib/Classes/EventProb.lean
@@ -201,10 +201,7 @@ theorem eventProb_biUnion_le {T : ℕ} {ι : Type*} [DecidableEq ι] (s : Finset
 
 /-- Finite additivity: the probability of a disjoint finite union is the sum of
     the probabilities of its events. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-theorem eventProb_biUnion {T : ℕ} {ι : Type*} [DecidableEq ι]
+theorem eventProb_biUnion {T : ℕ} {ι : Type*}
     (s : Finset ι) (E : ι → Finset (Fin T → Bool))
     (h : (s : Set ι).PairwiseDisjoint E) :
     eventProb (s.biUnion E) = ∑ i ∈ s, eventProb (E i) := by
diff --git a/Complexitylib/Classes/FiniteCounting.lean b/Complexitylib/Classes/FiniteCounting.lean
index 31536b77..d8bd8787 100644
--- a/Complexitylib/Classes/FiniteCounting.lean
+++ b/Complexitylib/Classes/FiniteCounting.lean
@@ -493,17 +493,11 @@ private theorem card_filter_blockEventCount_eq_iff (k T j : ℕ)
   · intro f _
     exact Equiv.apply_symm_apply _ _
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private def eventBits {k : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
+private def eventBits {k : ℕ} {α : Type*} [DecidableEq α]
     (E : Finset α) (f : Fin k → α) : Fin k → Bool :=
   fun i => decide (f i ∈ E)
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private def eventCount {k : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
+private def eventCount {k : ℕ} {α : Type*} [DecidableEq α]
     (E : Finset α) (f : Fin k → α) : ℕ :=
   (Finset.univ.filter (fun i : Fin k => f i ∈ E)).card
 
diff --git a/Complexitylib/Classes/PCP/Internal/AlgEdge.lean b/Complexitylib/Classes/PCP/Internal/AlgEdge.lean
index b9fa7999..ac002182 100644
--- a/Complexitylib/Classes/PCP/Internal/AlgEdge.lean
+++ b/Complexitylib/Classes/PCP/Internal/AlgEdge.lean
@@ -154,10 +154,7 @@ theorem blockBlk_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) :
     (ifEqLen_mem_FP readFn_mem_FP (constFn_mem_FP _) hrot (testFn_mem_FP r))
 
 /-- **The block is the one the read asks for.** -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-theorem blockBlk_eq {β : Type} [Fintype β] [DecidableEq β] [Nonempty β] {R : RegCSP β}
+theorem blockBlk_eq {β : Type} {R : RegCSP β}
     [NumEnc R.graph.V] [NumEnc R.graph.D] (F : FinBase) (pol : Polynomial ℕ) (r : Round)
     {w : List Bool} (p : R.Dart) (i : ReadIdx)
     (hread : readFn w = List.replicate (NumEnc.enc i) true)
diff --git a/Complexitylib/Classes/PCP/Internal/AlgPosNum.lean b/Complexitylib/Classes/PCP/Internal/AlgPosNum.lean
index b6282b3e..5cc069f5 100644
--- a/Complexitylib/Classes/PCP/Internal/AlgPosNum.lean
+++ b/Complexitylib/Classes/PCP/Internal/AlgPosNum.lean
@@ -191,11 +191,8 @@ theorem satSet_congr (p : R.Dart) (p' : R'.Dart)
 
 omit [DecidableEq β] [Nonempty β] [NumEnc R.graph.V] [NumEnc R.graph.D] in
 /-- **So does the cube a read names**, even across two different systems. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-theorem cubeNum_congr {β' : Type} [Fintype β'] [DecidableEq β'] [Nonempty β']
-    {R' : RegCSP β'} [NumEnc R'.graph.V] [NumEnc R'.graph.D] {enc' : β' → Cube B}
+theorem cubeNum_congr {β' : Type} [Fintype β']
+    {R' : RegCSP β'} {enc' : β' → Cube B}
     (p : R.Dart) (p' : R'.Dart) (z : Cube (ROf B)) (i : ReadIdx)
     (h : R.satSet enc p = R'.satSet enc' p') :
     R.cubeNum enc p z i = R'.cubeNum enc' p' z i := by
@@ -203,11 +200,8 @@ theorem cubeNum_congr {β' : Type} [Fintype β'] [DecidableEq β'] [Nonempty β'
 
 omit [DecidableEq β] [Nonempty β] [NumEnc R.graph.V] [NumEnc R.graph.D] in
 /-- **And so does the test's verdict.** -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-theorem check_congr {β' : Type} [Fintype β'] [DecidableEq β'] [Nonempty β']
-    {R' : RegCSP β'} [NumEnc R'.graph.V] [NumEnc R'.graph.D] {enc' : β' → Cube B}
+theorem check_congr {β' : Type} [Fintype β']
+    {R' : RegCSP β'} {enc' : β' → Cube B}
     (p : R.Dart) (p' : R'.Dart) (z : Cube (ROf B))
     (h : R.satSet enc p = R'.satSet enc' p') :
     (R.compose enc).check p z = (R'.compose enc').check p' z := by
@@ -255,6 +249,7 @@ theorem satSet_eq_of_data (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T
   rw [h]
   rfl
 
+omit [Nonempty α] in
 /-- **The cube a read names is the same across two such graphs.** -/
 theorem cubeNum_eq_of_data (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T B : ℕ}
     (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V)
@@ -268,6 +263,7 @@ theorem cubeNum_eq_of_data (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T
   RegCSP.cubeNum_congr (R := (G.preprocess E).killedPow q T hq) (enc := encβ)
     (R' := (G'.preprocess E).killedPow q T hq) (enc' := encβ) (v, x) (v', x) z i h
 
+omit [Nonempty α] in
 /-- **And so is the test's verdict.** -/
 theorem check_eq_of_data (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T B : ℕ}
     (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V)
diff --git a/Complexitylib/Classes/PCP/Internal/Pad.lean b/Complexitylib/Classes/PCP/Internal/Pad.lean
index 019968f5..3380f202 100644
--- a/Complexitylib/Classes/PCP/Internal/Pad.lean
+++ b/Complexitylib/Classes/PCP/Internal/Pad.lean
@@ -83,10 +83,7 @@ theorem unsatFrac_pad (G : ConstraintGraph α) {N : ℕ} (h : G.numVerts ≤ N)
     (G.pad N h).unsatFrac a = G.unsatFrac (G.restrict h a) := rfl
 
 /-- **Padding does not change the value.** -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-theorem unsatVal_pad [Fintype α] [Nonempty α] [DecidableEq α] (G : ConstraintGraph α)
+theorem unsatVal_pad [Fintype α] [Nonempty α] (G : ConstraintGraph α)
     (N : ℕ) (h : G.numVerts ≤ N) :
     (G.pad N h).unsatVal = G.unsatVal := by
   classical
diff --git a/Complexitylib/Languages/LengthDivBy.lean b/Complexitylib/Languages/LengthDivBy.lean
index 1573af4a..d655b16f 100644
--- a/Complexitylib/Languages/LengthDivBy.lean
+++ b/Complexitylib/Languages/LengthDivBy.lean
@@ -60,10 +60,7 @@ end Language
 
 /-- The "count bits mod k" fold: starting from `seed`, scanning `x` yields
     `seed + x.length` in `ZMod k`. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private theorem lengthDivBy_fold (k : ℕ) [NeZero k] :
+private theorem lengthDivBy_fold (k : ℕ) :
     ∀ (x : List Bool) (seed : ZMod k),
       x.foldl (fun (s : ZMod k) (_ : Bool) => s + 1) seed =
         seed + (x.length : ZMod k) := by
@@ -76,7 +73,7 @@ private theorem lengthDivBy_fold (k : ℕ) [NeZero k] :
     push_cast
     ring
 
-private theorem lengthDivBy_fold_zero (k : ℕ) [NeZero k] (x : List Bool) :
+private theorem lengthDivBy_fold_zero (k : ℕ) (x : List Bool) :
     x.foldl (fun (s : ZMod k) (_ : Bool) => s + 1) 0 = (x.length : ZMod k) := by
   rw [lengthDivBy_fold, zero_add]
 
diff --git a/Complexitylib/Mathlib/Digraph.lean b/Complexitylib/Mathlib/Digraph.lean
index 6214654a..cd4f3e74 100644
--- a/Complexitylib/Mathlib/Digraph.lean
+++ b/Complexitylib/Mathlib/Digraph.lean
@@ -59,14 +59,13 @@ lemma pathLength_bddAbove [Fintype V] (G : Digraph V) :
   rintro m ⟨p, _, hp⟩
   simpa only [Fintype.card_fin] using Fintype.card_le_of_injective p hp
 
-/-- The **depth** of a finite digraph is the maximum length — number of
-vertices — of a simple directed path. Using simple paths makes `depth` a
-total, honest finite measure even when the graph contains a cycle. Results
-whose proofs require a DAG state `IsAcyclic` explicitly. -/
--- The instance restricts the definition's domain to finite graphs; the
--- supremum expression itself does not inspect the chosen enumeration.
-@[nolint unusedArguments]
-noncomputable def depth [Fintype V] (G : Digraph V) : Nat :=
+/-- The **depth** of a digraph is the maximum length — number of vertices — of
+a simple directed path. Using simple paths makes `depth` a total, honest
+finite measure even when the graph contains a cycle. The supremum is only
+meaningful when the path lengths are bounded, so every result about `depth`
+takes `[Fintype V]`; those whose proofs additionally need a DAG state
+`IsAcyclic` explicitly. -/
+noncomputable def depth (G : Digraph V) : Nat :=
   sSup {m | ∃ p : Fin m → V, G.IsPath p}
 
 /-- A finite digraph's simple-path depth is at most its number of vertices. -/
@@ -111,7 +110,7 @@ def IsAcyclic (G : Digraph V) : Prop :=
 
 /-- The simple-path set of `G.deleteEdges ∅` agrees with that of `G`,
 so the two graphs have the same depth. -/
-lemma depth_deleteEdges_empty [Fintype V] (G : Digraph V) :
+lemma depth_deleteEdges_empty (G : Digraph V) :
     (G.deleteEdges ∅).depth = G.depth := by
   unfold Digraph.depth
   congr 1
diff --git a/Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Instruction/Sim/Defs.lean b/Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Instruction/Sim/Defs.lean
index d66a77a9..6e8c93ce 100644
--- a/Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Instruction/Sim/Defs.lean
+++ b/Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Instruction/Sim/Defs.lean
@@ -63,7 +63,6 @@ def liftedSource {n : ℕ} (tapes : ControlInstructionTapes n) : Fin (n + 1) :=
   tapes.lifted.data.update.entry.source
 
 /-- Fresh last work tape receiving the next encoded store. -/
-@[nolint unusedArguments]
 def buffer {n : ℕ} (_tapes : ControlInstructionTapes n) : Fin (n + 1) :=
   Fin.last n
 
diff --git a/Complexitylib/Models/TuringMachine/UTM/Diagonal.lean b/Complexitylib/Models/TuringMachine/UTM/Diagonal.lean
index e57da676..2e2a64af 100644
--- a/Complexitylib/Models/TuringMachine/UTM/Diagonal.lean
+++ b/Complexitylib/Models/TuringMachine/UTM/Diagonal.lean
@@ -2216,15 +2216,9 @@ theorem diagTM_flips_of_halts (clk : TM 8) (C : ℕ) (g : ℕ → ℕ)
   · rw [ite_eq_right hm]
     simp [hm]
 
-set_option linter.unusedVariables false in
-/-- Compatibility form of `diagTM_flips_of_halts`. The positivity hypothesis
-    is not needed for the flip itself, but remains in this public signature for
-    callers of the original theorem. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
+/-- Short name for `diagTM_flips_of_halts`. -/
 theorem diagTM_flips (clk : TM 8) (C : ℕ) (g : ℕ → ℕ)
-    (hclk : ClockWitness clk C g) (hg1 : ∀ n, 1 ≤ g n)
+    (hclk : ClockWitness clk C g)
     (x : List Bool) (hterm : TerminatedRegion x)
     (T : ℕ) (mcF : Cfg 1 (decodeDesc x).toTM.Q) (hT : T ≤ g x.length)
     (hrun : (decodeDesc x).toTM.reachesIn T ((decodeDesc x).toTM.initCfg x) mcF)