chore: remove >9 month old deprecations (leanprover-community#20505)

Author: kim-em

Mathlib/Algebra/Algebra/Operations.lean

@@ -144,10 +144,6 @@ theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
 instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le :=
   ⟨fun _ _ => smul_mono le_rfl⟩
 
-@[deprecated smul_mono_right (since := "2024-03-31")]
-protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
-  _root_.smul_mono_right I h
-
 variable (I J N P)
 
 @[simp]
@@ -180,10 +176,6 @@ protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module
       (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
       fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
 
-@[deprecated smul_inf_le (since := "2024-03-31")]
-protected theorem smul_inf_le (M₁ M₂ : Submodule R M) :
-    I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _
-
 theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
     I • (⨆ i, t i)= ⨆ i, I • t i :=
   toAddSubmonoid_injective <| by
@@ -196,11 +188,6 @@ theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} :
     (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
     (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)
 
-@[deprecated smul_iInf_le (since := "2024-03-31")]
-protected theorem smul_iInf_le {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
-    I • iInf t ≤ ⨅ i, I • t i :=
-  smul_iInf_le
-
 protected theorem one_smul : (1 : Submodule R A) • N = N := by
   refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
   · obtain ⟨r, rfl⟩ := hr

Mathlib/Algebra/Associated/Basic.lean

@@ -581,7 +581,6 @@ theorem mk_le_mk_of_dvd {a b : M} : a ∣ b → Associates.mk a ≤ Associates.m
 
 theorem mk_le_mk_iff_dvd {a b : M} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b := mk_dvd_mk
 
-@[deprecated (since := "2024-03-16")] alias mk_le_mk_iff_dvd_iff := mk_le_mk_iff_dvd
 
 @[simp]
 theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by
@@ -591,7 +590,6 @@ theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by
     exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
   · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩
 
-@[deprecated (since := "2024-03-16")] alias isPrimal_iff := isPrimal_mk
 
 @[simp]
 theorem decompositionMonoid_iff : DecompositionMonoid (Associates M) ↔ DecompositionMonoid M := by

Mathlib/Algebra/CharP/Reduced.lean

@@ -44,6 +44,3 @@ theorem ExpChar.pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [ExpChar R p] (x : R)
   rw [pow_mul']
   convert ← (iterateFrobenius_inj R p k).eq_iff
   apply map_one
-
-@[deprecated (since := "2024-02-02")]
-alias CharP.pow_prime_pow_mul_eq_one_iff := ExpChar.pow_prime_pow_mul_eq_one_iff

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -805,9 +805,6 @@ theorem lcm_eq_of_associated_right [NormalizedGCDMonoid α] {m n : α} (h : Asso
 
 end LCM
 
-@[deprecated (since := "2024-02-12")] alias GCDMonoid.prime_of_irreducible := Irreducible.prime
-@[deprecated (since := "2024-02-12")] alias GCDMonoid.irreducible_iff_prime := irreducible_iff_prime
-
 end GCDMonoid
 
 section UniqueUnit

Mathlib/Algebra/Group/Basic.lean

@@ -797,14 +797,6 @@ theorem leftInverse_inv_mul_mul_right (c : G) :
 @[to_additive (attr := simp) natAbs_nsmul_eq_zero]
 lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1 := by cases n <;> simp
 
-set_option linter.existingAttributeWarning false in
-@[to_additive, deprecated pow_natAbs_eq_one (since := "2024-02-14")]
-lemma exists_pow_eq_one_of_zpow_eq_one (hn : n ≠ 0) (h : a ^ n = 1) :
-    ∃ n : ℕ, 0 < n ∧ a ^ n = 1 := ⟨_, Int.natAbs_pos.2 hn, pow_natAbs_eq_one.2 h⟩
-
-attribute [deprecated natAbs_nsmul_eq_zero (since := "2024-02-14")]
-exists_nsmul_eq_zero_of_zsmul_eq_zero
-
 @[to_additive sub_nsmul]
 lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
   eq_mul_inv_of_mul_eq <| by rw [← pow_add, Nat.sub_add_cancel h]
@@ -1041,15 +1033,5 @@ theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a →
 
 end multiplicative
 
-@[deprecated (since := "2024-03-20")] alias div_mul_cancel' := div_mul_cancel
-@[deprecated (since := "2024-03-20")] alias mul_div_cancel'' := mul_div_cancel_right
 -- The name `add_sub_cancel` was reused
 -- @[deprecated (since := "2024-03-20")] alias add_sub_cancel := add_sub_cancel_right
-@[deprecated (since := "2024-03-20")] alias div_mul_cancel''' := div_mul_cancel_right
-@[deprecated (since := "2024-03-20")] alias sub_add_cancel'' := sub_add_cancel_right
-@[deprecated (since := "2024-03-20")] alias mul_div_cancel''' := mul_div_cancel_left
-@[deprecated (since := "2024-03-20")] alias add_sub_cancel' := add_sub_cancel_left
-@[deprecated (since := "2024-03-20")] alias mul_div_cancel'_right := mul_div_cancel
-@[deprecated (since := "2024-03-20")] alias add_sub_cancel'_right := add_sub_cancel
-@[deprecated (since := "2024-03-20")] alias div_mul_cancel'' := div_mul_cancel_left
-@[deprecated (since := "2024-03-20")] alias sub_add_cancel' := sub_add_cancel_left

Mathlib/Algebra/Group/Defs.lean

@@ -886,8 +886,6 @@ theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
     _ = a ^ n * a := congrArg (· * a) (zpow_natCast a n)
     _ = a ^ (n + 1) := (pow_succ _ _).symm
 
-@[deprecated (since := "2024-03-20")] alias zpow_coe_nat := zpow_natCast
-@[deprecated (since := "2024-03-20")] alias coe_nat_zsmul := natCast_zsmul
 
 @[to_additive ofNat_zsmul]
 lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n :=

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -625,23 +625,6 @@ instance (priority := 100) of_covariant_left [IsLeftCancelMul G]
 
 end TwoUniqueProds
 
-@[deprecated (since := "2024-02-04")]
-alias UniqueProds.mulHom_image_of_injective := UniqueProds.of_injective_mulHom
-@[deprecated (since := "2024-02-04")]
-alias UniqueSums.addHom_image_of_injective := UniqueSums.of_injective_addHom
-@[deprecated (since := "2024-02-04")]
-alias UniqueProds.mulHom_image_iff := MulEquiv.uniqueProds_iff
-@[deprecated (since := "2024-02-04")]
-alias UniqueSums.addHom_image_iff := AddEquiv.uniqueSums_iff
-@[deprecated (since := "2024-02-04")]
-alias TwoUniqueProds.mulHom_image_of_injective := TwoUniqueProds.of_injective_mulHom
-@[deprecated (since := "2024-02-04")]
-alias TwoUniqueSums.addHom_image_of_injective := TwoUniqueSums.of_injective_addHom
-@[deprecated (since := "2024-02-04")]
-alias TwoUniqueProds.mulHom_image_iff := MulEquiv.twoUniqueProds_iff
-@[deprecated (since := "2024-02-04")]
-alias TwoUniqueSums.addHom_image_iff := AddEquiv.twoUniqueSums_iff
-
 instance {ι} (G : ι → Type*) [∀ i, AddZeroClass (G i)] [∀ i, TwoUniqueSums (G i)] :
     TwoUniqueSums (Π₀ i, G i) :=
   TwoUniqueSums.of_injective_addHom

Mathlib/Algebra/Group/Units/Basic.lean

@@ -474,5 +474,3 @@ attribute [deprecated sub_add_cancel_left (since := "2024-03-20")] IsAddUnit.sub
 -- @[deprecated (since := "2024-03-20")] alias IsUnit.mul_div_cancel := IsUnit.mul_div_cancel_right
 -- @[deprecated (since := "2024-03-20")]
 -- alias IsAddUnit.add_sub_cancel := IsAddUnit.add_sub_cancel_right
-@[deprecated (since := "2024-03-20")] alias IsUnit.mul_div_cancel' := IsUnit.mul_div_cancel
-@[deprecated (since := "2024-03-20")] alias IsAddUnit.add_sub_cancel' := IsAddUnit.add_sub_cancel

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -315,10 +315,6 @@ lemma div_eq_one_iff_eq (hb : b ≠ 0) : a / b = 1 ↔ a = b := hb.isUnit.div_eq
 lemma div_mul_cancel_right₀ (hb : b ≠ 0) (a : G₀) : b / (a * b) = a⁻¹ :=
   hb.isUnit.div_mul_cancel_right _
 
-set_option linter.deprecated false in
-@[deprecated div_mul_cancel_right₀ (since := "2024-03-20")]
-lemma div_mul_left (hb : b ≠ 0) : b / (a * b) = 1 / a := hb.isUnit.div_mul_left
-
 lemma mul_div_mul_right (a b : G₀) (hc : c ≠ 0) : a * c / (b * c) = a / b :=
   hc.isUnit.mul_div_mul_right _ _
 
@@ -415,10 +411,6 @@ instance (priority := 100) CommGroupWithZero.toDivisionCommMonoid :
 lemma div_mul_cancel_left₀ (ha : a ≠ 0) (b : G₀) : a / (a * b) = b⁻¹ :=
   ha.isUnit.div_mul_cancel_left _
 
-@[deprecated div_mul_cancel_left₀ (since := "2024-03-22")]
-lemma div_mul_right (b : G₀) (ha : a ≠ 0) : a / (a * b) = 1 / b := by
-  simp [div_mul_cancel_left₀ ha]
-
 lemma mul_div_cancel_left_of_imp (h : a = 0 → b = 0) : a * b / a = b := by
   rw [mul_comm, mul_div_cancel_of_imp h]
 
@@ -485,5 +477,3 @@ noncomputable def commGroupWithZeroOfIsUnitOrEqZero [hM : CommMonoidWithZero M]
   { groupWithZeroOfIsUnitOrEqZero h, hM with }
 
 end NoncomputableDefs
-
-@[deprecated (since := "2024-03-20")] alias mul_div_cancel' := mul_div_cancel₀

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -347,11 +347,6 @@ instance : CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le :=
   ⟨fun _ _ _ le => set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr)
     (mem2 := le hm)⟩
 
-@[deprecated smul_mono_right (since := "2024-03-31")]
-theorem set_smul_mono_right {p q : Submodule R M} (le : p ≤ q) :
-    s • p ≤ s • q :=
-  smul_mono_right s le
-
 lemma set_smul_mono_left {s t : Set S} (le : s ≤ t) :
     s • N ≤ t • N :=
   set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := le hr)