chore: adaptations for nightly-2026-02-03

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -165,15 +165,11 @@ theorem disjoint_bits (p q : ℕ) :
 
 open MeasureTheory.Measure
 
-private def measurableSpace_list_int : MeasurableSpace (List ℤ) := ⊤
+private local instance measurableSpace_list_int : MeasurableSpace (List ℤ) := ⊤
 
-attribute [local instance] measurableSpace_list_int
-
-private theorem measurableSingletonClass_list_int : MeasurableSingletonClass (List ℤ) :=
+private local instance measurableSingletonClass_list_int : MeasurableSingletonClass (List ℤ) :=
   { measurableSet_singleton := fun _ => trivial }
 
-attribute [local instance] measurableSingletonClass_list_int
-
 private theorem list_int_measurableSet {s : Set (List ℤ)} : MeasurableSet s := trivial
 
 theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p + q).choose p

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -32,7 +32,7 @@ variable [SMulCommClass R A A] [IsScalarTower R A A]
 /-- The multiplication in a non-unital non-associative algebra is a bilinear map.
 
 A weaker version of this for semirings exists as `AddMonoidHom.mul`. -/
-@[simps!]
+@[instance_reducible, simps!]
 def mul : A →ₗ[R] A →ₗ[R] A :=
   LinearMap.mk₂ R (· * ·) add_mul smul_mul_assoc mul_add mul_smul_comm
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -510,6 +510,7 @@ open Pointwise
 /-- `Submodule.pointwiseNeg` distributes over multiplication.
 
 This is available as an instance in the `Pointwise` locale. -/
+@[instance_reducible]
 protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A) :=
   toAddSubmonoid_injective.hasDistribNeg _ neg_toAddSubmonoid mul_toAddSubmonoid
 
@@ -752,6 +753,7 @@ variable {α : Type*} [Monoid α] [MulSemiringAction α A] [SMulCommClass α R A
 This is available as an instance in the `Pointwise` locale.
 
 This is a stronger version of `Submodule.pointwiseDistribMulAction`. -/
+@[instance_reducible]
 protected def pointwiseMulSemiringAction : MulSemiringAction α (Submodule R A) where
   __ := Submodule.pointwiseDistribMulAction
   smul_mul r x y := Submodule.map_mul x y <| MulSemiringAction.toAlgHom R A r

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -92,6 +92,7 @@ section
 variable [Semiring S] [AddCommMonoid M]
 
 /-- We temporarily install an action of the original ring on `RestrictScalars R S M`. -/
+@[instance_reducible]
 def RestrictScalars.moduleOrig [I : Module S M] : Module S (RestrictScalars R S M) := I
 
 variable [CommSemiring R] [Algebra R S]

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

@@ -68,6 +68,7 @@ variable {R' : Type*} [Semiring R'] [MulSemiringAction R' A] [SMulCommClass R' R
 /-- The action on a subalgebra corresponding to applying the action to every element.
 
 This is available as an instance in the `Pointwise` locale. -/
+@[instance_reducible]
 protected def pointwiseMulAction : MulAction R' (Subalgebra R A) where
   smul a S := S.map (MulSemiringAction.toAlgHom _ _ a)
   one_smul S := (congr_arg (fun f => S.map f) (AlgHom.ext <| one_smul R')).trans S.map_id

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -244,7 +244,9 @@ lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
 
 @[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.foldr_op_eq
 
-@[to_additive (attr := simp)]
+-- The additive version `List.sum_reverse` exists in Core and it has less general instance
+-- parameters.
+@[simp]
 lemma prod_reverse (l : List M) : prod l.reverse = prod l := (reverse_perm l).prod_eq
 
 @[to_additive]

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -112,6 +112,7 @@ variable {R}
 equivalence with `Comon(R-Mod)`. This is just an auxiliary definition; the `MonoidalCategory`
 instance we make in `Mathlib/Algebra/Category/CoalgCat/Monoidal.lean` has better
 definitional equalities. -/
+@[instance_reducible]
 noncomputable def instMonoidalCategoryAux : MonoidalCategory (CoalgCat R) :=
   Monoidal.transport (comonEquivalence R).symm
 

Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean

@@ -57,6 +57,7 @@ instance (x : FGModuleRepr R) : Module.Finite R x := by
   unfold repr; infer_instance
 
 /-- A non-canonical representation of a finite module (as a quotient of `Rⁿ`). -/
+@[instance_reducible]
 noncomputable def ofFinite : FGModuleRepr R where
   n := (Module.Finite.exists_fin_quot_equiv R M).choose
   S := (Module.Finite.exists_fin_quot_equiv R M).choose_spec.choose

Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean

@@ -114,11 +114,14 @@ namespace AddCommGrpCat
 
 /-- We choose `AddCommGrpCat.of (G × H)` as the product of `G` and `H` and
 `AddCommGrpCat.of PUnit` as the terminal object. -/
+@[instance_reducible]
 noncomputable def cartesianMonoidalCategory : CartesianMonoidalCategory AddCommGrpCat.{u} :=
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (AddCommGrpCat.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
-@[deprecated (since := "2025-10-10")]
+-- This is deprecated, but still used as a `local instance` in
+-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
+@[instance_reducible, deprecated (since := "2025-10-10")]
 alias cartesianMonoidalCategoryAddCommGrp := cartesianMonoidalCategory
 
 attribute [local instance] cartesianMonoidalCategory

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -44,6 +44,8 @@ variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 namespace leftExactFunctorForgetEquivalence
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
+
+-- This was deprecated on 2025-10-10 but is still used as a local instance here!
 attribute [local instance] AddCommGrpCat.cartesianMonoidalCategoryAddCommGrp
 
 set_option backward.privateInPublic true in

Mathlib/Algebra/Category/ModuleCat/Algebra.lean

@@ -44,6 +44,7 @@ variable {k : Type u} [Field k]
 variable {A : Type w} [Ring A] [Algebra k A]
 
 /-- Type synonym for considering a module over a `k`-algebra as a `k`-module. -/
+@[instance_reducible]
 def moduleOfAlgebraModule (M : ModuleCat.{v} A) : Module k M :=
   RestrictScalars.module k A M
 

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -110,12 +110,10 @@ inductive Relation : Prequotient F → Prequotient F → Prop -- Make it an equi
 
 /-- The setoid corresponding to monoid expressions modulo monoid relations and identifications.
 -/
-def colimitSetoid : Setoid (Prequotient F) where
+instance colimitSetoid : Setoid (Prequotient F) where
   r := Relation F
   iseqv := ⟨Relation.refl, Relation.symm _ _, Relation.trans _ _ _⟩
 
-attribute [instance] colimitSetoid
-
 /-- The underlying type of the colimit of a diagram in `MonCat`.
 -/
 def ColimitType : Type v :=

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -98,12 +98,10 @@ inductive Relation : Prequotient F → Prequotient F → Prop -- Make it an equi
 
 /-- The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
 -/
-def colimitSetoid : Setoid (Prequotient F) where
+instance colimitSetoid : Setoid (Prequotient F) where
   r := Relation F
   iseqv := ⟨Relation.refl, Relation.symm _ _, Relation.trans _ _ _⟩
 
-attribute [instance] colimitSetoid
-
 /-- The underlying type of the colimit of a diagram in `CommRingCat`.
 -/
 def ColimitType : Type v :=
@@ -392,12 +390,10 @@ inductive Relation : Prequotient F → Prequotient F → Prop -- Make it an equi
 
 /-- The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
 -/
-def colimitSetoid : Setoid (Prequotient F) where
+instance colimitSetoid : Setoid (Prequotient F) where
   r := Relation F
   iseqv := ⟨Relation.refl, Relation.symm _ _, Relation.trans _ _ _⟩
 
-attribute [instance] colimitSetoid
-
 /-- The underlying type of the colimit of a diagram in `CommRingCat`.
 -/
 def ColimitType : Type v :=

Mathlib/Algebra/FreeAlgebra.lean

@@ -72,26 +72,33 @@ instance : Inhabited (Pre R X) := ⟨ofScalar 0⟩
 
 -- Note: These instances are only used to simplify the notation.
 /-- Coercion from `X` to `Pre R X`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasCoeGenerator : Coe X (Pre R X) := ⟨of⟩
 
 /-- Coercion from `R` to `Pre R X`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasCoeSemiring : Coe R (Pre R X) := ⟨ofScalar⟩
 
 /-- Multiplication in `Pre R X` defined as `Pre.mul`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasMul : Mul (Pre R X) := ⟨mul⟩
 
 /-- Addition in `Pre R X` defined as `Pre.add`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasAdd : Add (Pre R X) := ⟨add⟩
 
 /-- Zero in `Pre R X` defined as the image of `0` from `R`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasZero : Zero (Pre R X) := ⟨ofScalar 0⟩
 
 /-- One in `Pre R X` defined as the image of `1` from `R`. Note: Used for notation only. -/
+@[instance_reducible]
 def hasOne : One (Pre R X) := ⟨ofScalar 1⟩
 
 /-- Scalar multiplication defined as multiplication by the image of elements from `R`.
 Note: Used for notation only.
 -/
+@[instance_reducible]
 def hasSMul : SMul R (Pre R X) := ⟨fun r m ↦ mul (ofScalar r) m⟩
 
 end Pre

Mathlib/Algebra/Group/Action/Basic.lean

@@ -95,7 +95,7 @@ section Arrow
 variable {G A B : Type*} [DivisionMonoid G] [MulAction G A]
 
 /-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
-@[to_additive (attr := simps) arrowAddAction
+@[to_additive (attr := instance_reducible) (attr := simps) arrowAddAction
 /-- If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)` -/]
 def arrowAction : MulAction G (A → B) where
   smul g F a := F (g⁻¹ • a)
@@ -111,6 +111,7 @@ attribute [local instance] arrowAction
 variable [Monoid M]
 
 /-- When `M` is a monoid, `ArrowAction` is additionally a `MulDistribMulAction`. -/
+@[instance_reducible]
 def arrowMulDistribMulAction : MulDistribMulAction G (A → M) where
   smul_one _ := rfl
   smul_mul _ _ _ := rfl

Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

@@ -79,7 +79,7 @@ instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α
 
 /-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
 `Finset α` on `Finset β`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
       /-- An additive action of an additive monoid `α` on a type `β` gives an additive action
       of `Finset α` on `Finset β` -/]
 protected def mulAction [DecidableEq α] [Monoid α] [MulAction α β] :
@@ -89,7 +89,7 @@ protected def mulAction [DecidableEq α] [Monoid α] [MulAction α β] :
 
 /-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Finset β`.
 -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
       /-- An additive action of an additive monoid on a type `β` gives an additive action
       on `Finset β`. -/]
 protected def mulActionFinset [Monoid α] [MulAction α β] : MulAction α (Finset β) :=

Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

@@ -168,15 +168,15 @@ instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α
 
 /-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `Set α`
 on `Set β`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
 /-- An additive action of an additive monoid `α` on a type `β` gives an additive action of `Set α`
 on `Set β` -/]
 protected noncomputable def mulAction [Monoid α] [MulAction α β] : MulAction (Set α) (Set β) where
   mul_smul _ _ _ := image2_assoc mul_smul
   one_smul s := image2_singleton_left.trans <| by simp_rw [one_smul, image_id']
 
 /-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Set β`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
 /-- An additive action of an additive monoid on a type `β` gives an additive action on `Set β`. -/]
 protected def mulActionSet [Monoid α] [MulAction α β] : MulAction α (Set β) where
   mul_smul _ _ _ := by simp only [← image_smul, image_image, ← mul_smul]

Mathlib/Algebra/Group/Conj.lean

@@ -110,6 +110,7 @@ namespace IsConj
 /- This small quotient API is largely copied from the API of `Associates`;
 where possible, try to keep them in sync -/
 /-- The setoid of the relation `IsConj` iff there is a unit `u` such that `u * x = y * u` -/
+@[instance_reducible]
 protected def setoid (α : Type*) [Monoid α] : Setoid α where
   r := IsConj
   iseqv := ⟨IsConj.refl, IsConj.symm, IsConj.trans⟩

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -51,6 +51,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
+@[instance_reducible]
 def instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n) where
   __ := inferInstanceAs (AddCommMonoid (Fin n))
   natCast i := Fin.ofNat n i

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -66,7 +66,8 @@ section One
 variable [One α] {s : Finset α} {a : α}
 
 /-- The finset `1 : Finset α` is defined as `{1}` in scope `Pointwise`. -/
-@[to_additive /-- The finset `0 : Finset α` is defined as `{0}` in scope `Pointwise`. -/]
+@[to_additive (attr := instance_reducible)
+  /-- The finset `0 : Finset α` is defined as `{0}` in scope `Pointwise`. -/]
 protected def one : One (Finset α) :=
   ⟨{1}⟩
 
@@ -183,7 +184,7 @@ section Inv
 variable [DecidableEq α] [Inv α] {s t : Finset α} {a : α}
 
 /-- The pointwise inversion of finset `s⁻¹` is defined as `{x⁻¹ | x ∈ s}` in scope `Pointwise`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
   /-- The pointwise negation of finset `-s` is defined as `{-x | x ∈ s}` in scope `Pointwise`. -/]
 protected def inv : Inv (Finset α) :=
   ⟨image Inv.inv⟩
@@ -316,7 +317,7 @@ variable [DecidableEq α] [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α
 
 /-- The pointwise multiplication of finsets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}`
 in scope `Pointwise`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
   /-- The pointwise addition of finsets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in
   scope `Pointwise`. -/]
 protected def mul : Mul (Finset α) :=
@@ -535,7 +536,7 @@ variable [DecidableEq α] [Div α] {s s₁ s₂ t t₁ t₂ u : Finset α} {a b
 
 /-- The pointwise division of finsets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
 `Pointwise`. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
   /-- The pointwise subtraction of finsets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}`
   in scope `Pointwise`. -/]
 protected def div : Div (Finset α) :=
@@ -696,11 +697,13 @@ variable [DecidableEq α] [DecidableEq β]
 
 /-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Finset`. See
 note [pointwise nat action]. -/
+@[instance_reducible]
 protected def nsmul [Zero α] [Add α] : SMul ℕ (Finset α) :=
   ⟨nsmulRec⟩
 
 /-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
 `Finset`. See note [pointwise nat action]. -/
+@[instance_reducible]
 protected def npow [One α] [Mul α] : Pow (Finset α) ℕ :=
   ⟨fun s n => npowRec n s⟩
 
@@ -709,19 +712,21 @@ attribute [to_additive existing] Finset.npow
 
 /-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
 addition/subtraction!) of a `Finset`. See note [pointwise nat action]. -/
+@[instance_reducible]
 protected def zsmul [Zero α] [Add α] [Neg α] : SMul ℤ (Finset α) :=
   ⟨zsmulRec⟩
 
 /-- Repeated pointwise multiplication/division (not the same as pointwise repeated
 multiplication/division!) of a `Finset`. See note [pointwise nat action]. -/
-@[to_additive existing]
+@[instance_reducible, to_additive existing]
 protected def zpow [One α] [Mul α] [Inv α] : Pow (Finset α) ℤ :=
   ⟨fun s n => zpowRec npowRec n s⟩
 
 scoped[Pointwise] attribute [instance] Finset.nsmul Finset.npow Finset.zsmul Finset.zpow
 
 /-- `Finset α` is a `Semigroup` under pointwise operations if `α` is. -/
-@[to_additive /-- `Finset α` is an `AddSemigroup` under pointwise operations if `α` is. -/]
+@[to_additive (attr := instance_reducible)
+  /-- `Finset α` is an `AddSemigroup` under pointwise operations if `α` is. -/]
 protected def semigroup [Semigroup α] : Semigroup (Finset α) :=
   coe_injective.semigroup _ coe_mul
 
@@ -730,7 +735,8 @@ section CommSemigroup
 variable [CommSemigroup α] {s t : Finset α}
 
 /-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is. -/
-@[to_additive /-- `Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. -/]
+@[to_additive (attr := instance_reducible)
+  /-- `Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. -/]
 protected def commSemigroup : CommSemigroup (Finset α) :=
   coe_injective.commSemigroup _ coe_mul
 
@@ -749,7 +755,8 @@ section MulOneClass
 variable [MulOneClass α]
 
 /-- `Finset α` is a `MulOneClass` under pointwise operations if `α` is. -/
-@[to_additive /-- `Finset α` is an `AddZeroClass` under pointwise operations if `α` is. -/]
+@[to_additive (attr := instance_reducible)
+  /-- `Finset α` is an `AddZeroClass` under pointwise operations if `α` is. -/]
 protected def mulOneClass : MulOneClass (Finset α) :=
   coe_injective.mulOneClass _ (coe_singleton 1) coe_mul
 
@@ -812,7 +819,8 @@ theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n := by
   | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]
 
 /-- `Finset α` is a `Monoid` under pointwise operations if `α` is. -/
-@[to_additive /-- `Finset α` is an `AddMonoid` under pointwise operations if `α` is. -/]
+@[to_additive (attr := instance_reducible)
+  /-- `Finset α` is an `AddMonoid` under pointwise operations if `α` is. -/]
 protected def monoid : Monoid (Finset α) :=
   coe_injective.monoid _ coe_one coe_mul coe_pow
 
@@ -937,7 +945,8 @@ section CommMonoid
 variable [CommMonoid α]
 
 /-- `Finset α` is a `CommMonoid` under pointwise operations if `α` is. -/
-@[to_additive /-- `Finset α` is an `AddCommMonoid` under pointwise operations if `α` is. -/]
+@[to_additive (attr := instance_reducible)
+  /-- `Finset α` is an `AddCommMonoid` under pointwise operations if `α` is. -/]
 protected def commMonoid : CommMonoid (Finset α) :=
   coe_injective.commMonoid _ coe_one coe_mul coe_pow
 
@@ -961,7 +970,7 @@ protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} 
   simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
 
 /-- `Finset α` is a division monoid under pointwise operations if `α` is. -/
-@[to_additive
+@[to_additive (attr := instance_reducible)
   /-- `Finset α` is a subtraction monoid under pointwise operations if `α` is. -/]
 protected def divisionMonoid : DivisionMonoid (Finset α) :=
   coe_injective.divisionMonoid _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow
@@ -1015,7 +1024,7 @@ lemma singleton_zpow (a : α) (n : ℤ) : ({a} : Finset α) ^ n = {a ^ n} := by
 end DivisionMonoid
 
 /-- `Finset α` is a commutative division monoid under pointwise operations if `α` is. -/
-@[to_additive subtractionCommMonoid
+@[to_additive (attr := instance_reducible) subtractionCommMonoid
   /-- `Finset α` is a commutative subtraction monoid under pointwise operations if `α` is. -/]
 protected def divisionCommMonoid [DivisionCommMonoid α] :
     DivisionCommMonoid (Finset α) :=