From 7342e3c1e1d175ae0faaffac048a3c3c10415671 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Wed, 22 Jan 2025 07:45:35 +0100
Subject: [PATCH 1/3] chore: rename List.indexOf_lt_length to
 List.indexOf_lt_length_iff

---
 Mathlib/Data/FinEnum.lean                    | 2 +-
 Mathlib/Data/List/Basic.lean                 | 8 ++++----
 Mathlib/Data/List/FinRange.lean              | 2 +-
 Mathlib/Data/List/Nodup.lean                 | 2 +-
 Mathlib/Data/List/NodupEquivFin.lean         | 4 ++--
 Mathlib/GroupTheory/Perm/Cycle/Basic.lean    | 2 +-
 Mathlib/LinearAlgebra/Multilinear/Basic.lean | 4 ++--
 7 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean
index 3d499baf8ef5b..d928b5d459a79 100644
--- a/Mathlib/Data/FinEnum.lean
+++ b/Mathlib/Data/FinEnum.lean
@@ -46,7 +46,7 @@ def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' :
     FinEnum α where
   card := xs.length
   equiv :=
-    ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length]; apply h⟩, xs.get, fun x => by simp,
+    ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length_iff]; apply h⟩, xs.get, fun x => by simp,
       fun i => by ext; simp [List.indexOf_getElem h']⟩
 
 /-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index 27e8037124589..b96a9724ec003 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -704,7 +704,7 @@ theorem indexOf_le_length {a : α} {l : List α} : indexOf a l ≤ length l := b
   · rw [if_pos h]; exact Nat.zero_le _
   · rw [if_neg h]; exact succ_le_succ ih
 
-theorem indexOf_lt_length {a} {l : List α} : indexOf a l < length l ↔ a ∈ l :=
+theorem indexOf_lt_length_iff {a} {l : List α} : indexOf a l < length l ↔ a ∈ l :=
   ⟨fun h => Decidable.byContradiction fun al => Nat.ne_of_lt h <| indexOf_eq_length.2 al,
    fun al => (lt_of_le_of_ne indexOf_le_length) fun h => indexOf_eq_length.1 h al⟩
 
@@ -799,7 +799,7 @@ theorem indexOf_get [DecidableEq α] {a : α} {l : List α} (h) : get l ⟨index
 
 @[simp]
 theorem getElem?_indexOf [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
-    l[indexOf a l]? = some a := by rw [getElem?_eq_getElem, getElem_indexOf (indexOf_lt_length.2 h)]
+    l[indexOf a l]? = some a := by rw [getElem?_eq_getElem, getElem_indexOf (indexOf_lt_length_iff.2 h)]
 
 -- This is incorrectly named and should be `get?_indexOf`;
 -- this already exists, so will require a deprecation dance.
@@ -810,8 +810,8 @@ theorem indexOf_inj [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy
     indexOf x l = indexOf y l ↔ x = y :=
   ⟨fun h => by
     have x_eq_y :
-        get l ⟨indexOf x l, indexOf_lt_length.2 hx⟩ =
-        get l ⟨indexOf y l, indexOf_lt_length.2 hy⟩ := by
+        get l ⟨indexOf x l, indexOf_lt_length_iff.2 hx⟩ =
+        get l ⟨indexOf y l, indexOf_lt_length_iff.2 hy⟩ := by
       simp only [h]
     simp only [indexOf_get] at x_eq_y; exact x_eq_y, fun h => by subst h; rfl⟩
 
diff --git a/Mathlib/Data/List/FinRange.lean b/Mathlib/Data/List/FinRange.lean
index 8281f5ce92052..de54055232145 100644
--- a/Mathlib/Data/List/FinRange.lean
+++ b/Mathlib/Data/List/FinRange.lean
@@ -61,7 +61,7 @@ theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
   List.ext_get (by simp) (by simp)
 
 @[simp] theorem indexOf_finRange {k : ℕ} (i : Fin k) : (finRange k).indexOf i = i := by
-  have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length.mpr (by simp)
+  have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length_iff.mpr (by simp)
   have h₁ : (finRange k).get ⟨(finRange k).indexOf i, this⟩ = i := indexOf_get this
   have h₂ : (finRange k).get ⟨i, by simp⟩ = i := get_finRange _
   simpa using (Nodup.get_inj_iff (nodup_finRange k)).mp (Eq.trans h₁ h₂.symm)
diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
index dfa426586cded..084e0e51bba63 100644
--- a/Mathlib/Data/List/Nodup.lean
+++ b/Mathlib/Data/List/Nodup.lean
@@ -122,7 +122,7 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
 
 theorem indexOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) :
     indexOf l[i] l = i :=
-  suffices (⟨indexOf l[i] l, indexOf_lt_length.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
+  suffices (⟨indexOf l[i] l, indexOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
     from Fin.val_eq_of_eq this
   nodup_iff_injective_get.1 H (by simp)
 
diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean
index 9b381e748861c..0edcc7b2aba6c 100644
--- a/Mathlib/Data/List/NodupEquivFin.lean
+++ b/Mathlib/Data/List/NodupEquivFin.lean
@@ -50,7 +50,7 @@ the set of elements of `l`. -/
 @[simps]
 def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where
   toFun i := ⟨get l i, get_mem _ _⟩
-  invFun x := ⟨indexOf (↑x) l, indexOf_lt_length.2 x.2⟩
+  invFun x := ⟨indexOf (↑x) l, indexOf_lt_length_iff.2 x.2⟩
   left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
   right_inv x := by simp
 
@@ -63,7 +63,7 @@ decidable equality. -/
 def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) :
     Fin l.length ≃ α where
   toFun i := l.get i
-  invFun a := ⟨_, indexOf_lt_length.2 (h a)⟩
+  invFun a := ⟨_, indexOf_lt_length_iff.2 (h a)⟩
   left_inv i := by simp [List.indexOf_getElem, nd]
   right_inv a := by simp
 
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index 7a9275a5282d0..27345289bc340 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -867,7 +867,7 @@ variable [DecidableEq α] {l : List α}
 theorem Nodup.isCycleOn_formPerm (h : l.Nodup) :
     l.formPerm.IsCycleOn { a | a ∈ l } := by
   refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
-  rw [Set.mem_setOf, ← List.indexOf_lt_length] at ha hb
+  rw [Set.mem_setOf, ← List.indexOf_lt_length_iff] at ha hb
   rw [← List.getElem_indexOf ha, ← List.getElem_indexOf hb]
   refine ⟨l.indexOf b - l.indexOf a, ?_⟩
   simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
index d8830d118642b..91124505b00ab 100644
--- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean
+++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
@@ -1155,13 +1155,13 @@ protected def mkPiAlgebraFin : MultilinearMap R (fun _ : Fin n => A) A where
   map_update_add' {dec} m i x y := by
     rw [Subsingleton.elim dec (by infer_instance)]
     have : (List.finRange n).indexOf i < n := by
-      simpa using List.indexOf_lt_length.2 (List.mem_finRange i)
+      simpa using List.indexOf_lt_length_iff.2 (List.mem_finRange i)
     simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul, this,
       mul_add, add_mul]
   map_update_smul' {dec} m i c x := by
     rw [Subsingleton.elim dec (by infer_instance)]
     have : (List.finRange n).indexOf i < n := by
-      simpa using List.indexOf_lt_length.2 (List.mem_finRange i)
+      simpa using List.indexOf_lt_length_iff.2 (List.mem_finRange i)
     simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, this]
 
 variable {R A n}

From 1f88a15352f2b531a923a95db955d1d32b8439ac Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Wed, 22 Jan 2025 07:51:34 +0100
Subject: [PATCH 2/3] add deprecation alias

---
 Mathlib/Data/List/Basic.lean | 2 ++
 scripts/add_deprecations.sh  | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index b96a9724ec003..c9e86c665aaa1 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -708,6 +708,8 @@ theorem indexOf_lt_length_iff {a} {l : List α} : indexOf a l < length l ↔ a 
   ⟨fun h => Decidable.byContradiction fun al => Nat.ne_of_lt h <| indexOf_eq_length.2 al,
    fun al => (lt_of_le_of_ne indexOf_le_length) fun h => indexOf_eq_length.1 h al⟩
 
+@[deprecated (since := "2025-01-22")] alias indexOf_lt_length := indexOf_lt_length_iff
+
 theorem indexOf_append_of_mem {a : α} (h : a ∈ l₁) : indexOf a (l₁ ++ l₂) = indexOf a l₁ := by
   induction' l₁ with d₁ t₁ ih
   · exfalso
diff --git a/scripts/add_deprecations.sh b/scripts/add_deprecations.sh
index ae89ebfeaf5d5..f3601dda6daed 100755
--- a/scripts/add_deprecations.sh
+++ b/scripts/add_deprecations.sh
@@ -1,4 +1,4 @@
-#! /bin/bash
+#! /usr/bin/env bash
 
  : <<'BASH_MODULE_DOC'
 

From 9004ae4b7063c861992355b3dcfa8569f17c42fa Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Wed, 22 Jan 2025 07:54:47 +0100
Subject: [PATCH 3/3] lint

---
 Mathlib/Data/List/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index c9e86c665aaa1..d51295c269ce1 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -801,7 +801,8 @@ theorem indexOf_get [DecidableEq α] {a : α} {l : List α} (h) : get l ⟨index
 
 @[simp]
 theorem getElem?_indexOf [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
-    l[indexOf a l]? = some a := by rw [getElem?_eq_getElem, getElem_indexOf (indexOf_lt_length_iff.2 h)]
+    l[indexOf a l]? = some a := by
+  rw [getElem?_eq_getElem, getElem_indexOf (indexOf_lt_length_iff.2 h)]
 
 -- This is incorrectly named and should be `get?_indexOf`;
 -- this already exists, so will require a deprecation dance.