mapIdx

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

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

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

@[simp]

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

@[simp]

theorem Array.size_zipWithIndex {α : Type u_1} (as : Array α) : as.zipWithIndex.size = as.size

@[simp]

theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin a.size → α → β) (i : Nat) (h : i < (a.mapIdx f).size) : (a.mapIdx f)[i] = f ⟨i, ⋯⟩ a[i]

@[simp]

theorem Array.getElem?_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin a.size → α → β) (i : Nat) : (a.mapIdx f)[i]? = a[i]?.pbind fun (b : α) (h : b ∈ a[i]?) => some (f ⟨i, ⋯⟩ b)