chore: remove June 2025 deprecated declarations (leanprover-community#33429)

The first commit is the result of running
```lean
import Mathlib
import Archive
import Counterexamples

#clear_deprecations "2025-06-01" "2025-06-30" really
```
For the two removed files in the second commit I argue that they effectively _were_ `deprecated_module`s on the same day as their last deprecation was added; they consist entirely of deprecated declarations more than 6 months old, so there is no need to add a module deprecation.

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib.lean

@@ -497,7 +497,6 @@ public import Mathlib.Algebra.GroupWithZero.Hom
 public import Mathlib.Algebra.GroupWithZero.Idempotent
 public import Mathlib.Algebra.GroupWithZero.Indicator
 public import Mathlib.Algebra.GroupWithZero.InjSurj
-public import Mathlib.Algebra.GroupWithZero.Int
 public import Mathlib.Algebra.GroupWithZero.Invertible
 public import Mathlib.Algebra.GroupWithZero.Nat
 public import Mathlib.Algebra.GroupWithZero.NeZero
@@ -4050,7 +4049,6 @@ public import Mathlib.Deprecated.Aliases
 public import Mathlib.Deprecated.Estimator
 public import Mathlib.Deprecated.MLList.BestFirst
 public import Mathlib.Deprecated.Order
-public import Mathlib.Deprecated.RingHom
 public import Mathlib.Deprecated.Sort
 public import Mathlib.Dynamics.BirkhoffSum.Average
 public import Mathlib.Dynamics.BirkhoffSum.Basic

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

@@ -200,12 +200,6 @@ theorem prod_disjSum (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
   rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
   rfl
 
-@[deprecated (since := "2025-06-11")]
-alias sum_disj_sum := sum_disjSum
-
-@[to_additive existing, deprecated (since := "2025-06-11")]
-alias prod_disj_sum := prod_disjSum
-
 @[to_additive]
 lemma prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M) :
     ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) := by

Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean

@@ -40,14 +40,6 @@ def uliftZMultiplesHom (G : Type u) [AddGroup G] : G ≃ (ULift.{u} ℤ →+ G)
 def uliftZPowersHom (G : Type u) [Group G] : G ≃ (ULift.{u} (Multiplicative ℤ) →* G) :=
   (zpowersHom _).trans MulEquiv.ulift.symm.monoidHomCongrLeftEquiv
 
-namespace MonoidHom
-
-end MonoidHom
-
-namespace AddMonoidHom
-
-end AddMonoidHom
-
 /-- The forget functor `GrpCat.{u} ⥤ Type u` is corepresentable. -/
 def GrpCat.coyonedaObjIsoForget :
     coyoneda.obj (op (of (ULift.{u} (Multiplicative ℤ)))) ≅ forget GrpCat.{u} :=

Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

@@ -45,14 +45,6 @@ of `Multiplicative.ofAdd 1`. -/
 def uliftPowersHom (M : Type u) [Monoid M] : M ≃ (ULift.{u} (Multiplicative ℕ) →* M) :=
   (powersHom _).trans MulEquiv.ulift.symm.monoidHomCongrLeftEquiv
 
-namespace MonoidHom
-
-end MonoidHom
-
-namespace AddMonoidHom
-
-end AddMonoidHom
-
 /-- The forgetful functor `MonCat.{u} ⥤ Type u` is corepresentable. -/
 def MonCat.coyonedaObjIsoForget :
     coyoneda.obj (op (of (ULift.{u} (Multiplicative ℕ)))) ≅ forget MonCat.{u} :=

Mathlib/Algebra/Group/Irreducible/Defs.lean

@@ -47,10 +47,6 @@ structure Irreducible (p : M) : Prop where
   /-- If an irreducible element factors, then one factor is a unit. -/
   isUnit_or_isUnit ⦃a b : M⦄ : p = a * b → IsUnit a ∨ IsUnit b
 
-namespace Irreducible
-
-end Irreducible
-
 @[to_additive] lemma irreducible_iff :
     Irreducible p ↔ ¬IsUnit p ∧ ∀ ⦃a b⦄, p = a * b → IsUnit a ∨ IsUnit b where
   mp hp := ⟨hp.not_isUnit, hp.isUnit_or_isUnit⟩

Mathlib/Algebra/Group/Units/Defs.lean

@@ -121,8 +121,6 @@ theorem ext {u v : αˣ} (huv : u.val = v.val) : u = v := val_injective huv
 theorem val_inj {a b : αˣ} : (a : α) = b ↔ a = b :=
   val_injective.eq_iff
 
-@[to_additive (attr := deprecated val_inj (since := "2025-06-21"))] alias eq_iff := val_inj
-
 /-- Units have decidable equality if the base `Monoid` has decidable equality. -/
 @[to_additive /-- Additive units have decidable equality
 if the base `AddMonoid` has decidable equality. -/]

Mathlib/Algebra/GroupWithZero/Int.lean

@@ -687,8 +687,6 @@ variable {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
 variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
 variable (e : M ≃ₛₗ[σ₁₂] M₂)
 
-@[deprecated (since := "2025-06-18")] alias map_eq_comap := Submodule.map_equiv_eq_comap_symm
-
 /-- A linear equivalence of two modules restricts to a linear equivalence from any submodule
 `p` of the domain onto the image of that submodule.
 

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -346,8 +346,6 @@ def MapSubtype.orderIso : Submodule R p ≃o { p' : Submodule R M // p' ≤ p }
     rw [map_le_iff_le_comap,
       comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]
 
-@[deprecated (since := "2025-06-03")] alias MapSubtype.relIso := MapSubtype.orderIso
-
 /-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
 submodules of `M`. -/
 def MapSubtype.orderEmbedding : Submodule R p ↪o Submodule R M :=

Mathlib/Algebra/Module/Submodule/Range.lean

@@ -39,10 +39,6 @@ variable [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
   obtain ha | ha := le_total a 0 <;>
     simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos]
 
-@[deprecated abs_smul (since := "2025-06-24")]
-lemma abs_qsmul [Module ℚ α] [PosSMulMono ℚ α] (q : ℚ) (a : α) :
-    |q • a| = |q| • |a| := abs_smul q a
-
 end LinearOrderedAddCommGroup
 
 section LinearOrderedSemifield