mapFinIdx

theorem Array.mapFinIdx_induction {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (i : Nat) → α → i < xs.size → β) (motive : Nat → Prop) (h0 : motive 0) (p : (i : Nat) → β → i < xs.size → Prop) (hs : ∀ (i : Nat) (h : i < xs.size), motive i → p i (f i xs[i] h) h ∧ motive (i + 1)) : motive xs.size ∧ ∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h

theorem Array.mapFinIdx_induction.go {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (i : Nat) → α → i < xs.size → β) (motive : Nat → Prop) (p : (i : Nat) → β → i < xs.size → Prop) (hs : ∀ (i : Nat) (h : i < xs.size), motive i → p i (f i xs[i] h) h ∧ motive (i + 1)) {bs : Array β} {i j : Nat} {h : i + j = xs.size} (h₁ : j = bs.size) (h₂ : ∀ (i : Nat) (h : i < xs.size) (h' : i < bs.size), p i bs[i] h) (hm : motive j) : let as := mapFinIdxM.map xs f i j h bs; motive xs.size ∧ ∃ (eq : as.size = xs.size), ∀ (i_1 : Nat) (h_1 : i_1 < xs.size), p i_1 as[i_1] h_1

theorem Array.mapFinIdx_spec {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), p i (f i xs[i] h) h) : ∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h

@[simp]

theorem Array.size_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : (xs.mapFinIdx f).size = xs.size

@[simp]

theorem Array.size_zipIdx {α : Type u_1} {xs : Array α} {k : Nat} : (xs.zipIdx k).size = xs.size

@[reducible, inline, deprecated Array.size_zipIdx (since := "2025-01-21")]

abbrev Array.size_zipWithIndex {α : Type u_1} {xs : Array α} {k : Nat} : (xs.zipIdx k).size = xs.size

Equations

• @Array.size_zipWithIndex = @Array.size_zipIdx

@[simp]

theorem Array.getElem_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {i : Nat} (h : i < (xs.mapFinIdx f).size) : (xs.mapFinIdx f)[i] = f i xs[i] ⋯

@[simp]

theorem Array.getElem?_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {i : Nat} : (xs.mapFinIdx f)[i]? = xs[i]?.pbind fun (b : α) (h : b ∈ xs[i]?) => some (f i b ⋯)

@[simp]

theorem Array.toList_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : (xs.mapFinIdx f).toList = xs.toList.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.toList.length) => f i a h

mapIdx

theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {motive : Nat → Prop} (h0 : motive 0) {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), motive i → p i (f i xs[i]) h ∧ motive (i + 1)) : motive xs.size ∧ ∃ (eq : (mapIdx f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (mapIdx f xs)[i] h

theorem Array.mapIdx_spec {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {p : (i : Nat) → β → i < xs.size → Prop} (hs : ∀ (i : Nat) (h : i < xs.size), p i (f i xs[i]) h) : ∃ (eq : (mapIdx f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p i (mapIdx f xs)[i] h

@[simp]

theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} : (mapIdx f xs).size = xs.size

@[simp]

theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {i : Nat} (h : i < (mapIdx f xs).size) : (mapIdx f xs)[i] = f i xs[i]

@[simp]

theorem Array.getElem?_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} {i : Nat} : (mapIdx f xs)[i]? = Option.map (f i) xs[i]?

@[simp]

theorem Array.toList_mapIdx {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {xs : Array α} : (mapIdx f xs).toList = List.mapIdx (fun (i : Nat) (a : α) => f i a) xs.toList

@[simp]

theorem List.mapFinIdx_toArray {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → α → i < l.length → β} : l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray

@[simp]

theorem List.mapIdx_toArray {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {l : List α} : Array.mapIdx f l.toArray = (mapIdx f l).toArray

zipIdx

@[simp]

theorem Array.getElem_zipIdx {α : Type u_1} {xs : Array α} {k i : Nat} (h : i < (xs.zipIdx k).size) : (xs.zipIdx k)[i] = (xs[i], k + i)

@[reducible, inline, deprecated Array.getElem_zipIdx (since := "2025-01-21")]

abbrev Array.getElem_zipWithIndex {α : Type u_1} {xs : Array α} {k i : Nat} (h : i < (xs.zipIdx k).size) : (xs.zipIdx k)[i] = (xs[i], k + i)

Equations

• @Array.getElem_zipWithIndex = @Array.getElem_zipIdx

@[simp]

theorem Array.zipIdx_toArray {α : Type u_1} {l : List α} {k : Nat} : l.toArray.zipIdx k = (l.zipIdx k).toArray

@[reducible, inline, deprecated Array.zipIdx_toArray (since := "2025-01-21")]

abbrev Array.zipWithIndex_toArray {α : Type u_1} {l : List α} {k : Nat} : l.toArray.zipIdx k = (l.zipIdx k).toArray

Equations

• @Array.zipWithIndex_toArray = @Array.zipIdx_toArray

@[simp]

theorem Array.toList_zipIdx {α : Type u_1} {xs : Array α} {k : Nat} : (xs.zipIdx k).toList = xs.toList.zipIdx k

@[reducible, inline, deprecated Array.toList_zipIdx (since := "2025-01-21")]

abbrev Array.toList_zipWithIndex {α : Type u_1} {xs : Array α} {k : Nat} : (xs.zipIdx k).toList = xs.toList.zipIdx k

Equations

• @Array.toList_zipWithIndex = @Array.toList_zipIdx

theorem Array.mk_mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {k i : Nat} {x : α} {xs : Array α} : (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x

theorem Array.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {x : α} {i : Nat} {xs : Array α} : (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x

Variant of mk_mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

theorem Array.mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {x : α × Nat} {xs : Array α} {k : Nat} : x ∈ xs.zipIdx k ↔ k ≤ x.snd ∧ xs[x.snd - k]? = some x.fst

theorem Array.mem_zipIdx_iff_getElem? {α : Type u_1} {x : α × Nat} {xs : Array α} : x ∈ xs.zipIdx ↔ xs[x.snd]? = some x.fst

Variant of mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

@[reducible, inline, deprecated Array.mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]

abbrev Array.mk_mem_zipWithIndex_iff_getElem? {α : Type u_1} {x : α} {i : Nat} {xs : Array α} : (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x

Equations

• @Array.mk_mem_zipWithIndex_iff_getElem? = @Array.mk_mem_zipIdx_iff_getElem?

@[reducible, inline, deprecated Array.mem_zipIdx_iff_getElem? (since := "2025-01-21")]

abbrev Array.mem_zipWithIndex_iff_getElem? {α : Type u_1} {x : α × Nat} {xs : Array α} : x ∈ xs.zipIdx ↔ xs[x.snd]? = some x.fst

Equations

• @Array.mem_zipWithIndex_iff_getElem? = @Array.mem_zipIdx_iff_getElem?

mapFinIdx

theorem Array.mapFinIdx_congr {α : Type u_1} {β : Type u_2} {xs ys : Array α} (w : xs = ys) (f : (i : Nat) → α → i < xs.size → β) : xs.mapFinIdx f = ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.size) => f i a ⋯

@[simp]

theorem Array.mapFinIdx_empty {α : Type u_1} {β : Type u_2} {f : (i : Nat) → α → i < 0 → β} : #[].mapFinIdx f = #[]

theorem Array.mapFinIdx_eq_ofFn {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = ofFn fun (i : Fin xs.size) => f (↑i) xs[i] ⋯

theorem Array.mapFinIdx_append {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : (i : Nat) → α → i < (xs ++ ys).size → β} : (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => f i a ⋯) ++ ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.size) => f (i + xs.size) a ⋯

@[simp]

theorem Array.mapFinIdx_push {α : Type u_1} {β : Type u_2} {xs : Array α} {a : α} {f : (i : Nat) → α → i < (xs.push a).size → β} : (xs.push a).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < xs.size) => f i a_1 ⋯).push (f xs.size a ⋯)

theorem Array.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : (i : Nat) → α → i < 1 → β} : #[a].mapFinIdx f = #[f 0 a ⋯]

theorem Array.mapFinIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = map (fun (x : { x : α × Nat // x ∈ xs.zipIdx }) => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach

@[reducible, inline, deprecated Array.mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]

abbrev Array.mapFinIdx_eq_zipWithIndex_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = map (fun (x : { x : α × Nat // x ∈ xs.zipIdx }) => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach

Equations

• @Array.mapFinIdx_eq_zipWithIndex_map = @Array.mapFinIdx_eq_zipIdx_map

@[simp]

theorem Array.mapFinIdx_eq_empty_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = #[] ↔ xs = #[]

theorem Array.mapFinIdx_ne_empty_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f ≠ #[] ↔ xs ≠ #[]

theorem Array.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} (h : b ∈ xs.mapFinIdx f) : ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] h = b

@[simp]

theorem Array.mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} : b ∈ xs.mapFinIdx f ↔ ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] h = b

theorem Array.mapFinIdx_eq_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {ys : Array β} : xs.mapFinIdx f = ys ↔ ∃ (h : ys.size = xs.size), ∀ (i : Nat) (h_1 : i < xs.size), ys[i] = f i xs[i] h_1

@[simp]

theorem Array.mapFinIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} : xs.mapFinIdx f = #[b] ↔ ∃ (a : α), ∃ (w : xs = #[a]), f 0 a ⋯ = b

theorem Array.mapFinIdx_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {ys zs : Array β} : xs.mapFinIdx f = ys ++ zs ↔ ∃ (ys' : Array α), ∃ (zs' : Array α), ∃ (w : xs = ys' ++ zs'), (ys'.mapFinIdx fun (i : Nat) (a : α) (h : i < ys'.size) => f i a ⋯) = ys ∧ (zs'.mapFinIdx fun (i : Nat) (a : α) (h : i < zs'.size) => f (i + ys'.size) a ⋯) = zs

theorem Array.mapFinIdx_eq_push_iff {α : Type u_1} {β : Type u_2} {ys : Array β} {xs : Array α} {b : β} {f : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = ys.push b ↔ ∃ (zs : Array α), ∃ (a : α), ∃ (w : xs = zs.push a), (zs.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < zs.size) => f i a_1 ⋯) = ys ∧ b = f (xs.size - 1) a ⋯

theorem Array.mapFinIdx_eq_mapFinIdx_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : (i : Nat) → α → i < xs.size → β} : xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = g i xs[i] h

@[simp]

theorem Array.mapFinIdx_mapFinIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {g : (i : Nat) → β → i < (xs.mapFinIdx f).size → γ} : (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => g i (f i a h) ⋯

theorem Array.mapFinIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} : xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b

@[reducible, inline, deprecated Array.mapFinIdx_eq_replicate_iff (since := "2025-03-18")]

abbrev Array.mapFinIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {b : β} : xs.mapFinIdx f = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = b

Equations

• @Array.mapFinIdx_eq_mkArray_iff = @Array.mapFinIdx_eq_replicate_iff

@[simp]

theorem Array.mapFinIdx_reverse {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.reverse.size → β} : xs.reverse.mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => f (xs.size - 1 - i) a ⋯).reverse

mapIdx

@[simp]

theorem Array.mapIdx_empty {α : Type u_1} {β : Type u_2} {f : Nat → α → β} : mapIdx f #[] = #[]

@[simp]

theorem Array.mapFinIdx_eq_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : Nat) → α → i < xs.size → β} {g : Nat → α → β} (h : ∀ (i : Nat) (h : i < xs.size), f i xs[i] h = g i xs[i]) : xs.mapFinIdx f = mapIdx g xs

theorem Array.mapIdx_eq_mapFinIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} : mapIdx f xs = xs.mapFinIdx fun (i : Nat) (a : α) (x : i < xs.size) => f i a

theorem Array.mapIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} : mapIdx f xs = map (fun (x : α × Nat) => match x with | (a, i) => f i a) xs.zipIdx

@[reducible, inline, deprecated Array.mapIdx_eq_zipIdx_map (since := "2025-01-21")]

abbrev Array.mapIdx_eq_zipWithIndex_map {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} : mapIdx f xs = map (fun (x : α × Nat) => match x with | (a, i) => f i a) xs.zipIdx

Equations

• @Array.mapIdx_eq_zipWithIndex_map = @Array.mapIdx_eq_zipIdx_map

theorem Array.mapIdx_append {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs ys : Array α} : mapIdx f (xs ++ ys) = mapIdx f xs ++ mapIdx (fun (i : Nat) => f (i + xs.size)) ys

@[simp]

theorem Array.mapIdx_push {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} {a : α} : mapIdx f (xs.push a) = (mapIdx f xs).push (f xs.size a)

theorem Array.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {a : α} : mapIdx f #[a] = #[f 0 a]

@[simp]

theorem Array.mapIdx_eq_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} : mapIdx f xs = #[] ↔ xs = #[]

theorem Array.mapIdx_ne_empty_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} : mapIdx f xs ≠ #[] ↔ xs ≠ #[]

theorem Array.exists_of_mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Nat → α → β} {b : β} {xs : Array α} (h : b ∈ mapIdx f xs) : ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] = b

@[simp]

theorem Array.mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Nat → α → β} {b : β} {xs : Array α} : b ∈ mapIdx f xs ↔ ∃ (i : Nat), ∃ (h : i < xs.size), f i xs[i] = b

theorem Array.mapIdx_eq_push_iff {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {ys : Array β} {xs : Array α} {b : β} : mapIdx f xs = ys.push b ↔ ∃ (a : α), ∃ (zs : Array α), xs = zs.push a ∧ mapIdx f zs = ys ∧ f zs.size a = b

@[simp]

theorem Array.mapIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} : mapIdx f xs = #[b] ↔ ∃ (a : α), xs = #[a] ∧ f 0 a = b

theorem Array.mapIdx_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {ys zs : Array β} : mapIdx f xs = ys ++ zs ↔ ∃ (xs' : Array α), ∃ (zs' : Array α), xs = xs' ++ zs' ∧ mapIdx f xs' = ys ∧ mapIdx (fun (i : Nat) => f (i + xs'.size)) zs' = zs

theorem Array.mapIdx_eq_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {ys : Array α✝} {xs : Array α} : mapIdx f xs = ys ↔ ∀ (i : Nat), ys[i]? = Option.map (f i) xs[i]?

theorem Array.mapIdx_eq_mapIdx_iff {α : Type u_1} {α✝ : Type u_2} {f g : Nat → α → α✝} {xs : Array α} : mapIdx f xs = mapIdx g xs ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = g i xs[i]

@[simp]

theorem Array.mapIdx_set {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} : mapIdx f (xs.set i a h) = (mapIdx f xs).set i (f i a) ⋯

@[simp]

theorem Array.mapIdx_setIfInBounds {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {xs : Array α} {i : Nat} {a : α} : mapIdx f (xs.setIfInBounds i a) = (mapIdx f xs).setIfInBounds i (f i a)

@[simp]

theorem Array.back?_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} : (mapIdx f xs).back? = Option.map (f (xs.size - 1)) xs.back?

@[simp]

theorem Array.back_mapIdx {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} (h : 0 < (mapIdx f xs).size) : (mapIdx f xs).back h = f (xs.size - 1) (xs.back ⋯)

@[simp]

theorem Array.mapIdx_mapIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : Nat → α → β} {g : Nat → β → γ} : mapIdx g (mapIdx f xs) = mapIdx (fun (i : Nat) => g i ∘ f i) xs

theorem Array.mapIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} : mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b

@[reducible, inline, deprecated Array.mapIdx_eq_replicate_iff (since := "2025-03-18")]

abbrev Array.mapIdx_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} {b : β} : mapIdx f xs = replicate xs.size b ↔ ∀ (i : Nat) (h : i < xs.size), f i xs[i] = b

Equations

• @Array.mapIdx_eq_mkArray_iff = @Array.mapIdx_eq_replicate_iff

@[simp]

theorem Array.mapIdx_reverse {α : Type u_1} {β : Type u_2} {xs : Array α} {f : Nat → α → β} : mapIdx f xs.reverse = (mapIdx (fun (i : Nat) => f (xs.size - 1 - i)) xs).reverse

theorem List.mapFinIdxM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : (i : Nat) → α → i < l.length → m β} : l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f

theorem List.mapFinIdxM_toArray.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : (i : Nat) → α → i < l.length → m β} (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) : Array.mapFinIdxM.map l.toArray f i acc.size inv acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

theorem List.mapIdxM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : Nat → α → m β} : Array.mapIdxM f l.toArray = toArray <$> mapIdxM f l

theorem List.mapIdxM_toArray.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {l : List α} {f : Nat → α → m β} (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) : mapFinIdxM.go l (fun (i : Nat) (a : α) (h : i < l.length) => f i a) bs acc inv = mapIdxM.go f bs acc

theorem Array.toList_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : (i : Nat) → α → i < xs.size → m β} : toList <$> xs.mapFinIdxM f = xs.toList.mapFinIdxM f

theorem Array.toList_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : Nat → α → m β} : toList <$> mapIdxM f xs = List.mapIdxM f xs.toList