m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : i ≤ size arr
⊢ List.foldlM (fun x y => f y x) init (List.reverse (List.take i arr.data)) =
    if (i == 0) = true then pure init
    else
      match i, h with
      | 0, x => pure init
      | Nat.succ i, h =>
        let_fun this := (_ : i < size arr);
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i (_ : i ≤ size arr) __do_lift
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : i ≤ size arr
⊢ List.foldlM (fun x y => f y x) init (List.reverse (List.take i arr.data)) = foldrM.fold f arr 0 i h init
unfold foldrM.fold
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : 0 ≤ size arr
⊢ List.foldlM (fun x y => f y x) init (List.reverse (List.take 0 arr.data)) =
    if (0 == 0) = true then pure init
    else
      match 0, h with
      | 0, x => pure init
      | Nat.succ i, h =>
        let_fun this := (_ : i < size arr);
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i (_ : i ≤ size arr) __do_lift
simp [List.foldlM, List.take]
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i✝ i : Nat
h : i + 1 ≤ size arr
⊢ List.foldlM (fun x y => f y x) init (List.reverse (List.concat (List.take i arr.data) arr.data[i])) =
    if (i + 1 == 0) = true then pure init
    else
      match i + 1, h with
      | 0, x => pure init
      | Nat.succ i, h =>
        let_fun this := (_ : i < size arr);
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i (_ : i ≤ size arr) __do_lift
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i✝ i : Nat
h : i + 1 ≤ size arr
⊢ List.foldlM (fun x y => f y x) init (List.reverse (List.take (i + 1) arr.data)) =
    if (i + 1 == 0) = true then pure init
    else
      match i + 1, h with
      | 0, x => pure init
      | Nat.succ i, h =>
        let_fun this := (_ : i < size arr);
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i (_ : i ≤ size arr) __do_lift
rw [← List.take_concat_get _ _ h]
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i✝ i : Nat
h : i + 1 ≤ size arr
⊢ (do
      let s' ← f arr.data[i] init
      List.foldrM (fun x y => f x y) s' (List.take i arr.data)) =
    if i + 1 = 0 then pure init
    else do
      let s' ← f arr[i] init
      List.foldrM (fun x y => f x y) s' (List.take i arr.data)
rfl