[Merged by Bors] - chore: rename List.indexOf_lt_length to List.indexOf_lt_length_iff

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 -/

Mathlib/Data/List/Basic.lean

@@ -704,10 +704,12 @@ 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⟩
 
+@[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
@@ -799,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.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 +813,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⟩
 

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)

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)
 

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
 

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,

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}

scripts/add_deprecations.sh

@@ -1,4 +1,4 @@
-#! /bin/bash
+#! /usr/bin/env bash
 
  : <<'BASH_MODULE_DOC'