From 3fa5f452ee1652a47dcf496bc3d52db2f2bdd810 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 25 Nov 2024 13:34:38 +0000 Subject: [PATCH] chore: ensure there is a replacement identifier or text suggestion for all deprecations (#19426) This is for compatibility with the stricter requirements of leanprover/lean4#6112. Anyone is welcome to replace the "No deprecation message was provided." messages in other PRs! :-) --- Mathlib/Algebra/BigOperators/Group/List.lean | 2 +- Mathlib/Algebra/Group/Action/Defs.lean | 8 +- Mathlib/Algebra/Group/AddChar.lean | 2 +- Mathlib/Algebra/Group/Equiv/Basic.lean | 20 +++- Mathlib/Algebra/Group/Pointwise/Set/Card.lean | 29 +++++- Mathlib/Algebra/Module/LinearMap/Defs.lean | 4 +- Mathlib/Algebra/Order/Field/Power.lean | 4 +- .../Algebra/Order/Group/Pointwise/Bounds.lean | 7 +- Mathlib/Analysis/Complex/Circle.lean | 6 +- Mathlib/CategoryTheory/Adjunction/Limits.lean | 8 +- .../CategoryTheory/Idempotents/Karoubi.lean | 2 +- Mathlib/CategoryTheory/Limits/Creates.lean | 12 +-- .../Limits/FunctorCategory/Basic.lean | 8 +- Mathlib/Data/Complex/Abs.lean | 2 +- Mathlib/Data/Fin/Basic.lean | 2 +- Mathlib/Data/List/Basic.lean | 8 +- Mathlib/Data/List/Flatten.lean | 3 +- Mathlib/Data/List/Indexes.lean | 12 +-- Mathlib/Data/List/Lex.lean | 2 +- Mathlib/Data/List/Pairwise.lean | 3 +- Mathlib/Data/List/Permutation.lean | 2 +- Mathlib/Data/Nat/Defs.lean | 2 +- Mathlib/Data/Set/Pointwise/SMul.lean | 9 +- Mathlib/Data/Setoid/Basic.lean | 4 +- Mathlib/Deprecated/AlgebraClasses.lean | 47 ++++----- Mathlib/Deprecated/ByteArray.lean | 10 +- Mathlib/Deprecated/Combinator.lean | 9 +- Mathlib/Deprecated/Equiv.lean | 4 +- Mathlib/Deprecated/LazyList.lean | 10 +- Mathlib/Deprecated/Logic.lean | 74 +++++++-------- Mathlib/Deprecated/NatLemmas.lean | 8 +- Mathlib/Deprecated/RelClasses.lean | 10 +- Mathlib/GroupTheory/Coset/Basic.lean | 8 +- Mathlib/GroupTheory/Coset/Defs.lean | 20 +++- Mathlib/GroupTheory/Exponent.lean | 3 +- Mathlib/GroupTheory/GroupAction/Defs.lean | 8 +- Mathlib/GroupTheory/GroupAction/Quotient.lean | 17 +++- Mathlib/GroupTheory/OrderOfElement.lean | 7 +- .../GroupTheory/SpecificGroups/Cyclic.lean | 9 +- Mathlib/LinearAlgebra/BilinearForm/Basic.lean | 10 +- Mathlib/LinearAlgebra/BilinearForm/Hom.lean | 20 ++-- Mathlib/LinearAlgebra/Prod.lean | 28 +++--- Mathlib/Logic/Basic.lean | 9 +- Mathlib/MeasureTheory/Function/L1Space.lean | 2 +- .../MeasureTheory/Measure/Typeclasses.lean | 2 +- .../Measure/WithDensityFinite.lean | 2 +- Mathlib/NumberTheory/ArithmeticFunction.lean | 3 +- Mathlib/NumberTheory/MulChar/Basic.lean | 6 +- Mathlib/Order/Defs.lean | 8 +- Mathlib/Order/OmegaCompletePartialOrder.lean | 2 +- Mathlib/Order/RelClasses.lean | 6 +- Mathlib/SetTheory/Cardinal/Aleph.lean | 18 ++-- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- Mathlib/SetTheory/Cardinal/Cofinality.lean | 2 +- Mathlib/SetTheory/Game/Ordinal.lean | 2 +- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 95 ++++++++++--------- Mathlib/SetTheory/Ordinal/Basic.lean | 8 +- Mathlib/SetTheory/Ordinal/Enum.lean | 2 +- Mathlib/SetTheory/Ordinal/FixedPoint.lean | 66 ++++++------- Mathlib/SetTheory/Ordinal/Principal.lean | 4 +- Mathlib/SetTheory/ZFC/Basic.lean | 43 +++++---- Mathlib/Topology/Algebra/ConstMulAction.lean | 2 +- .../Topology/Algebra/ContinuousMonoidHom.lean | 3 +- Mathlib/Topology/Algebra/Group/Quotient.lean | 6 +- Mathlib/Topology/LocalAtTarget.lean | 4 +- Mathlib/Topology/MetricSpace/Polish.lean | 2 +- Mathlib/Topology/NoetherianSpace.lean | 2 +- Mathlib/Topology/Order/OrderClosed.lean | 2 +- 68 files changed, 442 insertions(+), 324 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean index bf01489af4f70..2bd6c8a351d66 100644 --- a/Mathlib/Algebra/BigOperators/Group/List.lean +++ b/Mathlib/Algebra/BigOperators/Group/List.lean @@ -634,7 +634,7 @@ end MonoidHom end MonoidHom set_option linter.deprecated false in -@[simp, deprecated (since := "2024-10-17")] +@[simp, deprecated "No deprecation message was provided." (since := "2024-10-17")] lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum := rfl namespace List diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean index 823dbf69f3586..294281be04be5 100644 --- a/Mathlib/Algebra/Group/Action/Defs.lean +++ b/Mathlib/Algebra/Group/Action/Defs.lean @@ -297,9 +297,15 @@ lemma smul_mul_smul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] (a • b) * (c • d) = (a * c) • (b * d) := by have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d -@[to_additive (attr := deprecated (since := "2024-08-29"))] +@[to_additive] alias smul_mul_smul := smul_mul_smul_comm +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated smul_mul_smul_comm (since := "2024-08-29")] smul_mul_smul +attribute [deprecated vadd_add_vadd_comm (since := "2024-08-29")] vadd_add_vadd + + /-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually satisfied by `Algebra α β`. -/ @[to_additive] diff --git a/Mathlib/Algebra/Group/AddChar.lean b/Mathlib/Algebra/Group/AddChar.lean index 4b0c0f3e8d9bd..0279bc188d39a 100644 --- a/Mathlib/Algebra/Group/AddChar.lean +++ b/Mathlib/Algebra/Group/AddChar.lean @@ -253,7 +253,7 @@ lemma ne_one_iff : ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff lemma ne_zero_iff : ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff /-- An additive character is *nontrivial* if it takes a value `≠ 1`. -/ -@[deprecated (since := "2024-06-06")] +@[deprecated "No deprecation message was provided." (since := "2024-06-06")] def IsNontrivial (ψ : AddChar A M) : Prop := ∃ a : A, ψ a ≠ 1 set_option linter.deprecated false in diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean index 203ef93e84ead..b0b66218245be 100644 --- a/Mathlib/Algebra/Group/Equiv/Basic.lean +++ b/Mathlib/Algebra/Group/Equiv/Basic.lean @@ -94,12 +94,28 @@ class MulEquivClass (F : Type*) (A B : outParam Type*) [Mul A] [Mul B] [EquivLik /-- Preserves multiplication. -/ map_mul : ∀ (f : F) (a b), f (a * b) = f a * f b -@[to_additive (attr := deprecated (since := "2024-11-10"))] +@[to_additive] alias MulEquivClass.map_eq_one_iff := EmbeddingLike.map_eq_one_iff -@[to_additive (attr := deprecated (since := "2024-11-10"))] +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated EmbeddingLike.map_eq_one_iff (since := "2024-11-10")] +MulEquivClass.map_eq_one_iff +attribute [deprecated EmbeddingLike.map_eq_zero_iff (since := "2024-11-10")] +AddEquivClass.map_eq_zero_iff + + +@[to_additive] alias MulEquivClass.map_ne_one_iff := EmbeddingLike.map_ne_one_iff +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated EmbeddingLike.map_ne_one_iff (since := "2024-11-10")] +MulEquivClass.map_ne_one_iff +attribute [deprecated EmbeddingLike.map_ne_zero_iff (since := "2024-11-10")] +AddEquivClass.map_ne_zero_iff + + namespace MulEquivClass variable (F) diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean index 404fdd46e25ad..d31f9773753a2 100644 --- a/Mathlib/Algebra/Group/Pointwise/Set/Card.lean +++ b/Mathlib/Algebra/Group/Pointwise/Set/Card.lean @@ -33,7 +33,13 @@ lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_ aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul]) -@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_mul_le := natCard_mul_le +@[to_additive] alias card_mul_le := natCard_mul_le + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated natCard_mul_le (since := "2024-09-30")] card_mul_le +attribute [deprecated natCard_add_le (since := "2024-09-30")] card_add_le + end Mul @@ -48,7 +54,12 @@ lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by rw [← image_inv, Nat.card_image_of_injective inv_injective] -@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_inv := natCard_inv +@[to_additive] alias card_inv := natCard_inv + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated natCard_inv (since := "2024-09-30")] card_inv +attribute [deprecated natCard_neg (since := "2024-09-30")] card_neg @[to_additive (attr := simp)] lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by simp [encard, PartENat.card] @@ -74,7 +85,12 @@ variable [Group G] {s t : Set G} lemma natCard_div_le : Nat.card (s / t) ≤ Nat.card s * Nat.card t := by rw [div_eq_mul_inv, ← natCard_inv t]; exact natCard_mul_le -@[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_div_le := natCard_div_le +@[to_additive] alias card_div_le := natCard_div_le + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated natCard_div_le (since := "2024-09-30")] card_div_le +attribute [deprecated natCard_sub_le (since := "2024-09-30")] card_sub_le variable [MulAction G α] @@ -86,9 +102,14 @@ lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s := lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s := Nat.card_image_of_injective (MulAction.injective a) _ -@[to_additive (attr := deprecated (since := "2024-09-30"))] +@[to_additive] alias card_smul_set := Cardinal.mk_smul_set +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated Cardinal.mk_smul_set (since := "2024-09-30")] card_smul_set +attribute [deprecated Cardinal.mk_vadd_set (since := "2024-09-30")] card_vadd_set + @[to_additive (attr := simp)] lemma encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard := by simp [encard, PartENat.card] diff --git a/Mathlib/Algebra/Module/LinearMap/Defs.lean b/Mathlib/Algebra/Module/LinearMap/Defs.lean index c6436036fb7c1..d4c25f58c52fb 100644 --- a/Mathlib/Algebra/Module/LinearMap/Defs.lean +++ b/Mathlib/Algebra/Module/LinearMap/Defs.lean @@ -596,14 +596,14 @@ variable [Semiring R] [Module R M] [Semiring S] [Module S M₂] [Module R M₃] variable {σ : R →+* S} /-- A `DistribMulActionHom` between two modules is a linear map. -/ -@[deprecated (since := "2024-11-08")] +@[deprecated "No deprecation message was provided." (since := "2024-11-08")] def toSemilinearMap (fₗ : M →ₑ+[σ.toMonoidHom] M₂) : M →ₛₗ[σ] M₂ := { fₗ with } instance : SemilinearMapClass (M →ₑ+[σ.toMonoidHom] M₂) σ M M₂ where /-- A `DistribMulActionHom` between two modules is a linear map. -/ -@[deprecated (since := "2024-11-08")] +@[deprecated "No deprecation message was provided." (since := "2024-11-08")] def toLinearMap (fₗ : M →+[R] M₃) : M →ₗ[R] M₃ := { fₗ with } diff --git a/Mathlib/Algebra/Order/Field/Power.lean b/Mathlib/Algebra/Order/Field/Power.lean index d363f2170a5c4..9cec9ad4fcc29 100644 --- a/Mathlib/Algebra/Order/Field/Power.lean +++ b/Mathlib/Algebra/Order/Field/Power.lean @@ -73,13 +73,13 @@ theorem zpow_injective (h₀ : 0 < a) (h₁ : a ≠ 1) : Injective (a ^ · : ℤ theorem zpow_inj (h₀ : 0 < a) (h₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n := zpow_right_inj₀ h₀ h₁ -@[deprecated (since := "2024-10-08")] +@[deprecated "No deprecation message was provided." (since := "2024-10-08")] theorem zpow_le_max_of_min_le {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : min a b ≤ c) : x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) := have : Antitone fun n : ℤ => x ^ (-n) := fun _ _ h => zpow_le_zpow_right₀ hx (neg_le_neg h) (this h).trans_eq this.map_min -@[deprecated (since := "2024-10-08")] +@[deprecated "No deprecation message was provided." (since := "2024-10-08")] theorem zpow_le_max_iff_min_le {x : α} (hx : 1 < x) {a b c : ℤ} : x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c := by simp_rw [le_max_iff, min_le_iff, zpow_le_zpow_iff_right₀ hx, neg_le_neg_iff] diff --git a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean index ceb329876b8e6..294f6be7c92df 100644 --- a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean +++ b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean @@ -48,7 +48,12 @@ lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) := lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) := (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t) -@[to_additive (attr := deprecated (since := "2024-11-13"))] alias Set.BddAbove.mul := BddAbove.mul +@[to_additive] alias Set.BddAbove.mul := BddAbove.mul + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated BddAbove.mul (since := "2024-11-13")] Set.BddAbove.mul +attribute [deprecated BddAbove.add (since := "2024-11-13")] Set.BddAbove.add @[to_additive] lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) : diff --git a/Mathlib/Analysis/Complex/Circle.lean b/Mathlib/Analysis/Complex/Circle.lean index 72e66ae46c1b7..e4a9a2e283278 100644 --- a/Mathlib/Analysis/Complex/Circle.lean +++ b/Mathlib/Analysis/Complex/Circle.lean @@ -41,17 +41,17 @@ open ComplexConjugate /-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. Please use `Circle` when referring to the circle as a type. -/ -@[deprecated (since := "2024-07-24")] +@[deprecated "No deprecation message was provided." (since := "2024-07-24")] def circle : Submonoid ℂ := Submonoid.unitSphere ℂ set_option linter.deprecated false in -@[deprecated (since := "2024-07-24")] +@[deprecated "No deprecation message was provided." (since := "2024-07-24")] theorem mem_circle_iff_abs {z : ℂ} : z ∈ circle ↔ abs z = 1 := mem_sphere_zero_iff_norm set_option linter.deprecated false in -@[deprecated (since := "2024-07-24")] +@[deprecated "No deprecation message was provided." (since := "2024-07-24")] theorem mem_circle_iff_normSq {z : ℂ} : z ∈ circle ↔ normSq z = 1 := by simp [Complex.abs, mem_circle_iff_abs] diff --git a/Mathlib/CategoryTheory/Adjunction/Limits.lean b/Mathlib/CategoryTheory/Adjunction/Limits.lean index dd86591976534..2db2c795ef2c2 100644 --- a/Mathlib/CategoryTheory/Adjunction/Limits.lean +++ b/Mathlib/CategoryTheory/Adjunction/Limits.lean @@ -92,7 +92,7 @@ lemma leftAdjoint_preservesColimits : PreservesColimitsOfSize.{v, u} F where ((adj.functorialityAdjunction _).homEquiv _ _)⟩ } } include adj in -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma leftAdjointPreservesColimits : PreservesColimitsOfSize.{v, u} F := adj.leftAdjoint_preservesColimits @@ -117,7 +117,7 @@ noncomputable instance (priority := 100) { reflects := fun t => ⟨(isColimitOfPreserves E.inv t).mapCoconeEquiv E.asEquivalence.unitIso.symm⟩ } } -@[deprecated (since := "2024-11-18")] +@[deprecated "No deprecation message was provided." (since := "2024-11-18")] lemma isEquivalenceReflectsColimits (E : D ⥤ C) [E.IsEquivalence] : ReflectsColimitsOfSize.{v, u} E := Functor.reflectsColimits_of_isEquivalence E @@ -216,7 +216,7 @@ lemma rightAdjoint_preservesLimits : PreservesLimitsOfSize.{v, u} G where ((adj.functorialityAdjunction' _).homEquiv _ _).symm⟩ } } include adj in -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma rightAdjointPreservesLimits : PreservesLimitsOfSize.{v, u} G := adj.rightAdjoint_preservesLimits @@ -240,7 +240,7 @@ noncomputable instance (priority := 100) { reflects := fun t => ⟨(isLimitOfPreserves E.inv t).mapConeEquiv E.asEquivalence.unitIso.symm⟩ } } -@[deprecated (since := "2024-11-18")] +@[deprecated "No deprecation message was provided." (since := "2024-11-18")] lemma isEquivalenceReflectsLimits (E : D ⥤ C) [E.IsEquivalence] : ReflectsLimitsOfSize.{v, u} E := Functor.reflectsLimits_of_isEquivalence E diff --git a/Mathlib/CategoryTheory/Idempotents/Karoubi.lean b/Mathlib/CategoryTheory/Idempotents/Karoubi.lean index 1c0f0936e00c6..d4b4fc8a4f69e 100644 --- a/Mathlib/CategoryTheory/Idempotents/Karoubi.lean +++ b/Mathlib/CategoryTheory/Idempotents/Karoubi.lean @@ -111,7 +111,7 @@ theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f @[simp] theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl -@[deprecated (since := "2024-07-15")] +@[deprecated "No deprecation message was provided." (since := "2024-07-15")] theorem id_eq {P : Karoubi C} : 𝟙 P = ⟨P.p, by repeat' rw [P.idem]⟩ := rfl /-- It is possible to coerce an object of `C` into an object of `Karoubi C`. diff --git a/Mathlib/CategoryTheory/Limits/Creates.lean b/Mathlib/CategoryTheory/Limits/Creates.lean index 148eafbe8efa1..9769ea2520000 100644 --- a/Mathlib/CategoryTheory/Limits/Creates.lean +++ b/Mathlib/CategoryTheory/Limits/Creates.lean @@ -332,7 +332,7 @@ instance (priority := 100) preservesLimit_of_createsLimit_and_hasLimit (K : J ((liftedLimitMapsToOriginal (limit.isLimit _)).symm ≪≫ (Cones.functoriality K F).mapIso ((liftedLimitIsLimit (limit.isLimit _)).uniqueUpToIso t))⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitOfCreatesLimitAndHasLimit (K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] [HasLimit (K ⋙ F)] : PreservesLimit K F := preservesLimit_of_createsLimit_and_hasLimit _ _ @@ -342,7 +342,7 @@ lemma preservesLimitOfCreatesLimitAndHasLimit (K : J ⥤ C) (F : C ⥤ D) instance (priority := 100) preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape (F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F where -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape (F : C ⥤ D) [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F := @@ -354,7 +354,7 @@ instance (priority := 100) preservesLimits_of_createsLimits_and_hasLimits (F : C [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] : PreservesLimitsOfSize.{w, w'} F where -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitsOfCreatesLimitsAndHasLimits (F : C ⥤ D) [CreatesLimitsOfSize.{w, w'} F] [HasLimitsOfSize.{w, w'} D] : PreservesLimitsOfSize.{w, w'} F := @@ -466,7 +466,7 @@ instance (priority := 100) preservesColimit_of_createsColimit_and_hasColimit (K (Cocones.functoriality K F).mapIso ((liftedColimitIsColimit (colimit.isColimit _)).uniqueUpToIso t))⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesColimitOfCreatesColimitAndHasColimit (K : J ⥤ C) (F : C ⥤ D) [CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F := preservesColimit_of_createsColimit_and_hasColimit _ _ @@ -477,7 +477,7 @@ instance (priority := 100) preservesColimitOfShape_of_createsColimitsOfShape_and (F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] : PreservesColimitsOfShape J F where -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape (F : C ⥤ D) [CreatesColimitsOfShape J F] [HasColimitsOfShape J D] : PreservesColimitsOfShape J F := @@ -489,7 +489,7 @@ instance (priority := 100) preservesColimits_of_createsColimits_and_hasColimits [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] : PreservesColimitsOfSize.{w, w'} F where -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesColimitsOfCreatesColimitsAndHasColimits (F : C ⥤ D) [CreatesColimitsOfSize.{w, w'} F] [HasColimitsOfSize.{w, w'} D] : PreservesColimitsOfSize.{w, w'} F := diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean index 357916b1fe01e..603001e9e6ce6 100644 --- a/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean +++ b/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean @@ -362,7 +362,7 @@ lemma preservesLimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D) change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c) exact isLimitOfPreserves _ hc⟩⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D) (H : ∀ k : K, PreservesLimit G (F ⋙ (evaluation K C).obj k : D ⥤ C)) : PreservesLimit G F := @@ -374,7 +374,7 @@ lemma preservesLimitsOfShape_of_evaluation (F : D ⥤ K ⥤ C) (J : Type*) [Cate PreservesLimitsOfShape J F := ⟨fun {G} => preservesLimit_of_evaluation F G fun _ => PreservesLimitsOfShape.preservesLimit⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitsOfShapeOfEvaluation (F : D ⥤ K ⥤ C) (J : Type*) [Category J] (H : ∀ k : K, PreservesLimitsOfShape J (F ⋙ (evaluation K C).obj k)) : PreservesLimitsOfShape J F := @@ -387,7 +387,7 @@ lemma preservesLimits_of_evaluation (F : D ⥤ K ⥤ C) ⟨fun {L} _ => preservesLimitsOfShape_of_evaluation F L fun _ => PreservesLimitsOfSize.preservesLimitsOfShape⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesLimitsOfEvaluation (F : D ⥤ K ⥤ C) (H : ∀ k : K, PreservesLimitsOfSize.{w', w} (F ⋙ (evaluation K C).obj k)) : PreservesLimitsOfSize.{w', w} F := @@ -412,7 +412,7 @@ lemma preservesColimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D) change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c) exact isColimitOfPreserves _ hc⟩⟩ -@[deprecated (since := "2024-11-19")] +@[deprecated "No deprecation message was provided." (since := "2024-11-19")] lemma preservesColimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D) (H : ∀ k, PreservesColimit G (F ⋙ (evaluation K C).obj k)) : PreservesColimit G F := preservesColimit_of_evaluation _ _ H diff --git a/Mathlib/Data/Complex/Abs.lean b/Mathlib/Data/Complex/Abs.lean index 99319c9d298b3..18f2f48e1b525 100644 --- a/Mathlib/Data/Complex/Abs.lean +++ b/Mathlib/Data/Complex/Abs.lean @@ -199,7 +199,7 @@ theorem abs_im_div_abs_le_one (z : ℂ) : |z.im / Complex.abs z| ≤ 1 := @[simp, norm_cast] lemma abs_intCast (n : ℤ) : abs n = |↑n| := by rw [← ofReal_intCast, abs_ofReal] -@[deprecated (since := "2024-02-14")] +@[deprecated "No deprecation message was provided." (since := "2024-02-14")] lemma int_cast_abs (n : ℤ) : |↑n| = Complex.abs n := (abs_intCast _).symm theorem normSq_eq_abs (x : ℂ) : normSq x = (Complex.abs x) ^ 2 := by diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 21c9e27353985..4fcd646907769 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1115,7 +1115,7 @@ lemma succAbove_ne_last {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last _) lemma succAbove_last_apply (i : Fin n) : succAbove (last n) i = castSucc i := by rw [succAbove_last] -@[deprecated (since := "2024-05-30")] +@[deprecated "No deprecation message was provided." (since := "2024-05-30")] lemma succAbove_lt_ge (p : Fin (n + 1)) (i : Fin n) : castSucc i < p ∨ p ≤ castSucc i := Nat.lt_or_ge (castSucc i) p diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 4e3ce8533a890..3f51c9f665d12 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -34,7 +34,7 @@ universe u v w variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {l₁ l₂ : List α} /-- `≤` implies not `>` for lists. -/ -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem le_eq_not_gt [LT α] : ∀ l₁ l₂ : List α, (l₁ ≤ l₂) = ¬l₂ < l₁ := fun _ _ => rfl -- Porting note: Delete this attribute @@ -496,7 +496,7 @@ theorem get_tail (l : List α) (i) (h : i < l.tail.length) l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩ := by cases l <;> [cases h; rfl] -@[deprecated (since := "2024-08-22")] +@[deprecated "No deprecation message was provided." (since := "2024-08-22")] theorem get_cons {l : List α} {a : α} {n} (hl) : (a :: l).get ⟨n, hl⟩ = if hn : n = 0 then a else l.get ⟨n - 1, by contrapose! hl; rw [length_cons]; omega⟩ := @@ -627,7 +627,7 @@ lemma cons_sublist_cons' {a b : α} : a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l theorem sublist_cons_of_sublist (a : α) (h : l₁ <+ l₂) : l₁ <+ a :: l₂ := h.cons _ -@[deprecated (since := "2024-04-07")] +@[deprecated "No deprecation message was provided." (since := "2024-04-07")] theorem sublist_of_cons_sublist_cons {a} (h : a :: l₁ <+ a :: l₂) : l₁ <+ l₂ := h.of_cons_cons @[deprecated (since := "2024-04-07")] alias cons_sublist_cons_iff := cons_sublist_cons @@ -2281,7 +2281,7 @@ theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs simp; omega set_option linter.deprecated false in -@[deprecated (since := "2024-07-25")] +@[deprecated "No deprecation message was provided." (since := "2024-07-25")] theorem sizeOf_dropSlice_lt [SizeOf α] (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) : SizeOf.sizeOf (List.dropSlice i j xs) < SizeOf.sizeOf xs := by induction xs generalizing i j hj with diff --git a/Mathlib/Data/List/Flatten.lean b/Mathlib/Data/List/Flatten.lean index f6fbc8e3044fc..797ba9dc5c297 100644 --- a/Mathlib/Data/List/Flatten.lean +++ b/Mathlib/Data/List/Flatten.lean @@ -158,7 +158,8 @@ theorem append_flatten_map_append (L : List (List α)) (x : List α) : @[deprecated (since := "2024-10-15")] alias append_join_map_append := append_flatten_map_append -@[deprecated (since := "2024-08-15")] theorem sublist_join {l} {L : List (List α)} (h : l ∈ L) : +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] +theorem sublist_join {l} {L : List (List α)} (h : l ∈ L) : l <+ L.flatten := sublist_flatten_of_mem h diff --git a/Mathlib/Data/List/Indexes.lean b/Mathlib/Data/List/Indexes.lean index a1b935a65e0cc..fdbe9168bfa47 100644 --- a/Mathlib/Data/List/Indexes.lean +++ b/Mathlib/Data/List/Indexes.lean @@ -89,7 +89,7 @@ theorem mapIdx_eq_ofFn (l : List α) (f : ℕ → α → β) : section deprecated /-- Lean3 `map_with_index` helper function -/ -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected def oldMapIdxCore (f : ℕ → α → β) : ℕ → List α → List β | _, [] => [] | k, a :: as => f k a :: List.oldMapIdxCore f (k + 1) as @@ -97,12 +97,12 @@ protected def oldMapIdxCore (f : ℕ → α → β) : ℕ → List α → List set_option linter.deprecated false in /-- Given a function `f : ℕ → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list `[f 0 a₀, f 1 a₁, ...]`. -/ -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected def oldMapIdx (f : ℕ → α → β) (as : List α) : List β := List.oldMapIdxCore f 0 as set_option linter.deprecated false in -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected theorem oldMapIdxCore_eq (l : List α) (f : ℕ → α → β) (n : ℕ) : l.oldMapIdxCore f n = l.oldMapIdx fun i a ↦ f (i + n) a := by induction' l with hd tl hl generalizing f n @@ -111,7 +111,7 @@ protected theorem oldMapIdxCore_eq (l : List α) (f : ℕ → α → β) (n : simp only [List.oldMapIdxCore, hl, Nat.add_left_comm, Nat.add_comm, Nat.add_zero] set_option linter.deprecated false in -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected theorem oldMapIdxCore_append : ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α), List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂ := by @@ -139,7 +139,7 @@ protected theorem oldMapIdxCore_append : ∀ (f : ℕ → α → β) (n : ℕ) ( rw [Nat.add_assoc]; simp only [Nat.add_comm] set_option linter.deprecated false in -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected theorem oldMapIdx_append : ∀ (f : ℕ → α → β) (l : List α) (e : α), List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e] := by intros f l e @@ -148,7 +148,7 @@ protected theorem oldMapIdx_append : ∀ (f : ℕ → α → β) (l : List α) ( simp only [Nat.zero_add]; rfl set_option linter.deprecated false in -@[deprecated (since := "2024-08-15")] +@[deprecated "No deprecation message was provided." (since := "2024-08-15")] protected theorem new_def_eq_old_def : ∀ (f : ℕ → α → β) (l : List α), l.mapIdx f = List.oldMapIdx f l := by intro f diff --git a/Mathlib/Data/List/Lex.lean b/Mathlib/Data/List/Lex.lean index fef097d96a69f..69566d9aa5d91 100644 --- a/Mathlib/Data/List/Lex.lean +++ b/Mathlib/Data/List/Lex.lean @@ -99,7 +99,7 @@ instance isAsymm (r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Le | _, _, Lex.cons _, Lex.rel h₂ => asymm h₂ h₂ | _, _, Lex.cons h₁, Lex.cons h₂ => aux _ _ h₁ h₂ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance isStrictTotalOrder (r : α → α → Prop) [IsStrictTotalOrder α r] : IsStrictTotalOrder (List α) (Lex r) := { isStrictWeakOrder_of_isOrderConnected with } diff --git a/Mathlib/Data/List/Pairwise.lean b/Mathlib/Data/List/Pairwise.lean index 4682916a610a0..be4f87bb84be6 100644 --- a/Mathlib/Data/List/Pairwise.lean +++ b/Mathlib/Data/List/Pairwise.lean @@ -50,7 +50,8 @@ theorem Pairwise.set_pairwise (hl : Pairwise R l) (hr : Symmetric R) : { x | x hl.forall hr -- Porting note: Duplicate of `pairwise_map` but with `f` explicit. -@[deprecated (since := "2024-02-25")] theorem pairwise_map' (f : β → α) : +@[deprecated "No deprecation message was provided." (since := "2024-02-25")] +theorem pairwise_map' (f : β → α) : ∀ {l : List β}, Pairwise R (map f l) ↔ Pairwise (R on f) l | [] => by simp only [map, Pairwise.nil] | b :: l => by diff --git a/Mathlib/Data/List/Permutation.lean b/Mathlib/Data/List/Permutation.lean index 2ce7b4ce525f3..3e0073e3e2049 100644 --- a/Mathlib/Data/List/Permutation.lean +++ b/Mathlib/Data/List/Permutation.lean @@ -419,7 +419,7 @@ theorem length_permutations'Aux (s : List α) (x : α) : · simp · simpa using IH -@[deprecated (since := "2024-06-12")] +@[deprecated "No deprecation message was provided." (since := "2024-06-12")] theorem permutations'Aux_get_zero (s : List α) (x : α) (hn : 0 < length (permutations'Aux x s) := (by simp)) : (permutations'Aux x s).get ⟨0, hn⟩ = x :: s := diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean index 85ee5070c28b1..20c3db731c333 100644 --- a/Mathlib/Data/Nat/Defs.lean +++ b/Mathlib/Data/Nat/Defs.lean @@ -1092,7 +1092,7 @@ lemma sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by lemma one_mod_eq_one : ∀ {n : ℕ}, 1 % n = 1 ↔ n ≠ 1 | 0 | 1 | n + 2 => by simp -@[deprecated (since := "2024-08-28")] +@[deprecated "No deprecation message was provided." (since := "2024-08-28")] lemma one_mod_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → 1 % n = 1 := one_mod_eq_one.mpr lemma dvd_sub_mod (k : ℕ) : n ∣ k - k % n := diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean index 1f4a5da3be5cd..e7008d4c67fbf 100644 --- a/Mathlib/Data/Set/Pointwise/SMul.lean +++ b/Mathlib/Data/Set/Pointwise/SMul.lean @@ -415,8 +415,13 @@ lemma disjoint_smul_set_left : Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t lemma disjoint_smul_set_right : Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t := by simpa using disjoint_smul_set (a := a) (s := a⁻¹ • s) -@[to_additive (attr := deprecated (since := "2024-10-18"))] -alias smul_set_disjoint_iff := disjoint_smul_set +@[to_additive] alias smul_set_disjoint_iff := disjoint_smul_set + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated disjoint_smul_set (since := "2024-10-18")] smul_set_disjoint_iff +attribute [deprecated disjoint_vadd_set (since := "2024-10-18")] vadd_set_disjoint_iff + end Group diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean index 2e75e96025a44..bbaa5b239fbfe 100644 --- a/Mathlib/Data/Setoid/Basic.lean +++ b/Mathlib/Data/Setoid/Basic.lean @@ -36,12 +36,12 @@ attribute [trans] Setoid.trans variable {α : Type*} {β : Type*} /-- A version of `Setoid.r` that takes the equivalence relation as an explicit argument. -/ -@[deprecated (since := "2024-08-29")] +@[deprecated "No deprecation message was provided." (since := "2024-08-29")] def Setoid.Rel (r : Setoid α) : α → α → Prop := @Setoid.r _ r set_option linter.deprecated false in -@[deprecated (since := "2024-10-09")] +@[deprecated "No deprecation message was provided." (since := "2024-10-09")] instance Setoid.decidableRel (r : Setoid α) [h : DecidableRel r.r] : DecidableRel r.Rel := h diff --git a/Mathlib/Deprecated/AlgebraClasses.lean b/Mathlib/Deprecated/AlgebraClasses.lean index cc26f497422b2..bb6f948871913 100644 --- a/Mathlib/Deprecated/AlgebraClasses.lean +++ b/Mathlib/Deprecated/AlgebraClasses.lean @@ -25,16 +25,16 @@ universe u v variable {α : Sort u} -@[deprecated (since := "2024-09-11")] +@[deprecated "No deprecation message was provided." (since := "2024-09-11")] class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop where left_cancel : ∀ a b c, op a b = op a c → b = c -@[deprecated (since := "2024-09-11")] +@[deprecated "No deprecation message was provided." (since := "2024-09-11")] class IsRightCancel (α : Sort u) (op : α → α → α) : Prop where right_cancel : ∀ a b c, op a b = op c b → a = c /-- `IsTotalPreorder X r` means that the binary relation `r` on `X` is total and a preorder. -/ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] class IsTotalPreorder (α : Sort u) (r : α → α → Prop) extends IsTrans α r, IsTotal α r : Prop /-- Every total pre-order is a pre-order. -/ @@ -45,11 +45,11 @@ instance (priority := 100) isTotalPreorder_isPreorder (α : Sort u) (r : α → /-- `IsIncompTrans X lt` means that for `lt` a binary relation on `X`, the incomparable relation `fun a b => ¬ lt a b ∧ ¬ lt b a` is transitive. -/ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] class IsIncompTrans (α : Sort u) (lt : α → α → Prop) : Prop where incomp_trans : ∀ a b c, ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance (priority := 100) (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] : IsIncompTrans α lt := { ‹IsStrictWeakOrder α lt› with } @@ -59,7 +59,7 @@ variable {r : α → α → Prop} local infixl:50 " ≺ " => r -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem incomp_trans [IsIncompTrans α r] {a b c : α} : ¬a ≺ b ∧ ¬b ≺ a → ¬b ≺ c ∧ ¬c ≺ b → ¬a ≺ c ∧ ¬c ≺ a := IsIncompTrans.incomp_trans _ _ _ @@ -68,7 +68,8 @@ section ExplicitRelationVariants variable (r) -@[elab_without_expected_type, deprecated (since := "2024-07-30")] +@[elab_without_expected_type, + deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem incomp_trans_of [IsIncompTrans α r] {a b c : α} : ¬a ≺ b ∧ ¬b ≺ a → ¬b ≺ c ∧ ¬c ≺ b → ¬a ≺ c ∧ ¬c ≺ a := incomp_trans @@ -85,32 +86,32 @@ variable {r : α → α → Prop} local infixl:50 " ≺ " => r -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] def Equiv (a b : α) : Prop := ¬a ≺ b ∧ ¬b ≺ a local infixl:50 " ≈ " => @Equiv _ r -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem esymm {a b : α} : a ≈ b → b ≈ a := fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem not_lt_of_equiv {a b : α} : a ≈ b → ¬a ≺ b := fun h => h.1 -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem not_lt_of_equiv' {a b : α} : a ≈ b → ¬b ≺ a := fun h => h.2 variable [IsStrictWeakOrder α r] -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem erefl (a : α) : a ≈ a := ⟨irrefl a, irrefl a⟩ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem etrans {a b c : α} : a ≈ b → b ≈ c → a ≈ c := incomp_trans -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance isEquiv : IsEquiv α (@Equiv _ r) where refl := erefl trans _ _ _ := etrans @@ -123,7 +124,7 @@ notation:50 a " ≈[" lt "]" b:50 => @Equiv _ lt a b end StrictWeakOrder -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le : α → α → Prop} {lt : α → α → Prop} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ a b, lt a b ↔ ¬le b a) : IsStrictWeakOrder α lt := @@ -149,20 +150,20 @@ section LinearOrder variable {α : Type*} [LinearOrder α] set_option linter.deprecated false in -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance : IsTotalPreorder α (· ≤ ·) where trans := @le_trans _ _ total := le_total set_option linter.deprecated false in -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance isStrictWeakOrder_of_linearOrder : IsStrictWeakOrder α (· < ·) := have : IsTotalPreorder α (· ≤ ·) := by infer_instance -- Porting note: added isStrictWeakOrder_of_isTotalPreorder lt_iff_not_ge end LinearOrder -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem lt_of_lt_of_incomp {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] : ∀ {a b c}, lt a b → ¬lt b c ∧ ¬lt c b → lt a c := @fun a b c hab ⟨nbc, ncb⟩ => @@ -171,7 +172,7 @@ theorem lt_of_lt_of_incomp {α : Sort u} {lt : α → α → Prop} [IsStrictWeak have : ¬lt a b ∧ ¬lt b a := incomp_trans_of lt ⟨nac, nca⟩ ⟨ncb, nbc⟩ absurd hab this.1 -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem lt_of_incomp_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] : ∀ {a b c}, ¬lt a b ∧ ¬lt b a → lt b c → lt a c := @fun a b c ⟨nab, nba⟩ hbc => @@ -180,7 +181,7 @@ theorem lt_of_incomp_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictWeak have : ¬lt b c ∧ ¬lt c b := incomp_trans_of lt ⟨nba, nab⟩ ⟨nac, nca⟩ absurd hbc this.1 -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} : ¬lt a b ∧ ¬lt b a → a = b := fun ⟨nab, nba⟩ => match trichotomous_of lt a b with @@ -188,17 +189,17 @@ theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α | Or.inr (Or.inl hab) => hab | Or.inr (Or.inr hba) => absurd hba nba -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem eq_of_eqv_lt {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b} : a ≈[lt]b → a = b := eq_of_incomp -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem incomp_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) : ¬lt a b ∧ ¬lt b a ↔ a = b := Iff.intro eq_of_incomp fun hab => hab ▸ And.intro (irrefl_of lt a) (irrefl_of lt a) -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem eqv_lt_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b) : a ≈[lt]b ↔ a = b := incomp_iff_eq a b diff --git a/Mathlib/Deprecated/ByteArray.lean b/Mathlib/Deprecated/ByteArray.lean index c199be41b3f7c..b7146dbf289c6 100644 --- a/Mathlib/Deprecated/ByteArray.lean +++ b/Mathlib/Deprecated/ByteArray.lean @@ -19,7 +19,7 @@ set_option linter.deprecated false namespace Nat /-- A well-ordered relation for "upwards" induction on the natural numbers up to some bound `ub`. -/ -@[deprecated (since := "2024-08-19")] +@[deprecated "No deprecation message was provided." (since := "2024-08-19")] def Up (ub a i : Nat) := i < a ∧ i < ub theorem Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩ @@ -28,13 +28,13 @@ theorem Up.WF (ub) : WellFounded (Up ub) := Subrelation.wf (h₂ := (measure (ub - ·)).wf) fun ⟨ia, iu⟩ ↦ Nat.sub_lt_sub_left iu ia /-- A well-ordered relation for "upwards" induction on the natural numbers up to some bound `ub`. -/ -@[deprecated (since := "2024-08-19")] +@[deprecated "No deprecation message was provided." (since := "2024-08-19")] def upRel (ub : Nat) : WellFoundedRelation Nat := ⟨Up ub, Up.WF ub⟩ end Nat /-- A terminal byte slice, a suffix of a byte array. -/ -@[deprecated (since := "2024-08-19")] +@[deprecated "No deprecation message was provided." (since := "2024-08-19")] structure ByteSliceT := (arr : ByteArray) (off : Nat) namespace ByteSliceT @@ -66,7 +66,7 @@ def toArray : ByteSlice → ByteArray universe u v /-- The inner loop of the `forIn` implementation for byte slices. -/ -@[deprecated (since := "2024-08-19")] +@[deprecated "No deprecation message was provided." (since := "2024-08-19")] def forIn.loop {m : Type u → Type v} {β : Type u} [Monad m] (f : UInt8 → β → m (ForInStep β)) (arr : ByteArray) (off _end : Nat) (i : Nat) (b : β) : m β := if h : i < _end then do @@ -75,7 +75,7 @@ def forIn.loop {m : Type u → Type v} {β : Type u} [Monad m] (f : UInt8 → β | ForInStep.yield b => have := Nat.Up.next h; loop f arr off _end (i+1) b else pure b -@[deprecated (since := "2024-08-19")] +@[deprecated "No deprecation message was provided." (since := "2024-08-19")] instance {m : Type u → Type v} : ForIn m ByteSlice UInt8 := ⟨fun ⟨arr, off, len⟩ b f ↦ forIn.loop f arr off (off + len) off b⟩ diff --git a/Mathlib/Deprecated/Combinator.lean b/Mathlib/Deprecated/Combinator.lean index 5c79bf0837a59..366fd5997f982 100644 --- a/Mathlib/Deprecated/Combinator.lean +++ b/Mathlib/Deprecated/Combinator.lean @@ -15,8 +15,11 @@ namespace Combinator universe u v w variable {α : Sort u} {β : Sort v} {γ : Sort w} -@[deprecated (since := "2024-07-27")] def I (a : α) := a -@[deprecated (since := "2024-07-27")] def K (a : α) (_b : β) := a -@[deprecated (since := "2024-07-27")] def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z) +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] +def I (a : α) := a +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] +def K (a : α) (_b : β) := a +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] +def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z) end Combinator diff --git a/Mathlib/Deprecated/Equiv.lean b/Mathlib/Deprecated/Equiv.lean index 74bc9b68ecdd3..b31fe578386cc 100644 --- a/Mathlib/Deprecated/Equiv.lean +++ b/Mathlib/Deprecated/Equiv.lean @@ -21,10 +21,10 @@ variable {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α set_option linter.deprecated false -@[deprecated (since := "2024-09-11")] +@[deprecated "No deprecation message was provided." (since := "2024-09-11")] instance [IsLeftCancel α₁ f] : IsLeftCancel β₁ (e.arrowCongr (e.arrowCongr e) f) := ⟨e.surjective.forall₃.2 fun x y z => by simpa using @IsLeftCancel.left_cancel _ f _ x y z⟩ -@[deprecated (since := "2024-09-11")] +@[deprecated "No deprecation message was provided." (since := "2024-09-11")] instance [IsRightCancel α₁ f] : IsRightCancel β₁ (e.arrowCongr (e.arrowCongr e) f) := ⟨e.surjective.forall₃.2 fun x y z => by simpa using @IsRightCancel.right_cancel _ f _ x y z⟩ diff --git a/Mathlib/Deprecated/LazyList.lean b/Mathlib/Deprecated/LazyList.lean index 7a9b820336505..5ba81d38999a8 100644 --- a/Mathlib/Deprecated/LazyList.lean +++ b/Mathlib/Deprecated/LazyList.lean @@ -24,7 +24,7 @@ namespace LazyList open Function /-- Isomorphism between strict and lazy lists. -/ -@[deprecated (since := "2024-07-22")] +@[deprecated "No deprecation message was provided." (since := "2024-07-22")] def listEquivLazyList (α : Type*) : List α ≃ LazyList α where toFun := LazyList.ofList invFun := LazyList.toList @@ -39,12 +39,12 @@ def listEquivLazyList (α : Type*) : List α ≃ LazyList α where · simp [toList, ofList] · simpa [ofList, toList] -@[deprecated (since := "2024-07-22")] +@[deprecated "No deprecation message was provided." (since := "2024-07-22")] instance : Traversable LazyList where map := @LazyList.traverse Id _ traverse := @LazyList.traverse -@[deprecated (since := "2024-07-22")] +@[deprecated "No deprecation message was provided." (since := "2024-07-22")] instance : LawfulTraversable LazyList := by apply Equiv.isLawfulTraversable' listEquivLazyList <;> intros <;> ext <;> rename_i f xs · induction xs using LazyList.rec with @@ -71,7 +71,7 @@ instance : LawfulTraversable LazyList := by Function.comp_def, Thunk.pure, ofList] | mk _ ih => apply ih -@[deprecated (since := "2024-07-22"), simp] +@[deprecated "No deprecation message was provided." (since := "2024-07-22"), simp] theorem bind_singleton {α} (x : LazyList α) : x.bind singleton = x := by induction x using LazyList.rec (motive_2 := fun xs => xs.get.bind singleton = xs.get) with | nil => simp [LazyList.bind] @@ -81,7 +81,7 @@ theorem bind_singleton {α} (x : LazyList α) : x.bind singleton = x := by simp [ih] | mk f ih => simp_all -@[deprecated (since := "2024-07-22")] +@[deprecated "No deprecation message was provided." (since := "2024-07-22")] instance : LawfulMonad LazyList := LawfulMonad.mk' (id_map := by intro α xs diff --git a/Mathlib/Deprecated/Logic.lean b/Mathlib/Deprecated/Logic.lean index f88642ec745a7..52d03620dc96a 100644 --- a/Mathlib/Deprecated/Logic.lean +++ b/Mathlib/Deprecated/Logic.lean @@ -37,43 +37,43 @@ local infix:65 (priority := high) " + " => g def Commutative := ∀ a b, a * b = b * a @[deprecated Std.Associative (since := "2024-09-13")] def Associative := ∀ a b c, (a * b) * c = a * (b * c) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def LeftIdentity := ∀ a, one * a = a -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def RightIdentity := ∀ a, a * one = a -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def RightInverse := ∀ a, a * a⁻¹ = one -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def LeftCancelative := ∀ a b c, a * b = a * c → b = c -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def RightCancelative := ∀ a b c, a * b = c * b → a = c -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def LeftDistributive := ∀ a b c, a * (b + c) = a * b + a * c -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def RightDistributive := ∀ a b c, (a + b) * c = a * c + b * c end Binary @[deprecated (since := "2024-09-03")] alias not_of_eq_false := of_eq_false -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem cast_proof_irrel {β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl @[deprecated (since := "2024-09-03")] alias eq_rec_heq := eqRec_heq @[deprecated (since := "2024-09-03")] alias heq_prop := proof_irrel_heq -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem heq_of_eq_rec_left {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} : (e : a = a') → (h₂ : Eq.rec (motive := fun a _ ↦ φ a) p₁ e = p₂) → HEq p₁ p₂ | rfl, rfl => HEq.rfl -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem heq_of_eq_rec_right {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} : (e : a' = a) → (h₂ : p₁ = Eq.rec (motive := fun a _ ↦ φ a) p₂ e) → HEq p₁ p₂ | rfl, rfl => HEq.rfl -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem of_heq_true {a : Prop} (h : HEq a True) : a := of_eq_true (eq_of_heq h) -@[deprecated (since := "2024-09-03")] +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] theorem eq_rec_compose {α β φ : Sort u} : ∀ (p₁ : β = φ) (p₂ : α = β) (a : α), (Eq.recOn p₁ (Eq.recOn p₂ a : β) : φ) = Eq.recOn (Eq.trans p₂ p₁) a @@ -114,20 +114,20 @@ theorem iff_self_iff (a : Prop) : (a ↔ a) ↔ True := iff_of_eq (iff_self _) /- decidable -/ -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem decide_True' (h : Decidable True) : decide True = true := by simp -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem decide_False' (h : Decidable False) : decide False = false := by simp namespace Decidable -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def recOn_true [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃) : Decidable.recOn h h₂ h₁ := cast (by match h with | .isTrue _ => rfl) h₄ -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def recOn_false [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃) : Decidable.recOn h h₂ h₁ := cast (by match h with | .isFalse _ => rfl) h₄ @@ -145,25 +145,25 @@ end Decidable @[deprecated (since := "2024-09-03")] alias decidableTrue := instDecidableTrue @[deprecated (since := "2024-09-03")] alias decidableFalse := instDecidableFalse -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def IsDecEq {α : Sort u} (p : α → α → Bool) : Prop := ∀ ⦃x y : α⦄, p x y = true → x = y -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def IsDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def decidableEq_of_bool_pred {α : Sort u} {p : α → α → Bool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) : DecidableEq α | x, y => if hp : p x y = true then isTrue (h₁ hp) else isFalse (fun hxy : x = y ↦ absurd (h₂ y) (by rwa [hxy] at hp)) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem decidableEq_inl_refl {α : Sort u} [h : DecidableEq α] (a : α) : h a a = isTrue (Eq.refl a) := match h a a with | isTrue _ => rfl -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a b : α} (n : a ≠ b) : h a b = isFalse n := match h a b with @@ -171,7 +171,7 @@ theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a b : α} /- subsingleton -/ -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem rec_subsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ h : p, Subsingleton (h₁ h)] [h₄ : ∀ h : ¬p, Subsingleton (h₂ h)] : Subsingleton (Decidable.recOn h h₂ h₁) := @@ -179,15 +179,15 @@ theorem rec_subsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h | isTrue h => h₃ h | isFalse h => h₄ h -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem imp_of_if_pos {c t e : Prop} [Decidable c] (h : ite c t e) (hc : c) : t := (if_pos hc ▸ h :) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem imp_of_if_neg {c t e : Prop} [Decidable c] (h : ite c t e) (hnc : ¬c) : e := (if_neg hnc ▸ h :) -@[deprecated (since := "2024-09-11")] +@[deprecated "No deprecation message was provided." (since := "2024-09-11")] theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ h : c, x (Iff.mpr h_c h) = u h) @@ -199,7 +199,7 @@ theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : | isFalse h₁, isTrue h₂ => absurd h₂ (Iff.mp (not_congr h_c) h₁) | isTrue h₁, isFalse h₂ => absurd h₁ (Iff.mpr (not_congr h_c) h₂) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem if_ctx_congr_prop {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : ite b x y ↔ ite c u v := match dec_b, dec_c with @@ -209,12 +209,12 @@ theorem if_ctx_congr_prop {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : De | isTrue h₁, isFalse h₂ => absurd h₁ (Iff.mpr (not_congr h_c) h₂) -- @[congr] -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem if_congr_prop {b c x y u v : Prop} [Decidable b] [Decidable c] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : ite b x y ↔ ite c u v := if_ctx_congr_prop h_c (fun _ ↦ h_t) (fun _ ↦ h_e) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c) (h_t : c → (x ↔ u)) -- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed, -- this should be changed back to: @@ -222,7 +222,7 @@ theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c (h_e : ¬c → (y ↔ v)) : ite b x y ↔ @ite _ c (decidable_of_decidable_of_iff h_c) u v := if_ctx_congr_prop (dec_c := decidable_of_decidable_of_iff h_c) h_c h_t h_e -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem if_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c) (h_t : x ↔ u) -- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed, -- this should be changed back to: @@ -230,7 +230,7 @@ theorem if_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c) (h (h_e : y ↔ v) : ite b x y ↔ (@ite _ c (decidable_of_decidable_of_iff h_c) u v) := if_ctx_simp_congr_prop h_c (fun _ ↦ h_t) (fun _ ↦ h_e) -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem dif_ctx_simp_congr {α : Sort u} {b c : Prop} [Decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ h : c, x (Iff.mpr h_c h) = u h) @@ -241,31 +241,31 @@ theorem dif_ctx_simp_congr {α : Sort u} {b c : Prop} [Decidable b] dite b x y = @dite _ c (decidable_of_decidable_of_iff h_c) u v := dif_ctx_congr (dec_c := decidable_of_decidable_of_iff h_c) h_c h_t h_e -@[deprecated (since := "2024-09-03")] +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] def AsTrue (c : Prop) [Decidable c] : Prop := if c then True else False -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib def AsFalse (c : Prop) [Decidable c] : Prop := if c then False else True -@[deprecated (since := "2024-09-03")] +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] theorem AsTrue.get {c : Prop} [h₁ : Decidable c] (_ : AsTrue c) : c := match h₁ with | isTrue h_c => h_c /- Equalities for rewriting let-expressions -/ -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) (h : a₁ = a₂) : (let x : α := a₁; b x) = (let x : α := a₂; b x) := congrArg b h -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : ∀ x : α, β x) (h : a₁ = a₂) : HEq (let x : α := a₁; b x) (let x : α := a₂; b x) := by cases h; rfl -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : ∀ x : α, β x} (h : ∀ x, b₁ x = b₂ x) : (let x : α := a; b₁ x) = (let x : α := a; b₂ x) := by exact h _ ▸ rfl -@[deprecated (since := "2024-09-03")] -- unused in Mathlib +@[deprecated "No deprecation message was provided." (since := "2024-09-03")] -- unused in Mathlib theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} (h₁ : a₁ = a₂) (h₂ : ∀ x, b₁ x = b₂ x) : (let x : α := a₁; b₁ x) = (let x : α := a₂; b₂ x) := by simp [h₁, h₂] diff --git a/Mathlib/Deprecated/NatLemmas.lean b/Mathlib/Deprecated/NatLemmas.lean index 37fd557b3fec3..81b124b4476cd 100644 --- a/Mathlib/Deprecated/NatLemmas.lean +++ b/Mathlib/Deprecated/NatLemmas.lean @@ -28,7 +28,7 @@ namespace Nat /-! successor and predecessor -/ -@[deprecated (since := "2024-08-23")] +@[deprecated "No deprecation message was provided." (since := "2024-08-23")] def discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : ∀ m, n = succ m → B) : B := by induction n with | zero => exact H1 rfl @@ -36,7 +36,7 @@ def discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : ∀ m, n = succ -- Unused in Mathlib; -- if downstream projects find this essential please copy it or remove the deprecation. -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem one_eq_succ_zero : 1 = succ 0 := rfl @@ -44,7 +44,7 @@ theorem one_eq_succ_zero : 1 = succ 0 := -- Unused in Mathlib; -- if downstream projects find this essential please copy it or remove the deprecation. -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] def subInduction {P : ℕ → ℕ → Sort u} (H1 : ∀ m, P 0 m) (H2 : ∀ n, P (succ n) 0) (H3 : ∀ n m, P n m → P (succ n) (succ m)) : ∀ n m : ℕ, P n m | 0, _m => H1 _ @@ -55,7 +55,7 @@ def subInduction {P : ℕ → ℕ → Sort u} (H1 : ∀ m, P 0 m) (H2 : ∀ n, P -- Unused in Mathlib; -- if downstream projects find this essential please copy it or remove the deprecation. -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem cond_decide_mod_two (x : ℕ) [d : Decidable (x % 2 = 1)] : cond (@decide (x % 2 = 1) d) 1 0 = x % 2 := by simp only [cond_eq_if, decide_eq_true_eq] diff --git a/Mathlib/Deprecated/RelClasses.lean b/Mathlib/Deprecated/RelClasses.lean index 357b10283c2d5..8d5f647030d5d 100644 --- a/Mathlib/Deprecated/RelClasses.lean +++ b/Mathlib/Deprecated/RelClasses.lean @@ -27,12 +27,14 @@ variable {α : Type u} open Function -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem IsTotalPreorder.swap (r) [IsTotalPreorder α r] : IsTotalPreorder α (swap r) := { @IsPreorder.swap α r _, @IsTotal.swap α r _ with } -@[deprecated (since := "2024-08-22")] instance [LinearOrder α] : IsTotalPreorder α (· ≤ ·) where -@[deprecated (since := "2024-08-22")] instance [LinearOrder α] : IsTotalPreorder α (· ≥ ·) where +@[deprecated "No deprecation message was provided." (since := "2024-08-22")] +instance [LinearOrder α] : IsTotalPreorder α (· ≤ ·) where +@[deprecated "No deprecation message was provided." (since := "2024-08-22")] +instance [LinearOrder α] : IsTotalPreorder α (· ≥ ·) where -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance [LinearOrder α] : IsIncompTrans α (· < ·) := by infer_instance diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean index a93c6f92a2109..4f8c575b67fcf 100644 --- a/Mathlib/GroupTheory/Coset/Basic.lean +++ b/Mathlib/GroupTheory/Coset/Basic.lean @@ -318,9 +318,15 @@ lemma orbit_eq_out_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x induction x using QuotientGroup.induction_on simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq'] -@[to_additive (attr := deprecated (since := "2024-10-19"))] +@[to_additive] alias orbit_eq_out'_smul := orbit_eq_out_smul +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated orbit_eq_out_smul (since := "2024-10-19")] orbit_eq_out'_smul +attribute [deprecated QuotientAddGroup.orbit_eq_out_vadd (since := "2024-10-19")] +QuotientAddGroup.orbit_eq_out'_vadd + end QuotientGroup namespace Subgroup diff --git a/Mathlib/GroupTheory/Coset/Defs.lean b/Mathlib/GroupTheory/Coset/Defs.lean index bd49ccf9a7568..c57164adfbaee 100644 --- a/Mathlib/GroupTheory/Coset/Defs.lean +++ b/Mathlib/GroupTheory/Coset/Defs.lean @@ -174,7 +174,13 @@ theorem induction_on {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (Quoti instance : Coe α (α ⧸ s) := ⟨mk⟩ -@[to_additive (attr := deprecated (since := "2024-08-04"))] alias induction_on' := induction_on +@[to_additive] alias induction_on' := induction_on + +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated induction_on (since := "2024-08-04")] induction_on' +attribute [deprecated QuotientAddGroup.induction_on (since := "2024-08-04")] +QuotientAddGroup.induction_on' @[to_additive (attr := simp)] theorem quotient_liftOn_mk {β} (f : α → β) (h) (x : α) : Quotient.liftOn' (x : α ⧸ s) f h = f x := @@ -198,7 +204,8 @@ protected theorem eq {a b : α} : (a : α ⧸ s) = b ↔ a⁻¹ * b ∈ s := _ ↔ leftRel s a b := Quotient.eq'' _ ↔ _ := by rw [leftRel_apply] -@[to_additive (attr := deprecated (since := "2024-08-04"))] alias eq' := QuotientGroup.eq +@[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-08-04"))] +alias eq' := QuotientGroup.eq @[to_additive] theorem out_eq' (a : α ⧸ s) : mk a.out = a := @@ -213,9 +220,16 @@ variable (s) theorem mk_out_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h := ⟨⟨g⁻¹ * (mk g).out, QuotientGroup.eq.mp (mk g).out_eq'.symm⟩, by rw [mul_inv_cancel_left]⟩ -@[to_additive (attr := deprecated (since := "2024-10-19")) QuotientAddGroup.mk_out'_eq_mul] +@[to_additive QuotientAddGroup.mk_out'_eq_mul] alias mk_out'_eq_mul := mk_out_eq_mul +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated mk_out_eq_mul (since := "2024-10-19")] mk_out'_eq_mul +attribute [deprecated QuotientAddGroup.mk_out_eq_mul (since := "2024-10-19")] +QuotientAddGroup.mk_out'_eq_mul + + variable {s} {a b : α} @[to_additive (attr := simp)] diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index 6ee49e4b8a6ac..ea64a5ce67e5e 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -644,7 +644,8 @@ lemma inv_eq_self_of_orderOf_eq_two {x : G} (hx : orderOf x = 2) : -- TODO: delete /-- Any group of exponent two is abelian. -/ -@[to_additive (attr := reducible, deprecated (since := "2024-02-17")) +@[to_additive (attr := reducible, + deprecated "No deprecation message was provided." (since := "2024-02-17")) "Any additive group of exponent two is abelian."] def instCommGroupOfExponentTwo (hG : Monoid.exponent G = 2) : CommGroup G where mul_comm := mul_comm_of_exponent_two hG diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean index 3848050964715..fa15f5e7d6253 100644 --- a/Mathlib/GroupTheory/GroupAction/Defs.lean +++ b/Mathlib/GroupTheory/GroupAction/Defs.lean @@ -312,9 +312,15 @@ variable {G α} theorem orbitRel_apply {a b : α} : orbitRel G α a b ↔ a ∈ orbit G b := Iff.rfl -@[to_additive (attr := deprecated (since := "2024-10-18"))] +@[to_additive] alias orbitRel_r_apply := orbitRel_apply +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated orbitRel_apply (since := "2024-10-18")] orbitRel_r_apply +attribute [deprecated AddAction.orbitRel_apply (since := "2024-10-18")] AddAction.orbitRel_r_apply + + /-- When you take a set `U` in `α`, push it down to the quotient, and pull back, you get the union of the orbit of `U` under `G`. -/ @[to_additive diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 4c15d5da76105..778fb1159400a 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -103,13 +103,26 @@ theorem _root_.QuotientGroup.out_conj_pow_minimalPeriod_mem (a : α) (q : α ⧸ rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out, eq_comm, pow_smul_eq_iff_minimalPeriod_dvd] -@[to_additive (attr := deprecated (since := "2024-10-19"))] +@[to_additive] alias Quotient.mk_smul_out' := Quotient.mk_smul_out +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated Quotient.mk_smul_out (since := "2024-10-19")] Quotient.mk_smul_out' +attribute [deprecated AddAction.Quotient.mk_vadd_out (since := "2024-10-19")] +AddAction.Quotient.mk_vadd_out' + -- Porting note: removed simp attribute, simp can prove this -@[to_additive (attr := deprecated (since := "2024-10-19"))] +@[to_additive] alias Quotient.coe_smul_out' := Quotient.coe_smul_out +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated Quotient.coe_smul_out (since := "2024-10-19")] Quotient.coe_smul_out' +attribute [deprecated AddAction.Quotient.coe_vadd_out (since := "2024-10-19")] +AddAction.Quotient.coe_vadd_out' + + @[deprecated (since := "2024-10-19")] alias _root_.QuotientGroup.out'_conj_pow_minimalPeriod_mem := QuotientGroup.out_conj_pow_minimalPeriod_mem diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index b380c1f71c410..b18e30f62e781 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -88,9 +88,14 @@ theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ => theorem IsOfFinOrder.one : IsOfFinOrder (1 : G) := isOfFinOrder_iff_pow_eq_one.mpr ⟨1, Nat.one_pos, one_pow 1⟩ -@[to_additive (attr := deprecated (since := "2024-10-11"))] +@[to_additive] alias isOfFinOrder_one := IsOfFinOrder.one +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated IsOfFinOrder.one (since := "2024-10-11")] isOfFinOrder_one +attribute [deprecated IsOfFinAddOrder.zero (since := "2024-10-11")] isOfFinAddOrder_zero + @[to_additive] lemma IsOfFinOrder.pow {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n) := by simp_rw [isOfFinOrder_iff_pow_eq_one] diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean index 11e9dc5991b44..d13254a943cc7 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean @@ -327,10 +327,17 @@ lemma isCyclic_iff_exists_ofOrder_eq_natCard [Finite α] : refine isCyclic_of_orderOf_eq_card g ?_ simp [hg] -@[to_additive (attr := deprecated (since := "2024-04-20"))] +@[to_additive] protected alias IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype := isCyclic_iff_exists_ofOrder_eq_natCard +-- `alias` doesn't add the deprecation suggestion to the `to_additive` version +-- see https://github.com/leanprover-community/mathlib4/issues/19424 +attribute [deprecated isCyclic_iff_exists_ofOrder_eq_natCard (since := "2024-04-20")] +IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype +attribute [deprecated isAddCyclic_iff_exists_ofOrder_eq_natCard (since := "2024-04-20")] +IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype + section variable [Fintype α] diff --git a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean index 0768933dedc46..da171b8d6bfaa 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Basic.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Basic.lean @@ -58,7 +58,7 @@ namespace LinearMap namespace BilinForm -@[deprecated (since := "2024-04-14")] +@[deprecated "No deprecation message was provided." (since := "2024-04-14")] theorem coeFn_congr : ∀ {x x' y y' : M}, x = x' → y = y' → B x y = B x' y' | _, _, _, _, rfl, rfl => rfl @@ -101,7 +101,7 @@ theorem ext (H : ∀ x y : M, B x y = D x y) : B = D := ext₂ H theorem congr_fun (h : B = D) (x y : M) : B x y = D x y := congr_fun₂ h _ _ -@[deprecated (since := "2024-04-14")] +@[deprecated "No deprecation message was provided." (since := "2024-04-14")] theorem coe_zero : ⇑(0 : BilinForm R M) = 0 := rfl @@ -111,7 +111,7 @@ theorem zero_apply (x y : M) : (0 : BilinForm R M) x y = 0 := variable (B D B₁ D₁) -@[deprecated (since := "2024-04-14")] +@[deprecated "No deprecation message was provided." (since := "2024-04-14")] theorem coe_add : ⇑(B + D) = B + D := rfl @@ -119,7 +119,7 @@ theorem coe_add : ⇑(B + D) = B + D := theorem add_apply (x y : M) : (B + D) x y = B x y + D x y := rfl -@[deprecated (since := "2024-04-14")] +@[deprecated "No deprecation message was provided." (since := "2024-04-14")] theorem coe_neg : ⇑(-B₁) = -B₁ := rfl @@ -127,7 +127,7 @@ theorem coe_neg : ⇑(-B₁) = -B₁ := theorem neg_apply (x y : M₁) : (-B₁) x y = -B₁ x y := rfl -@[deprecated (since := "2024-04-14")] +@[deprecated "No deprecation message was provided." (since := "2024-04-14")] theorem coe_sub : ⇑(B₁ - D₁) = B₁ - D₁ := rfl diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean index 9c011c36ed52b..c1b171f04d13e 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean @@ -58,16 +58,16 @@ section ToLin' def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R := A x /-- Auxiliary definition to define `toLinHom`; see below. -/ -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R := A /-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in the right. -/ -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := LinearMap.id set_option linter.deprecated false in -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem toLin'_apply (A : BilinForm R M) (x : M) : toLinHom (M := M) A x = A x := rfl @@ -112,7 +112,7 @@ def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M := f set_option linter.deprecated false in /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/ -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R := { BilinForm.toLinHom with invFun := LinearMap.toBilinAux @@ -121,35 +121,35 @@ def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] set_option linter.deprecated false in /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/ -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M := BilinForm.toLin.symm -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem LinearMap.toBilinAux_eq (f : M →ₗ[R] M →ₗ[R] R) : LinearMap.toBilinAux f = f := rfl set_option linter.deprecated false in -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem LinearMap.toBilin_symm : (LinearMap.toBilin.symm : BilinForm R M ≃ₗ[R] _) = BilinForm.toLin := rfl set_option linter.deprecated false in -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem BilinForm.toLin_symm : (BilinForm.toLin.symm : _ ≃ₗ[R] BilinForm R M) = LinearMap.toBilin := LinearMap.toBilin.symm_symm set_option linter.deprecated false in -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem LinearMap.toBilin_apply (f : M →ₗ[R] M →ₗ[R] R) (x y : M) : toBilin f x y = f x y := rfl set_option linter.deprecated false in -@[deprecated (since := "2024-04-26")] +@[deprecated "No deprecation message was provided." (since := "2024-04-26")] theorem BilinForm.toLin_apply (x : M) : BilinForm.toLin B x = B x := rfl diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 4a19736a68ba4..7bbb4ac2f4b65 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -834,17 +834,17 @@ set_option linter.deprecated false /-- An auxiliary construction for `tunnel`. The composition of `f`, followed by the isomorphism back to `K`, followed by the inclusion of this submodule back into `M`. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tunnelAux (f : M × N →ₗ[R] M) (Kφ : ΣK : Submodule R M, K ≃ₗ[R] M) : M × N →ₗ[R] M := (Kφ.1.subtype.comp Kφ.2.symm.toLinearMap).comp f -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tunnelAux_injective (f : M × N →ₗ[R] M) (i : Injective f) (Kφ : ΣK : Submodule R M, K ≃ₗ[R] M) : Injective (tunnelAux f Kφ) := (Subtype.val_injective.comp Kφ.2.symm.injective).comp i /-- Auxiliary definition for `tunnel`. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tunnel' (f : M × N →ₗ[R] M) (i : Injective f) : ℕ → ΣK : Submodule R M, K ≃ₗ[R] M | 0 => ⟨⊤, LinearEquiv.ofTop ⊤ rfl⟩ | n + 1 => @@ -855,7 +855,7 @@ def tunnel' (f : M × N →ₗ[R] M) (i : Injective f) : ℕ → ΣK : Submodule /-- Give an injective map `f : M × N →ₗ[R] M` we can find a nested sequence of submodules all isomorphic to `M`. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tunnel (f : M × N →ₗ[R] M) (i : Injective f) : ℕ →o (Submodule R M)ᵒᵈ := -- Note: the hint `(α := _)` had to be added in https://github.com/leanprover-community/mathlib4/pull/8386 ⟨fun n => OrderDual.toDual (α := Submodule R M) (tunnel' f i n).1, @@ -867,24 +867,24 @@ def tunnel (f : M × N →ₗ[R] M) (i : Injective f) : ℕ →o (Submodule R M) /-- Give an injective map `f : M × N →ₗ[R] M` we can find a sequence of submodules all isomorphic to `N`. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tailing (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : Submodule R M := (Submodule.snd R M N).map (tunnelAux f (tunnel' f i n)) /-- Each `tailing f i n` is a copy of `N`. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tailingLinearEquiv (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : tailing f i n ≃ₗ[R] N := ((Submodule.snd R M N).equivMapOfInjective _ (tunnelAux_injective f i (tunnel' f i n))).symm.trans (Submodule.sndEquiv R M N) -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailing_le_tunnel (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : tailing f i n ≤ OrderDual.ofDual (α := Submodule R M) (tunnel f i n) := by dsimp [tailing, tunnelAux] rw [Submodule.map_comp, Submodule.map_comp] apply Submodule.map_subtype_le -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailing_disjoint_tunnel_succ (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : Disjoint (tailing f i n) (OrderDual.ofDual (α := Submodule R M) <| tunnel f i (n + 1)) := by rw [disjoint_iff] @@ -893,7 +893,7 @@ theorem tailing_disjoint_tunnel_succ (f : M × N →ₗ[R] M) (i : Injective f) Submodule.comap_map_eq_of_injective (tunnelAux_injective _ i _), inf_comm, Submodule.fst_inf_snd, Submodule.map_bot] -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailing_sup_tunnel_succ_le_tunnel (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : tailing f i n ⊔ (OrderDual.ofDual (α := Submodule R M) <| tunnel f i (n + 1)) ≤ (OrderDual.ofDual (α := Submodule R M) <| tunnel f i n) := by @@ -902,19 +902,19 @@ theorem tailing_sup_tunnel_succ_le_tunnel (f : M × N →ₗ[R] M) (i : Injectiv apply Submodule.map_subtype_le /-- The supremum of all the copies of `N` found inside the tunnel. -/ -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] def tailings (f : M × N →ₗ[R] M) (i : Injective f) : ℕ → Submodule R M := partialSups (tailing f i) -@[simp, deprecated (since := "2024-06-05")] +@[simp, deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailings_zero (f : M × N →ₗ[R] M) (i : Injective f) : tailings f i 0 = tailing f i 0 := by simp [tailings] -@[simp, deprecated (since := "2024-06-05")] +@[simp, deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailings_succ (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : tailings f i (n + 1) = tailings f i n ⊔ tailing f i (n + 1) := by simp [tailings] -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailings_disjoint_tunnel (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : Disjoint (tailings f i n) (OrderDual.ofDual (α := Submodule R M) <| tunnel f i (n + 1)) := by induction' n with n ih @@ -926,7 +926,7 @@ theorem tailings_disjoint_tunnel (f : M × N →ₗ[R] M) (i : Injective f) (n : · apply Disjoint.mono_right _ ih apply tailing_sup_tunnel_succ_le_tunnel -@[deprecated (since := "2024-06-05")] +@[deprecated "No deprecation message was provided." (since := "2024-06-05")] theorem tailings_disjoint_tailing (f : M × N →ₗ[R] M) (i : Injective f) (n : ℕ) : Disjoint (tailings f i n) (tailing f i (n + 1)) := Disjoint.mono_right (tailing_le_tunnel f i _) (tailings_disjoint_tunnel f i _) diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index 7a0eb1ff4d84f..89c3a8fe8a2f1 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -725,20 +725,21 @@ alias by_contradiction := byContradiction -- TODO: remove? rename in core? alias prop_complete := propComplete -- TODO: remove? rename in core? -@[elab_as_elim, deprecated (since := "2024-07-27")] theorem cases_true_false (p : Prop → Prop) +@[elab_as_elim, deprecated "No deprecation message was provided." (since := "2024-07-27")] +theorem cases_true_false (p : Prop → Prop) (h1 : p True) (h2 : p False) (a : Prop) : p a := Or.elim (prop_complete a) (fun ht : a = True ↦ ht.symm ▸ h1) fun hf : a = False ↦ hf.symm ▸ h2 -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem eq_false_or_eq_true (a : Prop) : a = False ∨ a = True := (prop_complete a).symm set_option linter.deprecated false in -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p True) (h2 : p False) : p a := @cases_true_false p h1 h2 a set_option linter.deprecated false in -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem cases {p : Prop → Prop} (h1 : p True) (h2 : p False) (a) : p a := cases_on a h1 h2 end Classical diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 25e17db9f409b..b003cc9a9db03 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -443,7 +443,7 @@ lemma Integrable.of_finite [Finite α] [MeasurableSingletonClass α] [IsFiniteMe /-- This lemma is a special case of `Integrable.of_finite`. -/ -- Eternal deprecation for discoverability, don't remove -@[deprecated Integrable.of_finite, nolint deprecatedNoSince] +@[deprecated Integrable.of_finite (since := "2024-10-05"), nolint deprecatedNoSince] lemma Integrable.of_isEmpty [IsEmpty α] {f : α → β} : Integrable f μ := .of_finite @[deprecated (since := "2024-02-05")] alias integrable_of_fintype := Integrable.of_finite diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean index c9a41869344f8..f8d833559d3e9 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -567,7 +567,7 @@ instance isFiniteMeasure_sfiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure h.1.choose_spec.1 n set_option linter.deprecated false in -@[deprecated (since := "2024-10-11")] +@[deprecated "No deprecation message was provided." (since := "2024-10-11")] instance isFiniteMeasure_sFiniteSeq [SFinite μ] (n : ℕ) : IsFiniteMeasure (sFiniteSeq μ n) := isFiniteMeasure_sfiniteSeq n diff --git a/Mathlib/MeasureTheory/Measure/WithDensityFinite.lean b/Mathlib/MeasureTheory/Measure/WithDensityFinite.lean index 21abd06cd6cee..40b56846328c7 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensityFinite.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensityFinite.lean @@ -117,7 +117,7 @@ noncomputable def Measure.densityToFinite (μ : Measure α) [SFinite μ] (a : α μ.rnDeriv μ.toFinite a set_option linter.deprecated false in -@[deprecated (since := "2024-10-04")] +@[deprecated "No deprecation message was provided." (since := "2024-10-04")] lemma densityToFinite_def (μ : Measure α) [SFinite μ] : μ.densityToFinite = μ.rnDeriv μ.toFinite := rfl diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean index 5c13f9d53ebe2..8b8038b188ab0 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction.lean @@ -1291,7 +1291,8 @@ theorem _root_.Nat.card_divisors {n : ℕ} (hn : n ≠ 0) : exact Finset.prod_congr n.support_factorization fun _ h => sigma_zero_apply_prime_pow <| Nat.prime_of_mem_primeFactors h -@[deprecated (since := "2024-06-09")] theorem card_divisors (n : ℕ) (hn : n ≠ 0) : +@[deprecated "No deprecation message was provided." (since := "2024-06-09")] +theorem card_divisors (n : ℕ) (hn : n ≠ 0) : #n.divisors = n.primeFactors.prod (n.factorization · + 1) := Nat.card_divisors hn theorem _root_.Nat.sum_divisors {n : ℕ} (hn : n ≠ 0) : diff --git a/Mathlib/NumberTheory/MulChar/Basic.lean b/Mathlib/NumberTheory/MulChar/Basic.lean index 2df970973c59d..7ddd95b920b4e 100644 --- a/Mathlib/NumberTheory/MulChar/Basic.lean +++ b/Mathlib/NumberTheory/MulChar/Basic.lean @@ -391,13 +391,13 @@ lemma ne_one_iff {χ : MulChar R R'} : χ ≠ 1 ↔ ∃ a : Rˣ, χ a ≠ 1 := b simp only [Ne, eq_one_iff, not_forall] /-- A multiplicative character is *nontrivial* if it takes a value `≠ 1` on a unit. -/ -@[deprecated (since := "2024-06-16")] +@[deprecated "No deprecation message was provided." (since := "2024-06-16")] def IsNontrivial (χ : MulChar R R') : Prop := ∃ a : Rˣ, χ a ≠ 1 set_option linter.deprecated false in /-- A multiplicative character is nontrivial iff it is not the trivial character. -/ -@[deprecated (since := "2024-06-16")] +@[deprecated "No deprecation message was provided." (since := "2024-06-16")] theorem isNontrivial_iff (χ : MulChar R R') : χ.IsNontrivial ↔ χ ≠ 1 := by simp only [IsNontrivial, Ne, MulChar.ext_iff, not_forall, one_apply_coe] @@ -573,7 +573,7 @@ theorem sum_eq_zero_of_ne_one [IsDomain R'] {χ : MulChar R R'} (hχ : χ ≠ 1) simpa only [Finset.mul_sum, ← map_mul] using b.mulLeft_bijective.sum_comp _ set_option linter.deprecated false in -@[deprecated (since := "2024-06-16")] +@[deprecated "No deprecation message was provided." (since := "2024-06-16")] lemma IsNontrivial.sum_eq_zero [IsDomain R'] {χ : MulChar R R'} (hχ : χ.IsNontrivial) : ∑ a, χ a = 0 := sum_eq_zero_of_ne_one ((isNontrivial_iff _).mp hχ) diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean index dc90cc7b0adbe..b97cdc2c979d6 100644 --- a/Mathlib/Order/Defs.lean +++ b/Mathlib/Order/Defs.lean @@ -206,11 +206,11 @@ theorem Equivalence.transitive (h : Equivalence r) : Transitive r := variable {β : Sort*} (r : β → β → Prop) (f : α → β) -@[deprecated (since := "2024-09-13")] +@[deprecated "No deprecation message was provided." (since := "2024-09-13")] theorem InvImage.trans (h : Transitive r) : Transitive (InvImage r f) := fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) ↦ h h₁ h₂ -@[deprecated (since := "2024-09-13")] +@[deprecated "No deprecation message was provided." (since := "2024-09-13")] theorem InvImage.irreflexive (h : Irreflexive r) : Irreflexive (InvImage r f) := fun (a : α) (h₁ : InvImage r f a a) ↦ h (f a) h₁ @@ -276,7 +276,7 @@ lemma lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a := Preorder.lt_iff_le_n lemma lt_of_le_not_le (hab : a ≤ b) (hba : ¬ b ≤ a) : a < b := lt_iff_le_not_le.2 ⟨hab, hba⟩ -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem le_not_le_of_lt : ∀ {a b : α}, a < b → a ≤ b ∧ ¬b ≤ a | _a, _b, hab => lt_iff_le_not_le.mp hab @@ -502,7 +502,7 @@ namespace Nat /-! Deprecated properties of inequality on `Nat` -/ -@[deprecated (since := "2024-08-23")] +@[deprecated "No deprecation message was provided." (since := "2024-08-23")] protected def ltGeByCases {a b : Nat} {C : Sort*} (h₁ : a < b → C) (h₂ : b ≤ a → C) : C := Decidable.byCases h₁ fun h => h₂ (Or.elim (Nat.lt_or_ge a b) (fun a => absurd a h) fun a => a) diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean index 4c97970762171..c34eaa969055e 100644 --- a/Mathlib/Order/OmegaCompletePartialOrder.lean +++ b/Mathlib/Order/OmegaCompletePartialOrder.lean @@ -731,7 +731,7 @@ theorem apply_mono {f g : α →𝒄 β} {x y : α} (h₁ : f ≤ g) (h₂ : x OrderHom.apply_mono (show (f : α →o β) ≤ g from h₁) h₂ set_option linter.deprecated false in -@[deprecated (since := "2024-07-27")] +@[deprecated "No deprecation message was provided." (since := "2024-07-27")] theorem ite_continuous' {p : Prop} [hp : Decidable p] (f g : α → β) (hf : Continuous' f) (hg : Continuous' g) : Continuous' fun x => if p then f x else g x := by split_ifs <;> simp [*] diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean index c99abc227fd09..0acae0e49466b 100644 --- a/Mathlib/Order/RelClasses.lean +++ b/Mathlib/Order/RelClasses.lean @@ -86,7 +86,7 @@ theorem IsStrictOrder.swap (r) [IsStrictOrder α r] : IsStrictOrder α (swap r) theorem IsPartialOrder.swap (r) [IsPartialOrder α r] : IsPartialOrder α (swap r) := { @IsPreorder.swap α r _, @IsAntisymm.swap α r _ with } -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] theorem IsLinearOrder.swap (r) [IsLinearOrder α r] : IsLinearOrder α (swap r) := { @IsPartialOrder.swap α r _, @IsTotal.swap α r _ with } @@ -212,7 +212,7 @@ instance (priority := 100) isStrictOrderConnected_of_isStrictTotalOrder [IsStric fun o ↦ o.elim (fun e ↦ e ▸ h) fun h' ↦ _root_.trans h' h⟩ -- see Note [lower instance priority] -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance (priority := 100) isStrictTotalOrder_of_isStrictTotalOrder [IsStrictTotalOrder α r] : IsStrictWeakOrder α r := { isStrictWeakOrder_of_isOrderConnected with } @@ -780,7 +780,7 @@ instance [LinearOrder α] : IsStrictTotalOrder α (· < ·) where instance [LinearOrder α] : IsOrderConnected α (· < ·) := by infer_instance -@[deprecated (since := "2024-07-30")] +@[deprecated "No deprecation message was provided." (since := "2024-07-30")] instance [LinearOrder α] : IsStrictWeakOrder α (· < ·) := by infer_instance theorem transitive_le [Preorder α] : Transitive (@LE.le α _) := diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean index dafc9ee33dced..ca79284dac29a 100644 --- a/Mathlib/SetTheory/Cardinal/Aleph.lean +++ b/Mathlib/SetTheory/Cardinal/Aleph.lean @@ -541,7 +541,7 @@ def alephIdx.relIso : @RelIso Cardinal.{u} Ordinal.{u} (· < ·) (· < ·) := def alephIdx : Cardinal → Ordinal := aleph'.symm -@[deprecated (since := "2024-08-28")] +@[deprecated "No deprecation message was provided." (since := "2024-08-28")] theorem alephIdx.relIso_coe : (alephIdx.relIso : Cardinal → Ordinal) = alephIdx := rfl @@ -555,7 +555,7 @@ theorem alephIdx.relIso_coe : (alephIdx.relIso : Cardinal → Ordinal) = alephId def Aleph'.relIso := aleph' -@[deprecated (since := "2024-08-28")] +@[deprecated "No deprecation message was provided." (since := "2024-08-28")] theorem aleph'.relIso_coe : (Aleph'.relIso : Ordinal → Cardinal) = aleph' := rfl @@ -571,11 +571,11 @@ theorem aleph'_le {o₁ o₂ : Ordinal} : aleph' o₁ ≤ aleph' o₂ ↔ o₁ theorem aleph'_max (o₁ o₂ : Ordinal) : aleph' (max o₁ o₂) = max (aleph' o₁) (aleph' o₂) := aleph'.monotone.map_max -@[deprecated (since := "2024-08-28")] +@[deprecated "No deprecation message was provided." (since := "2024-08-28")] theorem aleph'_alephIdx (c : Cardinal) : aleph' c.alephIdx = c := Cardinal.alephIdx.relIso.toEquiv.symm_apply_apply c -@[deprecated (since := "2024-08-28")] +@[deprecated "No deprecation message was provided." (since := "2024-08-28")] theorem alephIdx_aleph' (o : Ordinal) : (aleph' o).alephIdx = o := Cardinal.alephIdx.relIso.toEquiv.apply_symm_apply o @@ -608,7 +608,7 @@ theorem aleph'_limit {o : Ordinal} (ho : o.IsLimit) : aleph' o = ⨆ a : Iio o, theorem aleph'_omega0 : aleph' ω = ℵ₀ := preAleph_omega0 -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias aleph'_omega := aleph'_omega0 /-- `aleph'` and `aleph_idx` form an equivalence between `Ordinal` and `Cardinal` -/ @@ -638,7 +638,7 @@ theorem aleph'_isNormal : IsNormal (ord ∘ aleph') := -- They should also use `¬ BddAbove` instead of `Unbounded (· < ·)`. /-- Ordinals that are cardinals are unbounded. -/ -@[deprecated (since := "2024-09-24")] +@[deprecated "No deprecation message was provided." (since := "2024-09-24")] theorem ord_card_unbounded : Unbounded (· < ·) { b : Ordinal | b.card.ord = b } := unbounded_lt_iff.2 fun a => ⟨_, @@ -646,16 +646,16 @@ theorem ord_card_unbounded : Unbounded (· < ·) { b : Ordinal | b.card.ord = b dsimp rw [card_ord], (lt_ord_succ_card a).le⟩⟩ -@[deprecated (since := "2024-09-24")] +@[deprecated "No deprecation message was provided." (since := "2024-09-24")] theorem eq_aleph'_of_eq_card_ord {o : Ordinal} (ho : o.card.ord = o) : ∃ a, (aleph' a).ord = o := ⟨aleph'.symm o.card, by simpa using ho⟩ /-- Infinite ordinals that are cardinals are unbounded. -/ -@[deprecated (since := "2024-09-24")] +@[deprecated "No deprecation message was provided." (since := "2024-09-24")] theorem ord_card_unbounded' : Unbounded (· < ·) { b : Ordinal | b.card.ord = b ∧ ω ≤ b } := (unbounded_lt_inter_le ω).2 ord_card_unbounded -@[deprecated (since := "2024-09-24")] +@[deprecated "No deprecation message was provided." (since := "2024-09-24")] theorem eq_aleph_of_eq_card_ord {o : Ordinal} (ho : o.card.ord = o) (ho' : ω ≤ o) : ∃ a, (ℵ_ a).ord = o := by cases' eq_aleph'_of_eq_card_ord ho with a ha diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 18f50f95db1cb..e0105b3587892 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -145,7 +145,7 @@ protected theorem eq : #α = #β ↔ Nonempty (α ≃ β) := Quotient.eq' /-- Avoid using `Quotient.mk` to construct a `Cardinal` directly -/ -@[deprecated (since := "2024-10-24")] +@[deprecated "No deprecation message was provided." (since := "2024-10-24")] theorem mk'_def (α : Type u) : @Eq Cardinal ⟦α⟧ #α := rfl diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index 87b3654599332..9a8363e186c9a 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -114,7 +114,7 @@ def StrictOrder.cof (r : α → α → Prop) : Cardinal := Order.cof (swap rᶜ) /-- The set in the definition of `Order.StrictOrder.cof` is nonempty. -/ -@[deprecated (since := "2024-10-22")] +@[deprecated "No deprecation message was provided." (since := "2024-10-22")] theorem StrictOrder.cof_nonempty (r : α → α → Prop) [IsIrrefl α r] : { c | ∃ S : Set α, Unbounded r S ∧ #S = c }.Nonempty := @Order.cof_nonempty α _ (IsRefl.swap rᶜ) diff --git a/Mathlib/SetTheory/Game/Ordinal.lean b/Mathlib/SetTheory/Game/Ordinal.lean index d281b72b36a02..cf5a7e8f4cf97 100644 --- a/Mathlib/SetTheory/Game/Ordinal.lean +++ b/Mathlib/SetTheory/Game/Ordinal.lean @@ -35,7 +35,7 @@ noncomputable def toPGame (o : Ordinal.{u}) : PGame.{u} := termination_by o decreasing_by exact ((enumIsoToType o).symm x).prop -@[deprecated (since := "2024-09-22")] +@[deprecated "No deprecation message was provided." (since := "2024-09-22")] theorem toPGame_def (o : Ordinal) : o.toPGame = ⟨o.toType, PEmpty, fun x => ((enumIsoToType o).symm x).val.toPGame, PEmpty.elim⟩ := by rw [toPGame] diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index 6cc7dfe51df9e..3563908538d09 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -605,14 +605,14 @@ theorem one_add_omega0 : 1 + ω = ω := by cases a <;> cases b <;> intro H <;> cases' H with _ _ H _ _ H <;> [exact H.elim; exact Nat.succ_pos _; exact Nat.succ_lt_succ H] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias one_add_omega := one_add_omega0 @[simp] theorem one_add_of_omega0_le {o} (h : ω ≤ o) : 1 + o = o := by rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, one_add_omega0] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias one_add_of_omega_le := one_add_of_omega0_le /-! ### Multiplication of ordinals -/ @@ -1185,7 +1185,7 @@ def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} := iSup f set_option linter.deprecated false in -@[deprecated (since := "2024-08-27")] +@[deprecated "No deprecation message was provided." (since := "2024-08-27")] theorem sSup_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : sSup (Set.range f) = sup.{_, v} f := rfl @@ -1252,14 +1252,15 @@ protected theorem lt_iSup_iff {ι} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [S a < iSup f ↔ ∃ i, a < f i := lt_ciSup_iff' (bddAbove_of_small _) -@[deprecated (since := "2024-11-12")] alias lt_iSup := lt_iSup_iff +@[deprecated "No deprecation message was provided." (since := "2024-11-12")] +alias lt_iSup := lt_iSup_iff set_option linter.deprecated false in @[deprecated Ordinal.lt_iSup (since := "2024-08-27")] theorem lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : a < sup.{_, v} f ↔ ∃ i, a < f i := by simpa only [not_forall, not_le] using not_congr (@sup_le_iff.{_, v} _ f a) -@[deprecated (since := "2024-08-27")] +@[deprecated "No deprecation message was provided." (since := "2024-08-27")] theorem ne_iSup_iff_lt_iSup {ι : Type u} {f : ι → Ordinal.{max u v}} : (∀ i, f i ≠ iSup f) ↔ ∀ i, f i < iSup f := forall_congr' fun i => (Ordinal.le_iSup f i).lt_iff_ne.symm @@ -1377,7 +1378,7 @@ theorem unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [IsW unbounded_range_of_le_iSup r f h set_option linter.deprecated false in -@[deprecated (since := "2024-08-27")] +@[deprecated "No deprecation message was provided." (since := "2024-08-27")] theorem le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u} s) (a) (ha : a ∈ s) : a ≤ sup.{u, u} fun x => ((@equivShrink s hs).symm x).val := by convert le_sup.{u, u} (fun x => ((@equivShrink s hs).symm x).val) ((@equivShrink s hs) ⟨a, ha⟩) @@ -1422,7 +1423,7 @@ theorem IsNormal.apply_of_isLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNorma rw [← H.map_iSup, ho.iSup_Iio] set_option linter.deprecated false in -@[deprecated (since := "2024-08-27")] +@[deprecated "No deprecation message was provided." (since := "2024-08-27")] theorem sup_eq_sSup {s : Set Ordinal.{u}} (hs : Small.{u} s) : (sup.{u, u} fun x => (@equivShrink s hs).symm x) = sSup s := let hs' := bddAbove_iff_small.2 hs @@ -1986,12 +1987,12 @@ theorem IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : Deprecated. If you need this value explicitly, write it in terms of `iSup`. If you just want an upper bound for the image of `op`, use that `Iio a ×ˢ Iio b` is a small set. -/ -@[deprecated (since := "2024-10-11")] +@[deprecated "No deprecation message was provided." (since := "2024-10-11")] def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) : Ordinal := lsub (fun x : o₁.toType × o₂.toType => op (typein_lt_self x.1) (typein_lt_self x.2)) -@[deprecated (since := "2024-10-11")] +@[deprecated "No deprecation message was provided." (since := "2024-10-11")] theorem lt_blsub₂ {o₁ o₂ : Ordinal} (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal} (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := by @@ -2012,34 +2013,34 @@ set_option linter.deprecated false def mex {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal := sInf (Set.range f)ᶜ -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem mex_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : mex.{_, v} f ∉ Set.range f := csInf_mem (nonempty_compl_range.{_, v} f) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem le_mex_of_forall {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal} (H : ∀ b < a, ∃ i, f i = b) : a ≤ mex.{_, v} f := by by_contra! h exact mex_not_mem_range f (H _ h) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem ne_mex {ι : Type u} (f : ι → Ordinal.{max u v}) : ∀ i, f i ≠ mex.{_, v} f := by simpa using mex_not_mem_range.{_, v} f -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem mex_le_of_ne {ι} {f : ι → Ordinal} {a} (ha : ∀ i, f i ≠ a) : mex f ≤ a := csInf_le' (by simp [ha]) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem exists_of_lt_mex {ι} {f : ι → Ordinal} {a} (ha : a < mex f) : ∃ i, f i = a := by by_contra! ha' exact ha.not_le (mex_le_of_ne ha') -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem mex_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : mex.{_, v} f ≤ lsub.{_, v} f := csInf_le' (lsub_not_mem_range f) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem mex_monotone {α β : Type u} {f : α → Ordinal.{max u v}} {g : β → Ordinal.{max u v}} (h : Set.range f ⊆ Set.range g) : mex.{_, v} f ≤ mex.{_, v} g := by refine mex_le_of_ne fun i hi => ?_ @@ -2072,18 +2073,18 @@ theorem mex_lt_ord_succ_mk {ι : Type u} (f : ι → Ordinal.{u}) : def bmex (o : Ordinal) (f : ∀ a < o, Ordinal) : Ordinal := mex (familyOfBFamily o f) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem bmex_not_mem_brange {o : Ordinal} (f : ∀ a < o, Ordinal) : bmex o f ∉ brange o f := by rw [← range_familyOfBFamily] apply mex_not_mem_range -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem le_bmex_of_forall {o : Ordinal} (f : ∀ a < o, Ordinal) {a : Ordinal} (H : ∀ b < a, ∃ i hi, f i hi = b) : a ≤ bmex o f := by by_contra! h exact bmex_not_mem_brange f (H _ h) -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem ne_bmex {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {i} (hi) : f i hi ≠ bmex.{_, v} o f := by convert (config := {transparency := .default}) @@ -2091,23 +2092,23 @@ theorem ne_bmex {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {i} (hi) : -- Porting note: `familyOfBFamily_enum` → `typein_enum` rw [typein_enum] -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem bmex_le_of_ne {o : Ordinal} {f : ∀ a < o, Ordinal} {a} (ha : ∀ i hi, f i hi ≠ a) : bmex o f ≤ a := mex_le_of_ne fun _i => ha _ _ -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem exists_of_lt_bmex {o : Ordinal} {f : ∀ a < o, Ordinal} {a} (ha : a < bmex o f) : ∃ i hi, f i hi = a := by cases' exists_of_lt_mex ha with i hi exact ⟨_, typein_lt_self i, hi⟩ -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem bmex_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : bmex.{_, v} o f ≤ blsub.{_, v} o f := mex_le_lsub _ -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem bmex_monotone {o o' : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} {g : ∀ a < o', Ordinal.{max u v}} (h : brange o f ⊆ brange o' g) : bmex.{_, v} o f ≤ bmex.{_, v} o' g := @@ -2165,7 +2166,7 @@ theorem one_add_natCast (m : ℕ) : 1 + (m : Ordinal) = succ m := by rw [← Nat.cast_one, ← Nat.cast_add, add_comm] rfl -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias one_add_nat_cast := one_add_natCast -- See note [no_index around OfNat.ofNat] @@ -2179,43 +2180,43 @@ theorem natCast_mul (m : ℕ) : ∀ n : ℕ, ((m * n : ℕ) : Ordinal) = m * n | 0 => by simp | n + 1 => by rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one] -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_mul := natCast_mul @[deprecated Nat.cast_le (since := "2024-10-17")] theorem natCast_le {m n : ℕ} : (m : Ordinal) ≤ n ↔ m ≤ n := Nat.cast_le -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_le := natCast_le @[deprecated Nat.cast_inj (since := "2024-10-17")] theorem natCast_inj {m n : ℕ} : (m : Ordinal) = n ↔ m = n := Nat.cast_inj -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_inj := natCast_inj @[deprecated Nat.cast_lt (since := "2024-10-17")] theorem natCast_lt {m n : ℕ} : (m : Ordinal) < n ↔ m < n := Nat.cast_lt -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_lt := natCast_lt @[deprecated Nat.cast_eq_zero (since := "2024-10-17")] theorem natCast_eq_zero {n : ℕ} : (n : Ordinal) = 0 ↔ n = 0 := Nat.cast_eq_zero -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_eq_zero := natCast_eq_zero @[deprecated Nat.cast_ne_zero (since := "2024-10-17")] theorem natCast_ne_zero {n : ℕ} : (n : Ordinal) ≠ 0 ↔ n ≠ 0 := Nat.cast_ne_zero -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_ne_zero := natCast_ne_zero @[deprecated Nat.cast_pos' (since := "2024-10-17")] theorem natCast_pos {n : ℕ} : (0 : Ordinal) < n ↔ 0 < n := Nat.cast_pos' -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_pos := natCast_pos @[simp, norm_cast] @@ -2226,7 +2227,7 @@ theorem natCast_sub (m n : ℕ) : ((m - n : ℕ) : Ordinal) = m - n := by · apply (add_left_cancel n).1 rw [← Nat.cast_add, add_tsub_cancel_of_le h, Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)] -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_sub := natCast_sub @[simp, norm_cast] @@ -2241,7 +2242,7 @@ theorem natCast_div (m n : ℕ) : ((m / n : ℕ) : Ordinal) = m / n := by ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)] apply Nat.lt_succ_self -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_div := natCast_div @[simp, norm_cast] @@ -2249,7 +2250,7 @@ theorem natCast_mod (m n : ℕ) : ((m % n : ℕ) : Ordinal) = m % n := by rw [← add_left_cancel, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add, Nat.div_add_mod] -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_mod := natCast_mod @[simp] @@ -2257,7 +2258,7 @@ theorem lift_natCast : ∀ n : ℕ, lift.{u, v} n = n | 0 => by simp | n + 1 => by simp [lift_natCast n] -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias lift_nat_cast := lift_natCast -- See note [no_index around OfNat.ofNat] @@ -2292,13 +2293,13 @@ theorem lt_add_of_limit {a b c : Ordinal.{u}} (h : IsLimit c) : theorem lt_omega0 {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n := by simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias lt_omega := lt_omega0 theorem nat_lt_omega0 (n : ℕ) : ↑n < ω := lt_omega0.2 ⟨_, rfl⟩ -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias nat_lt_omega := nat_lt_omega0 theorem omega0_pos : 0 < ω := @@ -2307,12 +2308,12 @@ theorem omega0_pos : 0 < ω := theorem omega0_ne_zero : ω ≠ 0 := omega0_pos.ne' -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias omega_ne_zero := omega0_ne_zero theorem one_lt_omega0 : 1 < ω := by simpa only [Nat.cast_one] using nat_lt_omega0 1 -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias one_lt_omega := one_lt_omega0 theorem isLimit_omega0 : IsLimit ω := @@ -2320,10 +2321,10 @@ theorem isLimit_omega0 : IsLimit ω := let ⟨n, e⟩ := lt_omega0.1 h rw [e]; exact nat_lt_omega0 (n + 1)⟩ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] alias omega0_isLimit := isLimit_omega0 -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias omega_isLimit := isLimit_omega0 theorem omega0_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o := @@ -2332,7 +2333,7 @@ theorem omega0_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o := let ⟨n, e⟩ := lt_omega0.1 h rw [e, ← succ_le_iff]; exact H (n + 1)⟩ -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias omega_le := omega0_le @[simp] @@ -2344,7 +2345,7 @@ set_option linter.deprecated false in theorem sup_natCast : sup Nat.cast = ω := iSup_natCast -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias sup_nat_cast := sup_natCast theorem nat_lt_limit {o} (h : IsLimit o) : ∀ n : ℕ, ↑n < o @@ -2354,7 +2355,7 @@ theorem nat_lt_limit {o} (h : IsLimit o) : ∀ n : ℕ, ↑n < o theorem omega0_le_of_isLimit {o} (h : IsLimit o) : ω ≤ o := omega0_le.2 fun n => le_of_lt <| nat_lt_limit h n -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias omega_le_of_isLimit := omega0_le_of_isLimit theorem isLimit_iff_omega0_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ a := by @@ -2372,7 +2373,7 @@ theorem isLimit_iff_omega0_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ intro e simp only [e, mul_zero] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias isLimit_iff_omega_dvd := isLimit_iff_omega0_dvd theorem add_mul_limit_aux {a b c : Ordinal} (ba : b + a = a) (l : IsLimit c) @@ -2416,7 +2417,7 @@ theorem add_le_of_forall_add_lt {a b c : Ordinal} (hb : 0 < b) (h : ∀ d < b, a theorem IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) : ⨆ n : ℕ, f n = f ω := by rw [← iSup_natCast, hf.map_iSup] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias IsNormal.apply_omega := IsNormal.apply_omega0 @[simp] @@ -2460,7 +2461,7 @@ theorem isLimit_ord {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit := by · rw [ord_aleph0] exact Ordinal.isLimit_omega0 -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] alias ord_isLimit := isLimit_ord theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.toType := diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 5a31bfe919ee9..ec9a34419fbf4 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -387,7 +387,7 @@ def typein (r : α → α → Prop) [IsWellOrder α r] : @PrincipalSeg α Ordina alias typein.principalSeg := typein set_option linter.deprecated false in -@[deprecated (since := "2024-10-09")] +@[deprecated "No deprecation message was provided." (since := "2024-10-09")] theorem typein.principalSeg_coe (r : α → α → Prop) [IsWellOrder α r] : (typein.principalSeg r : α → Ordinal) = typein r := rfl @@ -513,7 +513,7 @@ noncomputable def enumIsoToType (o : Ordinal) : Set.Iio o ≃o o.toType where right_inv _ := enum_typein _ _ map_rel_iff' := enum_le_enum' _ -@[deprecated (since := "2024-08-26")] +@[deprecated "No deprecation message was provided." (since := "2024-08-26")] alias enumIsoOut := enumIsoToType instance small_Iio (o : Ordinal.{u}) : Small.{u} (Iio o) := @@ -925,7 +925,7 @@ theorem card_succ (o : Ordinal) : card (succ o) = card o + 1 := by theorem natCast_succ (n : ℕ) : ↑n.succ = succ (n : Ordinal) := rfl -@[deprecated (since := "2024-04-17")] +@[deprecated "No deprecation message was provided." (since := "2024-04-17")] alias nat_cast_succ := natCast_succ instance uniqueIioOne : Unique (Iio (1 : Ordinal)) where @@ -1213,7 +1213,7 @@ alias card_typein_out_lt := card_typein_toType_lt theorem mk_Iio_ord_toType {c : Cardinal} (i : c.ord.toType) : #(Iio i) < c := card_typein_toType_lt c i -@[deprecated (since := "2024-08-26")] +@[deprecated "No deprecation message was provided." (since := "2024-08-26")] alias mk_Iio_ord_out_α := mk_Iio_ord_toType theorem ord_injective : Injective ord := by diff --git a/Mathlib/SetTheory/Ordinal/Enum.lean b/Mathlib/SetTheory/Ordinal/Enum.lean index 4e5d4d38a7cf6..e8b3bb9314bc5 100644 --- a/Mathlib/SetTheory/Ordinal/Enum.lean +++ b/Mathlib/SetTheory/Ordinal/Enum.lean @@ -33,7 +33,7 @@ termination_by o variable {s : Set Ordinal.{u}} -@[deprecated (since := "2024-09-20")] +@[deprecated "No deprecation message was provided." (since := "2024-09-20")] theorem enumOrd_def (o : Ordinal.{u}) : enumOrd s o = sInf (s ∩ { b | ∀ c, c < o → enumOrd s c < b }) := by rw [enumOrd] diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean index 36b50a052b83d..84f2f8db36b0d 100644 --- a/Mathlib/SetTheory/Ordinal/FixedPoint.lean +++ b/Mathlib/SetTheory/Ordinal/FixedPoint.lean @@ -52,7 +52,7 @@ least `a`, and `Ordinal.nfpFamily_le_fp` shows this is the least ordinal with th def nfpFamily (f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : Ordinal := ⨆ i, List.foldr f a i -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpFamily_eq_sup (f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : nfpFamily f a = ⨆ i, List.foldr f a i := rfl @@ -238,48 +238,48 @@ def nfpBFamily (o : Ordinal.{u}) (f : ∀ b < o, Ordinal.{max u v} → Ordinal.{ Ordinal.{max u v} → Ordinal.{max u v} := nfpFamily (familyOfBFamily o f) -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_eq_nfpFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) : nfpBFamily.{u, v} o f = nfpFamily (familyOfBFamily o f) := rfl -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem foldr_le_nfpBFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) (a l) : List.foldr (familyOfBFamily o f) a l ≤ nfpBFamily.{u, v} o f a := Ordinal.le_iSup _ _ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem le_nfpBFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) (a) : a ≤ nfpBFamily.{u, v} o f a := Ordinal.le_iSup (fun _ ↦ List.foldr _ a _) [] -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem lt_nfpBFamily {a b} : a < nfpBFamily.{u, v} o f b ↔ ∃ l, a < List.foldr (familyOfBFamily o f) b l := Ordinal.lt_iSup_iff -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_le_iff {o : Ordinal} {f : ∀ b < o, Ordinal → Ordinal} {a b} : nfpBFamily.{u, v} o f a ≤ b ↔ ∀ l, List.foldr (familyOfBFamily o f) a l ≤ b := Ordinal.iSup_le_iff -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_le {o : Ordinal} {f : ∀ b < o, Ordinal → Ordinal} {a b} : (∀ l, List.foldr (familyOfBFamily o f) a l ≤ b) → nfpBFamily.{u, v} o f a ≤ b := Ordinal.iSup_le -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_monotone (hf : ∀ i hi, Monotone (f i hi)) : Monotone (nfpBFamily.{u, v} o f) := nfpFamily_monotone fun _ => hf _ _ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem apply_lt_nfpBFamily (H : ∀ i hi, IsNormal (f i hi)) {a b} (hb : b < nfpBFamily.{u, v} o f a) (i hi) : f i hi b < nfpBFamily.{u, v} o f a := by rw [← familyOfBFamily_enum o f] apply apply_lt_nfpFamily (fun _ => H _ _) hb -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem apply_lt_nfpBFamily_iff (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} : (∀ i hi, f i hi b < nfpBFamily.{u, v} o f a) ↔ b < nfpBFamily.{u, v} o f a := ⟨fun h => by @@ -287,19 +287,19 @@ theorem apply_lt_nfpBFamily_iff (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) refine (apply_lt_nfpFamily_iff ?_).1 fun _ => h _ _ exact fun _ => H _ _, apply_lt_nfpBFamily H⟩ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_le_apply (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} : (∃ i hi, nfpBFamily.{u, v} o f a ≤ f i hi b) ↔ nfpBFamily.{u, v} o f a ≤ b := by rw [← not_iff_not] push_neg exact apply_lt_nfpBFamily_iff.{u, v} ho H -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_le_fp (H : ∀ i hi, Monotone (f i hi)) {a b} (ab : a ≤ b) (h : ∀ i hi, f i hi b ≤ b) : nfpBFamily.{u, v} o f a ≤ b := nfpFamily_le_fp (fun _ => H _ _) ab fun _ => h _ _ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_fp {i hi} (H : IsNormal (f i hi)) (a) : f i hi (nfpBFamily.{u, v} o f a) = nfpBFamily.{u, v} o f a := by rw [← familyOfBFamily_enum o f] @@ -307,7 +307,7 @@ theorem nfpBFamily_fp {i hi} (H : IsNormal (f i hi)) (a) : rw [familyOfBFamily_enum] exact H -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem apply_le_nfpBFamily (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} : (∀ i hi, f i hi b ≤ nfpBFamily.{u, v} o f a) ↔ b ≤ nfpBFamily.{u, v} o f a := by refine ⟨fun h => ?_, fun h i hi => ?_⟩ @@ -316,13 +316,13 @@ theorem apply_le_nfpBFamily (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a · rw [← nfpBFamily_fp (H i hi)] exact (H i hi).monotone h -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem nfpBFamily_eq_self {a} (h : ∀ i hi, f i hi a = a) : nfpBFamily.{u, v} o f a = a := nfpFamily_eq_self fun _ => h _ _ /-- A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points. -/ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem not_bddAbove_fp_bfamily (H : ∀ i hi, IsNormal (f i hi)) : ¬ BddAbove (⋂ (i) (hi), Function.fixedPoints (f i hi)) := by rw [not_bddAbove_iff] @@ -347,12 +347,12 @@ def derivBFamily (o : Ordinal.{u}) (f : ∀ b < o, Ordinal.{max u v} → Ordinal Ordinal.{max u v} → Ordinal.{max u v} := derivFamily (familyOfBFamily o f) -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem derivBFamily_eq_derivFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) : derivBFamily.{u, v} o f = derivFamily (familyOfBFamily o f) := rfl -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem isNormal_derivBFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) : IsNormal (derivBFamily o f) := isNormal_derivFamily _ @@ -360,7 +360,7 @@ theorem isNormal_derivBFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) @[deprecated isNormal_derivBFamily (since := "2024-10-11")] alias derivBFamily_isNormal := isNormal_derivBFamily -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem derivBFamily_fp {i hi} (H : IsNormal (f i hi)) (a : Ordinal) : f i hi (derivBFamily.{u, v} o f a) = derivBFamily.{u, v} o f a := by rw [← familyOfBFamily_enum o f] @@ -368,7 +368,7 @@ theorem derivBFamily_fp {i hi} (H : IsNormal (f i hi)) (a : Ordinal) : rw [familyOfBFamily_enum] exact H -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem le_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} : (∀ i hi, f i hi a ≤ a) ↔ ∃ b, derivBFamily.{u, v} o f b = a := by unfold derivBFamily @@ -378,7 +378,7 @@ theorem le_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} : apply h · exact fun _ => H _ _ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem fp_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} : (∀ i hi, f i hi a = a) ↔ ∃ b, derivBFamily.{u, v} o f b = a := by rw [← le_iff_derivBFamily H] @@ -387,7 +387,7 @@ theorem fp_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} : exact h i hi /-- For a family of normal functions, `Ordinal.derivBFamily` enumerates the common fixed points. -/ -@[deprecated (since := "2024-10-14")] +@[deprecated "No deprecation message was provided." (since := "2024-10-14")] theorem derivBFamily_eq_enumOrd (H : ∀ i hi, IsNormal (f i hi)) : derivBFamily.{u, v} o f = enumOrd (⋂ (i) (hi), Function.fixedPoints (f i hi)) := by rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_bfamily H)] @@ -428,7 +428,7 @@ theorem iSup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) exact Ordinal.le_iSup _ _ set_option linter.deprecated false in -@[deprecated (since := "2024-08-27")] +@[deprecated "No deprecation message was provided." (since := "2024-08-27")] theorem sup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : (sup fun n : ℕ => f^[n] a) = nfp f a := by refine le_antisymm ?_ (sup_le fun l => ?_) @@ -580,7 +580,7 @@ theorem nfp_add_eq_mul_omega0 {a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * exact nfp_monotone (isNormal_add_right a).monotone (Ordinal.zero_le b) · dsimp; rw [← mul_one_add, one_add_omega0] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias nfp_add_eq_mul_omega := nfp_add_eq_mul_omega0 theorem add_eq_right_iff_mul_omega0_le {a b : Ordinal} : a + b = b ↔ a * ω ≤ b := by @@ -593,14 +593,14 @@ theorem add_eq_right_iff_mul_omega0_le {a b : Ordinal} : a + b = b ↔ a * ω nth_rw 1 [← this] rwa [← add_assoc, ← mul_one_add, one_add_omega0] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias add_eq_right_iff_mul_omega_le := add_eq_right_iff_mul_omega0_le theorem add_le_right_iff_mul_omega0_le {a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b := by rw [← add_eq_right_iff_mul_omega0_le] exact (isNormal_add_right a).le_iff_eq -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias add_le_right_iff_mul_omega_le := add_le_right_iff_mul_omega0_le theorem deriv_add_eq_mul_omega0_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * ω + b := by @@ -612,7 +612,7 @@ theorem deriv_add_eq_mul_omega0_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * · rw [deriv_succ, h, add_succ] exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 ((le_add_right _ _).trans (le_succ _))) -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias deriv_add_eq_mul_omega_add := deriv_add_eq_mul_omega0_add /-! ### Fixed points of multiplication -/ @@ -645,7 +645,7 @@ theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) rw [← nfp_mul_one ha] exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb) -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias nfp_mul_eq_opow_omega := nfp_mul_eq_opow_omega0 theorem eq_zero_or_opow_omega0_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = b) : @@ -659,7 +659,7 @@ theorem eq_zero_or_opow_omega0_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = rw [← Ne, ← one_le_iff_ne_zero] at hb exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab) -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias eq_zero_or_opow_omega_le_of_mul_eq_right := eq_zero_or_opow_omega0_le_of_mul_eq_right theorem mul_eq_right_iff_opow_omega0_dvd {a b : Ordinal} : a * b = b ↔ a ^ ω ∣ b := by @@ -677,7 +677,7 @@ theorem mul_eq_right_iff_opow_omega0_dvd {a b : Ordinal} : a * b = b ↔ a ^ ω cases' h with c hc rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias mul_eq_right_iff_opow_omega_dvd := mul_eq_right_iff_opow_omega0_dvd theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) : @@ -685,7 +685,7 @@ theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) : rw [← mul_eq_right_iff_opow_omega0_dvd] exact (isNormal_mul_right ha).le_iff_eq -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias mul_le_right_iff_opow_omega_dvd := mul_le_right_iff_opow_omega0_dvd theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c) @@ -705,7 +705,7 @@ theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c) rw [add_zero, mul_lt_mul_iff_left (opow_pos ω ha)] at this rwa [succ_le_iff] -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias nfp_mul_opow_omega_add := nfp_mul_opow_omega0_add theorem deriv_mul_eq_opow_omega0_mul {a : Ordinal.{u}} (ha : 0 < a) (b) : @@ -718,7 +718,7 @@ theorem deriv_mul_eq_opow_omega0_mul {a : Ordinal.{u}} (ha : 0 < a) (b) : · rw [deriv_succ, h] exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha)) -@[deprecated (since := "2024-09-30")] +@[deprecated "No deprecation message was provided." (since := "2024-09-30")] alias deriv_mul_eq_opow_omega_mul := deriv_mul_eq_opow_omega0_mul end Ordinal diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean index 5d6417f174042..194abeabc7c50 100644 --- a/Mathlib/SetTheory/Ordinal/Principal.lean +++ b/Mathlib/SetTheory/Ordinal/Principal.lean @@ -129,7 +129,7 @@ theorem not_bddAbove_principal (op : Ordinal → Ordinal → Ordinal) : exact ((le_nfp _ _).trans (ha (principal_nfp_iSup op (succ a)))).not_lt (lt_succ a) set_option linter.deprecated false in -@[deprecated (since := "2024-10-11")] +@[deprecated "No deprecation message was provided." (since := "2024-10-11")] theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) := by intro a b ha hb @@ -147,7 +147,7 @@ theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordin exact lt_blsub₂ (@fun a _ b _ => op a b) hm (hn.trans_le h) set_option linter.deprecated false in -@[deprecated (since := "2024-10-11")] +@[deprecated "No deprecation message was provided." (since := "2024-10-11")] theorem unbounded_principal (op : Ordinal → Ordinal → Ordinal) : Set.Unbounded (· < ·) { o | Principal op o } := fun o => ⟨_, principal_nfp_blsub₂ op o, (le_nfp _ o).not_lt⟩ diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index c7a0c35cdfcef..a2b3354096bf0 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/Mathlib/SetTheory/ZFC/Basic.lean @@ -447,12 +447,12 @@ set_option linter.deprecated false /-- Function equivalence is defined so that `f ~ g` iff `∀ x y, x ~ y → f x ~ g y`. This extends to equivalence of `n`-ary functions. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Arity.Equiv : ∀ {n}, OfArity PSet.{u} PSet.{u} n → OfArity PSet.{u} PSet.{u} n → Prop | 0, a, b => PSet.Equiv a b | _ + 1, a, b => ∀ x y : PSet, PSet.Equiv x y → Arity.Equiv (a x) (b y) -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] theorem Arity.equiv_const {a : PSet.{u}} : ∀ n, Arity.Equiv (OfArity.const PSet.{u} a n) (OfArity.const PSet.{u} a n) | 0 => Equiv.rfl @@ -460,46 +460,46 @@ theorem Arity.equiv_const {a : PSet.{u}} : /-- `resp n` is the collection of n-ary functions on `PSet` that respect equivalence, i.e. when the inputs are equivalent the output is as well. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Resp (n) := { x : OfArity PSet.{u} PSet.{u} n // Arity.Equiv x x } -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] instance Resp.inhabited {n} : Inhabited (Resp n) := ⟨⟨OfArity.const _ default _, Arity.equiv_const _⟩⟩ /-- The `n`-ary image of a `(n + 1)`-ary function respecting equivalence as a function respecting equivalence. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Resp.f {n} (f : Resp (n + 1)) (x : PSet) : Resp n := ⟨f.1 x, f.2 _ _ <| Equiv.refl x⟩ /-- Function equivalence for functions respecting equivalence. See `PSet.Arity.Equiv`. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Resp.Equiv {n} (a b : Resp n) : Prop := Arity.Equiv a.1 b.1 -@[deprecated (since := "2024-09-02"), refl] +@[deprecated "No deprecation message was provided." (since := "2024-09-02"), refl] protected theorem Resp.Equiv.refl {n} (a : Resp n) : Resp.Equiv a a := a.2 -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] protected theorem Resp.Equiv.euc : ∀ {n} {a b c : Resp n}, Resp.Equiv a b → Resp.Equiv c b → Resp.Equiv a c | 0, _, _, _, hab, hcb => PSet.Equiv.euc hab hcb | n + 1, a, b, c, hab, hcb => fun x y h => @Resp.Equiv.euc n (a.f x) (b.f y) (c.f y) (hab _ _ h) (hcb _ _ <| PSet.Equiv.refl y) -@[deprecated (since := "2024-09-02"), symm] +@[deprecated "No deprecation message was provided." (since := "2024-09-02"), symm] protected theorem Resp.Equiv.symm {n} {a b : Resp n} : Resp.Equiv a b → Resp.Equiv b a := (Resp.Equiv.refl b).euc -@[deprecated (since := "2024-09-02"), trans] +@[deprecated "No deprecation message was provided." (since := "2024-09-02"), trans] protected theorem Resp.Equiv.trans {n} {x y z : Resp n} (h1 : Resp.Equiv x y) (h2 : Resp.Equiv y z) : Resp.Equiv x z := h1.euc h2.symm -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] instance Resp.setoid {n} : Setoid (Resp n) := ⟨Resp.Equiv, Resp.Equiv.refl, Resp.Equiv.symm, Resp.Equiv.trans⟩ @@ -611,7 +611,7 @@ set_option linter.deprecated false namespace Resp /-- Helper function for `PSet.eval`. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def evalAux : ∀ {n}, { f : Resp n → OfArity ZFSet.{u} ZFSet.{u} n // ∀ a b : Resp n, Resp.Equiv a b → f a = f b } @@ -626,11 +626,11 @@ def evalAux : evalAux.2 (Resp.f b z) (Resp.f c z) (h _ _ (PSet.Equiv.refl z))⟩ /-- An equivalence-respecting function yields an n-ary ZFC set function. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def eval (n) : Resp n → OfArity ZFSet.{u} ZFSet.{u} n := evalAux.1 -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] theorem eval_val {n f x} : (@eval (n + 1) f : ZFSet → OfArity ZFSet ZFSet n) ⟦x⟧ = eval n (Resp.f f x) := rfl @@ -640,24 +640,25 @@ end Resp /-- A set function is "definable" if it is the image of some n-ary pre-set function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] class inductive Definable (n) : OfArity ZFSet.{u} ZFSet.{u} n → Type (u + 1) | mk (f) : Definable n (Resp.eval n f) -attribute [deprecated (since := "2024-09-02"), instance] Definable.mk +attribute [deprecated "No deprecation message was provided." (since := "2024-09-02"), instance] + Definable.mk /-- The evaluation of a function respecting equivalence is definable, by that same function. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Definable.EqMk {n} (f) : ∀ {s : OfArity ZFSet.{u} ZFSet.{u} n} (_ : Resp.eval _ f = s), Definable n s | _, rfl => ⟨f⟩ /-- Turns a definable function into a function that respects equivalence. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] def Definable.Resp {n} : ∀ (s : OfArity ZFSet.{u} ZFSet.{u} n) [Definable n s], Resp n | _, ⟨f⟩ => f -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] theorem Definable.eq {n} : ∀ (s : OfArity ZFSet.{u} ZFSet.{u} n) [H : Definable n s], (@Definable.Resp n s H).eval _ = s | _, ⟨_⟩ => rfl @@ -670,7 +671,7 @@ open PSet ZFSet set_option linter.deprecated false in /-- All functions are classically definable. -/ -@[deprecated (since := "2024-09-02")] +@[deprecated "No deprecation message was provided." (since := "2024-09-02")] noncomputable def allDefinable : ∀ {n} (F : OfArity ZFSet ZFSet n), Definable n F | 0, F => let p := @Quotient.exists_rep PSet _ F @@ -706,7 +707,7 @@ theorem exact {x y : PSet} : mk x = mk y → PSet.Equiv x y := Quotient.exact set_option linter.deprecated false in -@[deprecated (since := "2024-09-02"), simp] +@[deprecated "No deprecation message was provided." (since := "2024-09-02"), simp] theorem eval_mk {n f x} : (@Resp.eval (n + 1) f : ZFSet → OfArity ZFSet ZFSet n) (mk x) = Resp.eval n (Resp.f f x) := rfl diff --git a/Mathlib/Topology/Algebra/ConstMulAction.lean b/Mathlib/Topology/Algebra/ConstMulAction.lean index 1da40dadc219d..44b6433923f59 100644 --- a/Mathlib/Topology/Algebra/ConstMulAction.lean +++ b/Mathlib/Topology/Algebra/ConstMulAction.lean @@ -266,7 +266,7 @@ theorem smul_mem_nhds_smul_iff {t : Set α} (g : G) {a : α} : g • t ∈ 𝓝 @[to_additive] alias ⟨_, smul_mem_nhds_smul⟩ := smul_mem_nhds_smul_iff -@[to_additive (attr := deprecated (since := "2024-08-06"))] +@[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-08-06"))] alias smul_mem_nhds := smul_mem_nhds_smul @[to_additive (attr := simp)] diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean index 91b1a4ca3bcd4..f7373a1da6da0 100644 --- a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean +++ b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean @@ -65,7 +65,8 @@ homomorphisms. Deprecated and changed from a `class` to a `structure`. Use `[MonoidHomClass F A B] [ContinuousMapClass F A B]` instead. -/ -@[to_additive (attr := deprecated (since := "2024-10-08"))] +@[to_additive (attr := deprecated "Use `[MonoidHomClass F A B] [ContinuousMapClass F A B]` instead." + (since := "2024-10-08"))] structure ContinuousMonoidHomClass (A B : outParam Type*) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] extends MonoidHomClass F A B, ContinuousMapClass F A B : Prop diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean index 4a2b490786409..e46af523bf2ca 100644 --- a/Mathlib/Topology/Algebra/Group/Quotient.lean +++ b/Mathlib/Topology/Algebra/Group/Quotient.lean @@ -76,7 +76,7 @@ instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace -@[to_additive (attr := deprecated (since := "2024-10-05"))] +@[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-10-05"))] theorem continuous_smul₁ (x : G ⧸ N) : Continuous fun g : G => g • x := continuous_id.smul continuous_const @@ -101,7 +101,7 @@ instance instSecondCountableTopology [SecondCountableTopology G] : SecondCountableTopology (G ⧸ N) := ContinuousConstSMul.secondCountableTopology -@[to_additive (attr := deprecated (since := "2024-08-05"))] +@[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-08-05"))] theorem nhds_one_isCountablyGenerated [FirstCountableTopology G] [N.Normal] : (𝓝 (1 : G ⧸ N)).IsCountablyGenerated := inferInstance @@ -117,7 +117,7 @@ instance instTopologicalGroup [N.Normal] : TopologicalGroup (G ⧸ N) where exact continuous_mk.comp continuous_mul continuous_inv := continuous_inv.quotient_map' _ -@[to_additive (attr := deprecated (since := "2024-08-05"))] +@[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-08-05"))] theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N) := instTopologicalGroup N diff --git a/Mathlib/Topology/LocalAtTarget.lean b/Mathlib/Topology/LocalAtTarget.lean index 9ab72631191fb..af16705f2ce51 100644 --- a/Mathlib/Topology/LocalAtTarget.lean +++ b/Mathlib/Topology/LocalAtTarget.lean @@ -82,7 +82,7 @@ theorem IsClosedMap.restrictPreimage (H : IsClosedMap f) (s : Set β) : simpa [isClosed_induced_iff] exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩ -@[deprecated (since := "2024-04-02")] +@[deprecated "No deprecation message was provided." (since := "2024-04-02")] theorem Set.restrictPreimage_isClosedMap (s : Set β) (H : IsClosedMap f) : IsClosedMap (s.restrictPreimage f) := H.restrictPreimage s @@ -94,7 +94,7 @@ theorem IsOpenMap.restrictPreimage (H : IsOpenMap f) (s : Set β) : simpa [isOpen_induced_iff] exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩ -@[deprecated (since := "2024-04-02")] +@[deprecated "No deprecation message was provided." (since := "2024-04-02")] theorem Set.restrictPreimage_isOpenMap (s : Set β) (H : IsOpenMap f) : IsOpenMap (s.restrictPreimage f) := H.restrictPreimage s diff --git a/Mathlib/Topology/MetricSpace/Polish.lean b/Mathlib/Topology/MetricSpace/Polish.lean index d1e851e3c7d44..93c053adc16d7 100644 --- a/Mathlib/Topology/MetricSpace/Polish.lean +++ b/Mathlib/Topology/MetricSpace/Polish.lean @@ -102,7 +102,7 @@ instance (priority := 100) instMetrizableSpace (α : Type*) [TopologicalSpace α letI := upgradePolishSpace α infer_instance -@[deprecated (since := "2024-02-23")] +@[deprecated "No deprecation message was provided." (since := "2024-02-23")] theorem t2Space (α : Type*) [TopologicalSpace α] [PolishSpace α] : T2Space α := inferInstance /-- A countable product of Polish spaces is Polish. -/ diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean index 64689fd04f3f0..931e8748cbfce 100644 --- a/Mathlib/Topology/NoetherianSpace.lean +++ b/Mathlib/Topology/NoetherianSpace.lean @@ -98,7 +98,7 @@ theorem noetherianSpace_iff_isCompact : NoetherianSpace α ↔ ∀ s : Set α, I instance [NoetherianSpace α] : WellFoundedLT (Closeds α) := Iff.mp ((noetherianSpace_TFAE α).out 0 1) ‹_› -@[deprecated (since := "2024-10-07")] +@[deprecated "No deprecation message was provided." (since := "2024-10-07")] theorem NoetherianSpace.wellFounded_closeds [NoetherianSpace α] : WellFounded fun s t : Closeds α => s < t := wellFounded_lt diff --git a/Mathlib/Topology/Order/OrderClosed.lean b/Mathlib/Topology/Order/OrderClosed.lean index 7ded140f87a07..46e8626f54295 100644 --- a/Mathlib/Topology/Order/OrderClosed.lean +++ b/Mathlib/Topology/Order/OrderClosed.lean @@ -368,7 +368,7 @@ variable [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → theorem isClosed_Ici {a : α} : IsClosed (Ici a) := ClosedIciTopology.isClosed_Ici a -@[deprecated (since := "2024-02-15")] +@[deprecated "No deprecation message was provided." (since := "2024-02-15")] lemma ClosedIciTopology.isClosed_ge' (a : α) : IsClosed {x | a ≤ x} := isClosed_Ici a export ClosedIciTopology (isClosed_ge')