m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
⊢ (if hlt : j < size arr then
      match i with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : j < size arr);
        do
        let __do_lift ← f b arr[j]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop j arr.data)
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
unfold foldlM.loop
case inl
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : j < size arr
⊢ (match i with
    | 0 => pure b
    | Nat.succ i' =>
      let_fun this := (_ : j < size arr);
      do
      let __do_lift ← f b arr[j]
      foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)

case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b (List.drop j arr.data)
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
⊢ (if hlt : j < size arr then
      match i with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : j < size arr);
        do
        let __do_lift ← f b arr[j]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop j arr.data)
split
case inl.h_1
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ : Nat
H : size arr ≤ 0 + j
⊢ pure b = List.foldlM f b (List.drop j arr.data)

case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i'✝ : Nat
H : size arr ≤ Nat.succ i'✝ + j
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i'✝ (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)

case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b (List.drop j arr.data)
case inl
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : j < size arr
⊢ (match i with
    | 0 => pure b
    | Nat.succ i' =>
      let_fun this := (_ : j < size arr);
      do
      let __do_lift ← f b arr[j]
      foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)

case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b (List.drop j arr.data)
split
no goals
case inl.h_1
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ : Nat
H : size arr ≤ 0 + j
⊢ pure b = List.foldlM f b (List.drop j arr.data)
cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ i + j
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i'✝ : Nat
H : size arr ≤ Nat.succ i'✝ + j
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i'✝ (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)
rename_i i
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ (i + j)
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ i + j
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)
rw [Nat.succ_add] at H
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ (i + j)
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.data)) =
    List.foldlM f b (List.drop j arr.data)
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ (i + j)
⊢ (let_fun this := (_ : j < size arr);
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.data)
simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
no goals
case inl.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
h✝ : j < size arr
i✝ i : Nat
H : size arr ≤ Nat.succ (i + j)
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.data)) =
    List.foldlM f b (List.drop j arr.data)
conv => rhs; rw [← List.get_drop_eq_drop _ _ ‹_›]
case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b []
case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b (List.drop j arr.data)
rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]
no goals
case inr
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr ≤ i + j
b : β
h✝ : ¬j < size arr
⊢ pure b = List.foldlM f b []
rfl