leanprover · Kha · Sep 8, 2026 · Sep 8, 2026
diff --git a/mathlib4/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/mathlib4/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -1230,7 +1230,7 @@ variable (R) in
 semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinNonUnitalCommSemiringOfComm {s : Set A} (hcomm : s.Pairwise Commute) :
     NonUnitalCommSemiring (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm

diff --git a/mathlib4/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean b/mathlib4/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
@@ -769,7 +769,7 @@ open scoped IsMulCommutative in
 semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommSemiringOfComm {s : Set A} (hcomm : s.Pairwise Commute) :
     CommSemiring (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm
@@ -849,7 +849,7 @@ variable (R)
 open scoped IsMulCommutative in
 /-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a commutative
 ring. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommRingOfComm {s : Set A} (hcomm : s.Pairwise Commute) :
     CommRing (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm

diff --git a/mathlib4/Mathlib/Algebra/Ring/Subring/Basic.lean b/mathlib4/Mathlib/Algebra/Ring/Subring/Basic.lean
@@ -605,7 +605,7 @@ theorem isMulCommutative_closure {R} [Ring R] {s : Set R}
 
 open scoped IsMulCommutative in
 /-- If all elements of `s : Set R` commute pairwise, then `closure s` is a commutative ring. -/
-@[deprecated isMulCommutative_closure (since := "2026-03-11")]
+@[deprecated isMulCommutative_closure +typeChanged (since := "2026-03-11")]
 abbrev closureCommRingOfComm {R} [Ring R] {s : Set R} (hcomm : s.Pairwise Commute) :
     CommRing (closure s) :=
   have := isMulCommutative_closure hcomm

diff --git a/mathlib4/Mathlib/Algebra/Ring/Subsemiring/Basic.lean b/mathlib4/Mathlib/Algebra/Ring/Subsemiring/Basic.lean
@@ -1041,7 +1041,7 @@ theorem isMulCommutative_closure {s : Set R'} (hcomm : s.Pairwise Commute) :
 
 open scoped IsMulCommutative in
 /-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring. -/
-@[deprecated isMulCommutative_closure (since := "2026-03-11")]
+@[deprecated isMulCommutative_closure +typeChanged (since := "2026-03-11")]
 abbrev closureCommSemiringOfComm {s : Set R'} (hcomm : s.Pairwise Commute) :
     CommSemiring (closure s) :=
   have := isMulCommutative_closure hcomm

diff --git a/mathlib4/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/mathlib4/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@@ -1293,7 +1293,7 @@ variable (R) in
 `star` of elements in this set, then `adjoin R s` is a non-unital commutative semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinNonUnitalCommSemiringOfComm {s : Set A} (hnormal : ∀ x ∈ s, IsStarNormal x)
     (hcomm : s.Pairwise Commute) (hcomm_star : s.Pairwise (Commute · <| star ·)) :
     NonUnitalCommSemiring (adjoin R s) :=

diff --git a/mathlib4/Mathlib/Algebra/Star/Subalgebra.lean b/mathlib4/Mathlib/Algebra/Star/Subalgebra.lean
@@ -600,7 +600,7 @@ open scoped IsMulCommutative in
 `star` of elements in this set, then `StarAlgebra.adjoin R s` is a commutative semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommSemiringOfComm {s : Set A} (hnormal : ∀ x ∈ s, IsStarNormal x)
     (hcomm : s.Pairwise Commute) (hcomm_star : s.Pairwise (Commute · <| star ·)) :
     CommSemiring (adjoin R s) :=
@@ -619,7 +619,7 @@ open scoped IsMulCommutative in
 `star` of elements in this set, then `StarAlgebra.adjoin R s` is a commutative ring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A]
     [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} (hnormal : ∀ x ∈ s, IsStarNormal x)
     (hcomm : s.Pairwise Commute) (hcomm_star : s.Pairwise (Commute · <| star ·)) :

diff --git a/mathlib4/Mathlib/Data/ENat/Monoid.lean b/mathlib4/Mathlib/Data/ENat/Monoid.lean
@@ -74,7 +74,7 @@ lemma toNatHom_apply (n : ℕ) : toNatHom n = toNat n := rfl
   · rename_i a; cases a <;> simp
   · simp only [toNat_natCast]; rw [← natCast_mul, toNat_natCast]
 
-@[deprecated add_pos_of_right (since := "2026-05-25")]
+@[deprecated add_pos_of_right +typeChanged (since := "2026-05-25")]
 lemma add_one_pos : 0 < n + 1 :=
   add_pos_of_right zero_lt_one n
 

diff --git a/mathlib4/Mathlib/RingTheory/Ideal/GoingUp.lean b/mathlib4/Mathlib/RingTheory/Ideal/GoingUp.lean
@@ -243,7 +243,7 @@ theorem IsIntegral.under_lt_under {I J : Ideal A} [I.IsPrime] (I_lt_J : I < J) :
 @[deprecated (since := "2026-09-03")] alias IsIntegral.comap_lt_comap := IsIntegral.under_lt_under
 
 @[deprecated (since := "2026-05-08")] alias IsIntegralClosure.comap_le_comap :=
-  IsIntegral.comap_lt_comap
+  IsIntegral.under_lt_under
 
 theorem IsIntegral.isMaximal_of_isMaximal_under (I : Ideal A) [I.IsPrime]
     (hI : IsMaximal (I.under R)) : IsMaximal I :=
@@ -253,7 +253,7 @@ theorem IsIntegral.isMaximal_of_isMaximal_under (I : Ideal A) [I.IsPrime]
   IsIntegral.isMaximal_of_isMaximal_under
 
 @[deprecated (since := "2026-05-08")] alias IsIntegralClosure.isMaximal_of_isMaximal_comap :=
-  IsIntegral.isMaximal_of_isMaximal_comap
+  IsIntegral.isMaximal_of_isMaximal_under
 
 theorem IsIntegral.mem_minimalPrimes_map_under (I : Ideal A) [I.IsPrime] :
     I ∈ ((I.under R).map (algebraMap R A)).minimalPrimes := by
@@ -272,7 +272,7 @@ theorem IsIntegral.under_ne_bot [Nontrivial R] {I : Ideal A} (I_ne_bot : I ≠
 @[deprecated (since := "2026-09-03")] alias IsIntegral.comap_ne_bot := IsIntegral.under_ne_bot
 
 @[deprecated (since := "2026-05-08")] alias IsIntegralClosure.comap_ne_bot :=
-  IsIntegral.comap_ne_bot
+  IsIntegral.under_ne_bot
 
 variable (R) in
 theorem IsIntegral.eq_bot_of_under_eq_bot [Nontrivial R] {I : Ideal A} :
@@ -284,24 +284,24 @@ theorem IsIntegral.eq_bot_of_under_eq_bot [Nontrivial R] {I : Ideal A} :
   IsIntegral.eq_bot_of_under_eq_bot
 
 @[deprecated (since := "2026-05-08")] alias IsIntegralClosure.eq_bot_of_comap_eq_bot :=
-    IsIntegral.eq_bot_of_comap_eq_bot
+    IsIntegral.eq_bot_of_under_eq_bot
 
 end IsIntegral
 
 @[deprecated (since := "2026-05-08")] alias IntegralClosure.comap_lt_comap :=
-  IsIntegral.comap_lt_comap
+  IsIntegral.under_lt_under
 
 @[deprecated (since := "2026-05-08")] alias IntegralClosure.isMaximal_of_isMaximal_comap :=
-  IsIntegral.isMaximal_of_isMaximal_comap
+  IsIntegral.isMaximal_of_isMaximal_under
 
 section
 
 variable [IsDomain S]
 
-@[deprecated (since := "2026-05-08")] alias IntegralClosure.comap_ne_bot := IsIntegral.comap_ne_bot
+@[deprecated (since := "2026-05-08")] alias IntegralClosure.comap_ne_bot := IsIntegral.under_ne_bot
 
 @[deprecated (since := "2026-05-08")] alias IntegralClosure.eq_bot_of_comap_eq_bot :=
-  IsIntegral.eq_bot_of_comap_eq_bot
+  IsIntegral.eq_bot_of_under_eq_bot
 
 /-- `comap (algebraMap R S)` is a surjection from the prime spec of `R` to prime spec of `S`.
 `hP : (algebraMap R S).ker ≤ P` is a slight generalization of the extension being injective -/

diff --git a/mathlib4/Mathlib/RingTheory/PowerSeries/Derivative.lean b/mathlib4/Mathlib/RingTheory/PowerSeries/Derivative.lean
@@ -161,7 +161,7 @@ The formal derivative of a power series in one variable.
 This is defined here as a function, but will be packaged as a
 derivation `derivative` on `R⟦X⟧`.
 -/
-@[deprecated derivative (since := "2026-06-26")]
+@[deprecated derivative +typeChanged (since := "2026-06-26")]
 noncomputable def derivativeFun (f : R⟦X⟧) := derivative.toFun f
 
 set_option linter.deprecated false in