cleanup

src/Init/Data/Array/Basic.lean

@@ -455,7 +455,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
-    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+    (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
@@ -464,12 +464,12 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
+      map i (j+1) this (bs.push (← f j (as.get j j_lt) j_lt))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
-  as.mapFinIdxM fun i a => f i a
+  as.mapFinIdxM fun i a _ => f i a
 
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
@@ -588,7 +588,7 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :
 
 /-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
   Id.run <| as.mapFinIdxM f
 
 @[inline]

src/Init/Data/Array/MapIdx.lean

@@ -12,81 +12,82 @@ namespace Array
 /-! ### mapFinIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
+theorem mapFinIdx_induction (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    (p : (i : Nat) → β → (h : i < as.size) → Prop)
+    (hs : ∀ i h, motive i → p i (f i as[i] h) h ∧ motive (i + 1)) :
     motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+      ∀ i h, p i ((Array.mapFinIdx as f)[i]) h := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
     let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
       exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
     | succ i ih =>
-      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      apply @ih (bs.push (f j as[j] (by omega))) (j + 1) (by omega) (by simp; omega)
       · intro i i_lt h'
         rw [getElem_push]
         split
         · apply h₂
         · simp only [size_push] at h'
           obtain rfl : i = j := by omega
-          apply (hs ⟨i, by omega⟩ hm).1
-      · exact (hs ⟨j, by omega⟩ hm).2
+          apply (hs i (by omega) hm).1
+      · exact (hs j (by omega) hm).2
   simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
 
-theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+theorem mapFinIdx_spec (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β)
+    (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i] h) h) :
     ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
-  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+      ∀ i h, p i ((Array.mapFinIdx as f)[i]) h :=
+  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2
 
-@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
-  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+@[simp] theorem size_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) :
+    (a.mapFinIdx f).size = a.size :=
+  (mapFinIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
 
 @[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
   Array.size_mapFinIdx _ _
 
-@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+@[simp] theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat)
     (h : i < (mapFinIdx a f).size) :
-    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+    (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all))  (by simp_all) :=
+  (mapFinIdx_spec _ _ (fun i b h => b = f i a[i] h) fun _ _ => rfl).2 i _
 
-@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat) :
     (a.mapFinIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+      a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
-@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size → α → β) :
-    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f ⟨i, by simp⟩ a) := by
+@[simp] theorem toList_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) :
+    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
   apply List.ext_getElem <;> simp
 
 /-! ### mapIdx -/
 
 theorem mapIdx_induction (f : Nat → α → β) (as : Array α)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    (p : (i : Nat) → β → (h : i < as.size) → Prop)
+    (hs : ∀ i h, motive i → p i (f i as[i]) h ∧ motive (i + 1)) :
     motive as.size ∧ ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
-  mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
+      ∀ i h, p i ((as.mapIdx f)[i]) h :=
+  mapFinIdx_induction as (fun i a _ => f i a) motive h0 p hs
 
 theorem mapIdx_spec (f : Nat → α → β) (as : Array α)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i]) h) :
     ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
-  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+      ∀ i h, p i ((as.mapIdx f)[i]) h :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2
 
 @[simp] theorem size_mapIdx (f : Nat → α → β) (as : Array α) : (as.mapIdx f).size = as.size :=
-  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+  (mapIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
 
 @[simp] theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat)
     (h : i < (as.mapIdx f).size) :
     (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i as[i]) fun _ => rfl).2 i (by simp_all)
+  (mapIdx_spec _ _ (fun i b h => b = f i as[i]) fun _ _ => rfl).2 i (by simp_all)
 
 @[simp] theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) :
     (as.mapIdx f)[i]? =
@@ -101,7 +102,7 @@ end Array
 
 namespace List
 
-@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length → α → β) :
+@[simp] theorem mapFinIdx_toArray (l : List α) (f : (i : Nat) → α → (h : i < l.length) → β) :
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 

src/Init/Data/List/MapIdx.lean

@@ -22,13 +22,13 @@ namespace List
 Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list
 `[f 0 a₀, f 1 a₁, ...]`.
 -/
-@[inline] def mapFinIdx (as : List α) (f : Fin as.length → α → β) : List β := go as #[] (by simp) where
+@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β := go as #[] (by simp) where
   /-- Auxiliary for `mapFinIdx`:
   `mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/
   @[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
   | [], acc, h => acc.toList
   | a :: as, acc, h =>
-    go as (acc.push (f ⟨acc.size, by simp at h; omega⟩ a)) (by simp at h ⊢; omega)
+    go as (acc.push (f acc.size a (by simp at h; omega))) (by simp at h ⊢; omega)
 
 /--
 Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list
@@ -44,7 +44,7 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁,
 /-! ### mapFinIdx -/
 
 @[simp]
-theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] :=
+theorem mapFinIdx_nil {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx [] f = [] :=
   rfl
 
 @[simp] theorem length_mapFinIdx_go :
@@ -53,13 +53,16 @@ theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] :=
   | nil => simpa using h
   | cons _ _ ih => simp [mapFinIdx.go, ih]
 
-@[simp] theorem length_mapFinIdx {as : List α} {f : Fin as.length → α → β} :
+@[simp] theorem length_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
     (as.mapFinIdx f).length = as.length := by
   simp [mapFinIdx, length_mapFinIdx_go]
 
-theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} {w} :
+theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} :
     (mapFinIdx.go as f bs acc h)[i] =
-      if w' : i < acc.size then acc[i] else f ⟨i, by simp at w; omega⟩ (bs[i - acc.size]'(by simp at w; omega)) := by
+      if w' : i < acc.size then
+        acc[i]
+      else
+        f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega) := by
   induction bs generalizing acc with
   | nil =>
     simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h
@@ -78,29 +81,30 @@ theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i
     · have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega
       simp [h₃]
 
-@[simp] theorem getElem_mapFinIdx {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} :
-    (as.mapFinIdx f)[i] = f ⟨i, by simp at h; omega⟩ (as[i]'(by simp at h; omega)) := by
+@[simp] theorem getElem_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} :
+    (as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega) := by
   simp [mapFinIdx, getElem_mapFinIdx_go]
 
-theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} :
-    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] := by
+theorem mapFinIdx_eq_ofFn {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
+    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] i.2 := by
   apply ext_getElem <;> simp
 
-@[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} :
-    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some_iff] at m; exact m.1⟩ x := by
+@[simp] theorem getElem?_mapFinIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} :
+    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1) := by
   simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]
   split <;> simp
 
 @[simp]
-theorem mapFinIdx_cons {l : List α} {a : α} {f : Fin (l.length + 1) → α → β} :
-    mapFinIdx (a :: l) f = f 0 a :: mapFinIdx l (fun i => f i.succ) := by
+theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} :
+    mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega)) := by
   apply ext_getElem
   · simp
   · rintro (_|i) h₁ h₂ <;> simp
 
-theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β} :
+theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} :
     (K ++ L).mapFinIdx f =
-      K.mapFinIdx (fun i => f (i.castLE (by simp))) ++ L.mapFinIdx (fun i => f ((i.natAdd K.length).cast (by simp))) := by
+      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
+        L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega)) := by
   apply ext_getElem
   · simp
   · intro i h₁ h₂
@@ -108,60 +112,57 @@ theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β}
     simp only [getElem_mapFinIdx, length_mapFinIdx]
     split <;> rename_i h
     · rw [getElem_append_left]
-      congr
     · simp only [Nat.not_lt] at h
       rw [getElem_append_right h]
       congr
-      simp
       omega
 
-@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : Fin (l ++ [e]).length → α → β}:
-    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i => f (i.castLE (by simp))) ++ [f ⟨l.length, by simp⟩ e] := by
+@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β}:
+    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)] := by
   simp [mapFinIdx_append]
-  congr
 
-theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} :
-    [a].mapFinIdx f = [f ⟨0, by simp⟩ a] := by
+theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
+    [a].mapFinIdx f = [f 0 a (by simp)] := by
   simp
 
-theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} :
+theorem mapFinIdx_eq_enum_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = l.enum.attach.map
       fun ⟨⟨i, x⟩, m⟩ =>
-        f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1⟩ x := by
+        f i x (by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   apply ext_getElem <;> simp
 
 @[simp]
-theorem mapFinIdx_eq_nil_iff {l : List α} {f : Fin l.length → α → β} :
+theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = [] ↔ l = [] := by
   rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
 
-theorem mapFinIdx_ne_nil_iff {l : List α} {f : Fin l.length → α → β} :
+theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
   simp
 
-theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β}
-    (h : b ∈ l.mapFinIdx f) : ∃ (i : Fin l.length), f i l[i] = b := by
+theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
+    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
   rw [mapFinIdx_eq_enum_map] at h
   replace h := exists_of_mem_map h
   simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h
   obtain ⟨i, b, h, rfl⟩ := h
   rw [getElem?_eq_some_iff] at h
   obtain ⟨h', rfl⟩ := h
-  exact ⟨⟨i, h'⟩, rfl⟩
+  exact ⟨i, h', rfl⟩
 
-@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β} :
-    b ∈ l.mapFinIdx f ↔ ∃ (i : Fin l.length), f i l[i] = b := by
+@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
   constructor
   · intro h
     exact exists_of_mem_mapFinIdx h
   · rintro ⟨i, h, rfl⟩
     rw [mem_iff_getElem]
-    exact ⟨i, by simp⟩
+    exact ⟨i, by simpa using h, by simp⟩
 
-theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α → β} :
+theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = b :: l₂ ↔
-      ∃ (a : α) (l₁ : List α) (h : l = a :: l₁),
-        f ⟨0, by simp [h]⟩ a = b ∧ l₁.mapFinIdx (fun i => f (i.succ.cast (by simp [h]))) = l₂ := by
+      ∃ (a : α) (l₁ : List α) (w : l = a :: l₁),
+        f 0 a (by simp [w]) = b ∧ l₁.mapFinIdx (fun i a h => f (i + 1) a (by simp [w]; omega)) = l₂ := by
   cases l with
   | nil => simp
   | cons x l' =>
@@ -169,39 +170,48 @@ theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α
       exists_and_left]
     constructor
     · rintro ⟨rfl, rfl⟩
-      refine ⟨x, rfl, l', by simp⟩
-    · rintro ⟨a, ⟨rfl, h⟩, ⟨_, ⟨rfl, rfl⟩, h⟩⟩
-      exact ⟨rfl, h⟩
+      refine ⟨x, l', ⟨rfl, rfl⟩, by simp⟩
+    · rintro ⟨a, l', ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
+      exact ⟨rfl, by simp⟩
 
-theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : Fin l.length → α → β} :
+theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = b :: l₂ ↔
-      l.head?.pbind (fun x m => (f ⟨0, by cases l <;> simp_all⟩ x)) = some b ∧
-        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i => f (i.succ.cast (by cases l <;> simp_all))) = some l₂ := by
+      l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧
+        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂ := by
   cases l <;> simp
 
-theorem mapFinIdx_eq_iff {l : List α} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f ⟨i, h⟩ l[i] := by
+theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h := by
   constructor
   · rintro rfl
     simp
   · rintro ⟨h, w⟩
     apply ext_getElem <;> simp_all
 
-theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : Fin l.length → α → β} :
-    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Fin l.length), f i l[i] = g i l[i] := by
+theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
+    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h := by
   rw [eq_comm, mapFinIdx_eq_iff]
   simp [Fin.forall_iff]
 
-@[simp] theorem mapFinIdx_mapFinIdx {l : List α} {f : Fin l.length → α → β} {g : Fin _ → β → γ} :
-    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i => g (i.cast (by simp)) ∘ f i) := by
+@[simp] theorem mapFinIdx_mapFinIdx {l : List α}
+    {f : (i : Nat) → α → (h : i < l.length) → β}
+    {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).length) → γ} :
+    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa)) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_replicate_iff {l : List α} {f : Fin l.length → α → β} {b : β} :
-    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Fin l.length), f i l[i] = b := by
-  simp [eq_replicate_iff, length_mapFinIdx, mem_mapFinIdx, forall_exists_index, true_and]
+theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
+    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b := by
+  rw [eq_replicate_iff, length_mapFinIdx]
+  simp only [mem_mapFinIdx, forall_exists_index, true_and]
+  constructor
+  · intro w i h
+    exact w (f i l[i] h) i h rfl
+  · rintro w b i h rfl
+    exact w i h
 
-@[simp] theorem mapFinIdx_reverse {l : List α} {f : Fin l.reverse.length → α → β} :
-    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i => f ⟨l.length - 1 - i, by simp; omega⟩)).reverse := by
+@[simp] theorem mapFinIdx_reverse {l : List α} {f : (i : Nat) → α → (h : i < l.reverse.length) → β} :
+    l.reverse.mapFinIdx f =
+      (l.mapFinIdx (fun i a h => f (l.length - 1 - i) a (by simp; omega))).reverse := by
   simp [mapFinIdx_eq_iff]
   intro i h
   congr
@@ -262,13 +272,13 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
   rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
   simp
 
-@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : Fin l.length → α → β} {g : Nat → α → β}
-    (h : ∀ (i : Fin l.length), f i l[i] = g i l[i]) :
+@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : Nat → α → β}
+    (h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) :
     l.mapFinIdx f = l.mapIdx g := by
   simp_all [mapFinIdx_eq_iff]
 
 theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
-    l.mapIdx f = l.mapFinIdx (fun i => f i) := by
+    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
 theorem mapIdx_eq_enum_map {l : List α} :

src/Lean/Meta/IndPredBelow.lean

@@ -296,7 +296,7 @@ where
     m.apply recursor
 
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
-    let mss ← ms.toArray.mapIdxM fun _ m => do
+    let mss ← ms.toArray.mapM fun m => do
       let m ← introNPRec m
       (← m.getType).withApp fun below args =>
       m.withContext do