chore: remove many set_option linter.deprecated false (leanprover-community#40018)

Since v4.31.rc0, the "deprecated declaration" linter warning is automatically silenced when a deprecated declaration is used _inside another one_. Hence most of the 400 manual disablements of this linter in mathlib can be removed.

Author: loefflerd

Mathlib/Algebra/Group/Finsupp.lean

@@ -86,7 +86,6 @@ noncomputable def uniqueAddEquiv (i : ι) [Subsingleton ι] : (ι →₀ M) ≃+
 @[simp↓ high] lemma uniqueAddEquiv_symm_apply_apply (i : ι) [Subsingleton ι] (m : M) (j : ι) :
     (uniqueAddEquiv i).symm m j = m := by simp [Subsingleton.elim j i]
 
-set_option linter.deprecated false in
 /-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
 is isomorphic to `M`. -/
 @[simps!, deprecated uniqueAddEquiv (since := "2026-05-06")]
@@ -173,7 +172,6 @@ lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g
   refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩ <;>
   exact subset_trans Finsupp.support_single_subset (by simp)
 
-set_option linter.deprecated false in
 @[deprecated uniqueAddEquiv_symm_apply (since := "2026-05-06")]
 lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
     AddEquiv.finsuppUnique.symm d = single () d := by ext; simp [AddEquiv.finsuppUnique]

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -123,14 +123,12 @@ polynomials over the ground ring. -/
 @[deprecated uniqueAlgEquiv (since := "2026-04-15")]
 abbrev pUnitAlgEquiv := uniqueAlgEquiv (R := R) PUnit
 
-set_option linter.deprecated false in
 @[deprecated uniqueAlgEquiv_monomial (since := "2026-04-15")]
 theorem pUnitAlgEquiv_monomial {d : PUnit →₀ ℕ} {r : R} :
     MvPolynomial.pUnitAlgEquiv R (MvPolynomial.monomial d r)
       = Polynomial.monomial (d ()) r :=
   uniqueAlgEquiv_monomial _
 
-set_option linter.deprecated false in
 @[deprecated uniqueAlgEquiv_symm_monomial (since := "2026-04-15")]
 theorem pUnitAlgEquiv_symm_monomial {d : PUnit →₀ ℕ} {r : R} :
     (MvPolynomial.pUnitAlgEquiv R).symm (Polynomial.monomial (d ()) r)
@@ -230,27 +228,23 @@ theorem eval₂_const_uniqueAlgEquiv [Unique σ] {f : MvPolynomial σ R}
       f.eval₂ φ (fun _ ↦ a) := by
   rw [← eval₂_uniqueAlgEquiv]
 
-set_option linter.deprecated false in
 @[deprecated eval₂_uniqueAlgEquiv_symm (since := "2026-04-15")]
 theorem eval₂_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : Unit → S} :
     ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ a =
       f.eval₂ φ (a ()) :=
   eval₂_uniqueAlgEquiv_symm
 
-set_option linter.deprecated false in
 @[deprecated eval₂_const_uniqueAlgEquiv_symm (since := "2026-04-15")]
 theorem eval₂_const_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : S} :
     ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ (fun _ ↦ a) =
       f.eval₂ φ a :=
   eval₂_const_uniqueAlgEquiv_symm
 
-set_option linter.deprecated false in
 @[deprecated eval₂_uniqueAlgEquiv (since := "2026-04-15")]
 theorem eval₂_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : PUnit → S} :
     ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a :=
   eval₂_uniqueAlgEquiv
 
-set_option linter.deprecated false in
 @[deprecated eval₂_const_uniqueAlgEquiv (since := "2026-04-15")]
 theorem eval₂_const_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : S} :
     ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a) :=

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

@@ -413,7 +413,6 @@ section ModularScalarTowers
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 def coe (g : SL(2, ℤ)) : GL(2, ℝ)⁺ := ((g : SL(2, ℝ)) : GL(2, ℝ)⁺)
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 lemma coe_inj (a b : SL(2, ℤ)) : coe a = coe b ↔ a = b := by
   refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
@@ -424,22 +423,18 @@ lemma coe_inj (a b : SL(2, ℤ)) : coe a = coe b ↔ a = b := by
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 def coeHom : SL(2, ℤ) →* GL(2, ℝ)⁺ := toGLPos.comp <| map <| Int.castRingHom _
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 lemma coeHom_apply (g : SL(2, ℤ)) : coeHom g = coe g := rfl
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 theorem coe_apply_complex {g : SL(2, ℤ)} {i j : Fin 2} :
     (Units.val <| Subtype.val <| coe g) i j = (Subtype.val g i j : ℂ) :=
   rfl
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 theorem det_coe {g : SL(2, ℤ)} : det (Units.val <| Subtype.val <| coe g) = 1 := by
   simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe]
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 lemma coe_one : coe 1 = 1 := by
   simp only [coe, map_one]
@@ -456,7 +451,6 @@ theorem SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) :
     (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
   rfl
 
-set_option linter.deprecated false in
 @[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]
 lemma SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ where
   smul_assoc s g z := by

Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

@@ -132,13 +132,11 @@ theorem decompLinearIsometryEquiv_symm_contLinear (p : W × (V →L[𝕜] W)) :
   inherit_doc decompLinearIsometryEquiv]
 abbrev toConstProdContinuousLinearMap := decompLinearIsometryEquiv 𝕜 𝕜 V W
 
-set_option linter.deprecated false in
 @[deprecated fst_decompLinearIsometryEquiv (since := "2026-03-03")]
 theorem toConstProdContinuousLinearMap_fst (f : V →ᴬ[𝕜] W) :
     (toConstProdContinuousLinearMap 𝕜 V W f).fst = f 0 :=
   rfl
 
-set_option linter.deprecated false in
 @[deprecated snd_decompLinearIsometryEquiv (since := "2026-03-03")]
 theorem toConstProdContinuousLinearMap_snd (f : V →ᴬ[𝕜] W) :
     (toConstProdContinuousLinearMap 𝕜 V W f).snd = f.contLinear :=