α : Type u_1
β : Type u_2
f : α → β
arr : Array α
i : Nat
h : i < size (map f arr)
this :
  (∀ (i : Fin (size arr)), SatisfiesM (fun b => b = f arr[i]) (f arr[i])) →
    SatisfiesM (fun arr_1 => ∃ eq, ∀ (i : Nat) (h : i < size arr), arr_1[i] = f arr[{ val := i, isLt := h }])
      (mapM f arr)
⊢ (map f arr)[i] = f arr[i]
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
i : Nat
h : i < size (map f arr)
⊢ (map f arr)[i] = f arr[i]
have := SatisfiesM_mapM' (m := Id) arr f (fun i b => b = f (arr[i]))
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
i : Nat
h : i < size (map f arr)
this : ∃ eq, ∀ (i : Nat) (h : i < size arr), (mapM f arr)[i] = f arr[{ val := i, isLt := h }]
⊢ (map f arr)[i] = f arr[i]
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
i : Nat
h : i < size (map f arr)
this :
  (∀ (i : Fin (size arr)), SatisfiesM (fun b => b = f arr[i]) (f arr[i])) →
    SatisfiesM (fun arr_1 => ∃ eq, ∀ (i : Nat) (h : i < size arr), arr_1[i] = f arr[{ val := i, isLt := h }])
      (mapM f arr)
⊢ (map f arr)[i] = f arr[i]
simp [SatisfiesM_Id_eq] at this
no goals
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
i : Nat
h : i < size (map f arr)
this : ∃ eq, ∀ (i : Nat) (h : i < size arr), (mapM f arr)[i] = f arr[{ val := i, isLt := h }]
⊢ (map f arr)[i] = f arr[i]
exact this.2 i (size_map .. ▸ h)