fix: address unused simp theorem warnings (#12829)

This PR fixes a few warnings that were introduced by #12325, presumably
because of an interaction with another PR.

.github/workflows/build-template.yml

@@ -131,7 +131,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=()
+          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI

src/Init/Classical.lean

@@ -69,9 +69,11 @@ theorem em (p : Prop) : p ∨ ¬p :=
 theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
   | ⟨x⟩ => ⟨x, trivial⟩
 
+@[implicit_reducible]
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
   ⟨choice h⟩
 
+@[implicit_reducible]
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
   inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
 
@@ -81,6 +83,7 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
     | Or.inl h => ⟨isTrue h⟩
     | Or.inr h => ⟨isFalse h⟩
 
+@[implicit_reducible]
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 

src/Init/Control/Id.lean

@@ -49,6 +49,7 @@ instance : Monad Id where
 /--
 The identity monad has a `bind` operator.
 -/
+@[implicit_reducible]
 def hasBind : Bind Id :=
   inferInstance
 

src/Init/Data/Bool.lean

@@ -629,6 +629,7 @@ export Bool (cond_eq_if cond_eq_ite xor and or not)
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
+@[implicit_reducible]
 def boolPredToPred : Coe (α → Bool) (α  → Prop) where
   coe r := fun a => Eq (r a) true
 

src/Init/Data/Nat/Basic.lean

@@ -478,7 +478,7 @@ instance : Std.Trichotomous (. < . : Nat → Nat → Prop) where
 
 set_option linter.missingDocs false in
 @[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]
-def Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+theorem Nat.instAntisymmNotLt : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm := Nat.instTrichotomousLt.trichotomous
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=

src/Init/Data/Order/Factories.lean

@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
     haveI := LE.ofLT α
     LawfulOrderLT α :=
   letI := LE.ofLT α
-  { lt_iff a b := by simp +instances [LE.ofLT, LE.le]; apply Asymm.asymm }
+  { lt_iff a b := by simp +instances [LE.le]; apply Asymm.asymm }
 
 /--
 If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,7 +253,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
   letI := LE.ofLT α
   { le_min_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, LE.le]
+      simp +instances only [LE.le]
       simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
@@ -283,7 +283,7 @@ public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
   letI := LE.ofLT α
   { max_le_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, LE.le]
+      simp +instances only [LE.le]
       simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 

src/Init/Data/String/Pattern/Basic.lean

@@ -245,7 +245,7 @@ the given {name}`ForwardPattern` instance.
 It is sometimes possible to give a more efficient implementation; see {name}`ToForwardSearcher`
 for more details.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def defaultImplementation [ForwardPattern pat] :
     ToForwardSearcher pat (DefaultForwardSearcher pat) where
   toSearcher := DefaultForwardSearcher.iter pat
@@ -450,7 +450,7 @@ the given {name}`BackwardPattern` instance.
 It is sometimes possible to give a more efficient implementation; see {name}`ToBackwardSearcher`
 for more details.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def defaultImplementation [BackwardPattern pat] :
     ToBackwardSearcher pat (DefaultBackwardSearcher pat) where
   toSearcher := DefaultBackwardSearcher.iter pat

src/Init/Dynamic.lean

@@ -47,6 +47,7 @@ Creates a `TypeName` instance.
 For safety, it is required that the constant `typeName` is definitionally equal
 to `α`.
 -/
+@[implicit_reducible]
 unsafe def TypeName.mk (α : Type u) (typeName : Name) : TypeName α :=
   ⟨unsafeCast typeName⟩
 

src/Init/Grind/Module/Basic.lean

@@ -266,6 +266,7 @@ export NoNatZeroDivisors (no_nat_zero_divisors)
 namespace NoNatZeroDivisors
 
 /-- Alternative constructor for `NoNatZeroDivisors` when we have an `IntModule`. -/
+@[implicit_reducible]
 def mk' {α} [IntModule α]
     (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k • a = 0 → a = 0) :
     NoNatZeroDivisors α where

src/Init/Grind/Ring/Basic.lean

@@ -501,6 +501,7 @@ private theorem mk'_aux {x y : Nat} (p : Nat) (h : y ≤ x) :
       omega
 
 /-- Alternative constructor when `α` is a `Ring`. -/
+@[implicit_reducible]
 def mk' (p : Nat) (α : Type u) [Ring α]
     (ofNat_eq_zero_iff : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0) : IsCharP α p where
   ofNat_ext_iff {x y} := by

src/Init/Grind/Ring/Field.lean

@@ -223,6 +223,7 @@ theorem natCast_div_of_dvd {x y : Nat} (h : y ∣ x) (w : (y : α) ≠ 0) :
       mul_inv_cancel w, Semiring.mul_one]
 
 -- This is expensive as an instance. Let's see what breaks without it.
+@[implicit_reducible]
 def noNatZeroDivisors.ofIsCharPZero [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w
   have := IsCharP.natCast_eq_zero_iff (α := α) 0 a

src/Init/Grind/Ring/ToInt.lean

@@ -15,6 +15,7 @@ public section
 namespace Lean.Grind
 
 /-- A `ToInt` instance on a semiring preserves powers if it preserves numerals and multiplication. -/
+@[implicit_reducible]
 def ToInt.pow_of_semiring [Semiring α] [ToInt α I] [ToInt.OfNat α I] [ToInt.Mul α I]
     (h₁ : I.isFinite) : ToInt.Pow α I where
   toInt_pow x n := by

src/Init/Grind/ToInt.lean

@@ -350,6 +350,7 @@ theorem wrap_toInt (I : IntInterval) [ToInt α I] (x : α) :
 
 /-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and
 a `sub_eq_add_neg` assumption. -/
+@[implicit_reducible]
 def Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α]
     (sub_eq_add_neg : ∀ x y : α, x - y = x + -y)
     {I : IntInterval} (h : I.isFinite) [ToInt α I] [Add α I] [Neg α I] : ToInt.Sub α I where

src/Init/Prelude.lean

@@ -1287,7 +1287,7 @@ export Max (max)
 Constructs a `Max` instance from a decidable `≤` operation.
 -/
 -- Marked inline so that `min x y + max x y` can be optimized to a single branch.
-@[inline]
+@[inline, implicit_reducible]
 def maxOfLe [LE α] [DecidableRel (@LE.le α _)] : Max α where
   max x y := ite (LE.le x y) y x
 
@@ -1304,7 +1304,7 @@ export Min (min)
 Constructs a `Min` instance from a decidable `≤` operation.
 -/
 -- Marked inline so that `min x y + max x y` can be optimized to a single branch.
-@[inline]
+@[inline, implicit_reducible]
 def minOfLe [LE α] [DecidableRel (@LE.le α _)] : Min α where
   min x y := ite (LE.le x y) x y
 

src/Init/System/ST.lean

@@ -272,6 +272,7 @@ Creates a `MonadStateOf` instance from a reference cell.
 This allows programs written against the [state monad](lean-manual://section/state-monads) API to
 be executed using a mutable reference cell to track the state.
 -/
+@[implicit_reducible]
 def Ref.toMonadStateOf (r : Ref σ α) : MonadStateOf α m where
   get := r.get
   set := r.set

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -106,6 +106,7 @@ private def getLitAux (fvarId : FVarId) (ofNat : Nat → α) (ofNatName : Name)
   let some natLit ← getLit fvarId | return none
   return ofNat natLit
 
+@[implicit_reducible]
 def mkNatWrapperInstance (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) : Literal α where
   getLit := (getLitAux · ofNat ofNatName)
   mkLit x := do
@@ -114,6 +115,7 @@ def mkNatWrapperInstance (ofNat : Nat → α) (ofNatName : Name) (toNat : α →
 
 instance : Literal Char := mkNatWrapperInstance Char.ofNat ``Char.ofNat Char.toNat
 
+@[implicit_reducible]
 def mkUIntInstance (matchLit : LitValue → Option α) (litValueCtor : α → LitValue) : Literal α where
   getLit fvarId := do
     let some (.lit litVal) ← findLetValue? (pu := .pure) fvarId | return none

src/Lean/Data/JsonRpc.lean

@@ -224,7 +224,7 @@ instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩
   | RequestID.num _, RequestID.str _            => true
   | _, _ /- str < *, num < null, null < null -/ => false
 
-@[expose] def RequestID.ltProp : LT RequestID :=
+@[expose, implicit_reducible] def RequestID.ltProp : LT RequestID :=
   ⟨fun a b => RequestID.lt a b = true⟩
 
 instance : LT RequestID :=

src/Lean/ToLevel.lean

@@ -34,10 +34,12 @@ instance [ToLevel.{u}] : ToLevel.{u+1} where
   toLevel := .succ toLevel.{u}
 
 /-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/
+@[implicit_reducible]
 def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where
   toLevel := .max toLevel.{u} toLevel.{v}
 
 /-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/
+@[implicit_reducible]
 def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where
   toLevel := .imax toLevel.{u} toLevel.{v}
 

src/lake/Lake/Build/Run.lean

@@ -51,7 +51,7 @@ private structure MonitorContext where
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat
 
-@[inline] def MonitorContext.logger (ctx : MonitorContext) : MonadLog BaseIO :=
+@[inline, implicit_reducible] def MonitorContext.logger (ctx : MonitorContext) : MonadLog BaseIO :=
   .stream ctx.out ctx.outLv ctx.useAnsi
 
 /-- State of the Lake build monitor. -/

tests/elab/Reparen.lean.out.expected

@@ -1286,7 +1286,7 @@ export Max (max)
 Constructs a `Max` instance from a decidable `≤` operation.
 -/
 -- Marked inline so that `min x y + max x y` can be optimized to a single branch.
-@[inline]
+@[inline, implicit_reducible]
 def maxOfLe [LE α] [DecidableRel (  @LE.le α _)] : Max α where
   max x y := ite (  LE.le x y)y x
 
@@ -1303,7 +1303,7 @@ export Min (min)
 Constructs a `Min` instance from a decidable `≤` operation.
 -/
 -- Marked inline so that `min x y + max x y` can be optimized to a single branch.
-@[inline]
+@[inline, implicit_reducible]
 def minOfLe [LE α] [DecidableRel (  @LE.le α _)] : Min α where
   min x y := ite (  LE.le x y)x y