chore: cleanup set_option linter.deprecated (#19701)

Remove several uses of deprecated lemmas in non-deprecated lemmas.

Also convert all `set_option linter.deprecated false` to `set_option linter.deprecated false in`, so it is easier for us to count via regex what remains.

I think
```
set_option linter\.deprecated false.*(?:(?:\n/--.*?-/\n(?!.*deprecated))|\n(?!.*deprecated|/--))
```
is the correct regex to use now: it accounts properly for intervening doc-strings. It now reports that there are only ~~three~~ one! file~~s~~ that use `set_option linter.deprecated false` on non-deprecated declarations, namely:

* ~~Mathlib.Data.List.Permutation~~ (fixed by moving some List theorems earlier)
* ~~Mathlib.LinearAlgebra.CliffordAlgebra.Grading~~ (replace `AlgHom.map_zero` with just `map_zero`; only costs 2000 heartbeats)
* Mathlib.SetTheory.Ordinal.Arithmetic (which is a mess)

Author: kim-em

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Int
+import Mathlib.Data.List.Lemmas
 import Mathlib.Data.List.Dedup
 import Mathlib.Data.List.Flatten
 import Mathlib.Data.List.Pairwise
@@ -661,22 +662,10 @@ lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
     (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by
   rw [← mem_range, ← ranges_flatten, mem_flatten]
 
-@[simp]
-theorem length_flatMap (l : List α) (f : α → List β) :
-    length (List.flatMap l f) = sum (map (length ∘ f) l) := by
-  rw [List.flatMap, length_flatten, map_map]
-
 @[deprecated (since := "2024-10-16")] alias length_bind := length_flatMap
 
-lemma countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
-    countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
-  rw [List.flatMap, countP_flatten, map_map]
-
 @[deprecated (since := "2024-10-16")] alias countP_bind := countP_flatMap
 
-lemma count_flatMap [BEq β] (l : List α) (f : α → List β) (x : β) :
-    count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _
-
 @[deprecated (since := "2024-10-16")] alias count_bind := count_flatMap
 
 /-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the

Mathlib/Analysis/Analytic/Composition.lean

@@ -1051,16 +1051,15 @@ theorem length_sigmaCompositionAux (a : Composition n) (b : Composition a.length
   show List.length ((splitWrtComposition a.blocks b)[i.1]) = blocksFun b i by
     rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _)]; rfl
 
-set_option linter.deprecated false in
 theorem blocksFun_sigmaCompositionAux (a : Composition n) (b : Composition a.length)
     (i : Fin b.length) (j : Fin (blocksFun b i)) :
     blocksFun (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ i.2⟩)
         ⟨j, (length_sigmaCompositionAux a b i).symm ▸ j.2⟩ =
-      blocksFun a (embedding b i j) :=
-  show get (get _ ⟨_, _⟩) ⟨_, _⟩  = a.blocks.get ⟨_, _⟩ by
-    rw [get_of_eq (get_splitWrtComposition _ _ _), get_drop', get_take']; rfl
+      blocksFun a (embedding b i j) := by
+  unfold sigmaCompositionAux
+  rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _),
+    getElem_drop, getElem_take]; rfl
 
-set_option linter.deprecated false in
 /-- Auxiliary lemma to prove that the composition of formal multilinear series is associative.
 
 Consider a composition `a` of `n` and a composition `b` of `a.length`. Grouping together some

Mathlib/Data/List/Basic.lean

@@ -831,17 +831,13 @@ theorem get_reverse (l : List α) (i : Nat) (h1 h2) :
   dsimp
   omega
 
-set_option linter.deprecated false
-
 theorem get_reverse' (l : List α) (n) (hn') :
     l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩ := by
-  rw [eq_comm]
-  convert get_reverse l.reverse n (by simpa) n.2 using 1
   simp
 
 theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) : l = [l.get ⟨0, by omega⟩] := by
   refine ext_get (by convert h) fun n h₁ h₂ => ?_
-  simp only [get_singleton]
+  simp
   congr
   omega
 

Mathlib/Data/List/Lemmas.lean

@@ -17,6 +17,18 @@ variable {α β γ : Type*}
 
 namespace List
 
+@[simp]
+theorem length_flatMap (l : List α) (f : α → List β) :
+    length (List.flatMap l f) = sum (map (length ∘ f) l) := by
+  rw [List.flatMap, length_flatten, map_map]
+
+lemma countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
+    countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
+  rw [List.flatMap, countP_flatten, map_map]
+
+lemma count_flatMap [BEq β] (l : List α) (f : α → List β) (x : β) :
+    count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _
+
 @[deprecated (since := "2024-08-20")] alias getElem_reverse' := getElem_reverse
 
 theorem tail_reverse_eq_reverse_dropLast (l : List α) :

Mathlib/Data/List/Permutation.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import Mathlib.Data.List.Flatten
+import Mathlib.Data.List.Lemmas
 import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Data.List.Count
 import Mathlib.Data.List.Duplicate
@@ -181,20 +181,18 @@ theorem mem_foldr_permutationsAux2 {t : α} {ts : List α} {r L : List (List α)
   simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap,
     append_assoc, cons_append, exists_prop]
 
-set_option linter.deprecated false in
 theorem length_foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
     length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) =
-      Nat.sum (map length L) + length r := by
-  simp [foldr_permutationsAux2, Function.comp_def, length_permutationsAux2, length_flatMap']
+      (map length L).sum + length r := by
+  simp [foldr_permutationsAux2, Function.comp_def, length_permutationsAux2, length_flatMap]
 
-set_option linter.deprecated false in
 theorem length_foldr_permutationsAux2' (t : α) (ts : List α) (r L : List (List α)) (n)
     (H : ∀ l ∈ L, length l = n) :
     length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) = n * length L + length r := by
-  rw [length_foldr_permutationsAux2, (_ : Nat.sum (map length L) = n * length L)]
+  rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]
   induction' L with l L ih
   · simp
-  have sum_map : Nat.sum (map length L) = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
+  have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
   have length_l : length l = n := H _ (mem_cons_self _ _)
   simp [sum_map, length_l, Nat.mul_add, Nat.add_comm, mul_succ]
 

Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

@@ -99,8 +99,7 @@ theorem GradedAlgebra.lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') :
       · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
       rfl
   | zero =>
-    set_option linter.deprecated false in
-    rw [AlgHom.map_zero]
+    rw [map_zero]
     apply Eq.symm
     apply DFinsupp.single_eq_zero.mpr; rfl
   | add x y hx hy ihx ihy =>

Mathlib/LinearAlgebra/Prod.lean

@@ -830,20 +830,21 @@ variable {N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
 
 open Function
 
-set_option linter.deprecated false
-
+set_option linter.deprecated false in
 /-- 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 "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
 
+set_option linter.deprecated false in
 @[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
 
+set_option linter.deprecated false in
 /-- Auxiliary definition for `tunnel`. -/
 @[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
@@ -853,6 +854,7 @@ def tunnel' (f : M × N →ₗ[R] M) (i : Injective f) : ℕ → ΣK : Submodule
       ((Submodule.fst R M N).equivMapOfInjective _
         (tunnelAux_injective f i (tunnel' f i n))).symm.trans (Submodule.fstEquiv R M N)⟩
 
+set_option linter.deprecated false in
 /-- Give an injective map `f : M × N →ₗ[R] M` we can find a nested sequence of submodules
 all isomorphic to `M`.
 -/
@@ -865,26 +867,30 @@ def tunnel (f : M × N →ₗ[R] M) (i : Injective f) : ℕ →o (Submodule R M)
       rw [Submodule.map_comp, Submodule.map_comp]
       apply Submodule.map_subtype_le⟩
 
+set_option linter.deprecated false in
 /-- Give an injective map `f : M × N →ₗ[R] M` we can find a sequence of submodules
 all isomorphic to `N`.
 -/
 @[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))
 
+set_option linter.deprecated false in
 /-- Each `tailing f i n` is a copy of `N`. -/
 @[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)
 
+set_option linter.deprecated false in
 @[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
 
+set_option linter.deprecated false in
 @[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
@@ -894,6 +900,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]
 
+set_option linter.deprecated false in
 @[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)) ≤
@@ -902,19 +909,23 @@ theorem tailing_sup_tunnel_succ_le_tunnel (f : M × N →ₗ[R] M) (i : Injectiv
   rw [← Submodule.map_sup, sup_comm, Submodule.fst_sup_snd, Submodule.map_comp, Submodule.map_comp]
   apply Submodule.map_subtype_le
 
+set_option linter.deprecated false in
 /-- The supremum of all the copies of `N` found inside the tunnel. -/
 @[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)
 
+set_option linter.deprecated false in
 @[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]
 
+set_option linter.deprecated false in
 @[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]
 
+set_option linter.deprecated false in
 @[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
@@ -927,6 +938,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
 
+set_option linter.deprecated false in
 @[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)) :=

Mathlib/Order/Extension/Well.lean

@@ -70,10 +70,9 @@ end IsWellFounded
 
 namespace WellFounded
 
-set_option linter.deprecated false
-
 variable (hwf : WellFounded r)
 
+set_option linter.deprecated false in
 /-- An arbitrary well order on `α` that extends `r`.
 
 The construction maps `r` into two well-orders: the first map is `WellFounded.rank`, which is not
@@ -89,12 +88,14 @@ noncomputable def wellOrderExtension : LinearOrder α :=
   @LinearOrder.lift' α (Ordinal ×ₗ Cardinal) _ (fun a : α => (hwf.rank a, embeddingToCardinal a))
     fun _ _ h => embeddingToCardinal.injective <| congr_arg Prod.snd h
 
+set_option linter.deprecated false in
 @[deprecated IsWellFounded.wellOrderExtension.isWellFounded_lt (since := "2024-09-07")]
 instance wellOrderExtension.isWellFounded_lt : IsWellFounded α hwf.wellOrderExtension.lt :=
   ⟨InvImage.wf (fun a : α => (hwf.rank a, embeddingToCardinal a)) <|
     Ordinal.lt_wf.prod_lex Cardinal.lt_wf⟩
 
 include hwf in
+set_option linter.deprecated false in
 /-- Any well-founded relation can be extended to a well-ordering on that type. -/
 @[deprecated IsWellFounded.exists_well_order_ge (since := "2024-09-07")]
 theorem exists_well_order_ge : ∃ s, r ≤ s ∧ IsWellOrder α s :=