-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldlM_toList.aux [Monad m]
    (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b

Proof state:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.toList)) =
    List.foldlM f b (List.drop j arr.toList)

Tactic:
rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]

Result:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.toList)) =
    List.foldlM f b (arr.toList[j] :: List.drop (j + 1) arr.toList)

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
⊢ foldlM.loop f arr arr.size ⋯ i j b = List.foldlM f b (List.drop j arr.toList)

Tactic:
unfold foldlM.loop

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

Proof state:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.toList)) =
    List.foldlM f b (arr.toList[j] :: List.drop (j + 1) arr.toList)

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue.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 < arr.size
i✝ : Nat
H : arr.size ≤ 0 + j
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

Tactic:
cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)

Result:
no goals

Proof state:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

Tactic:
rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]

Result:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b []

Proof state:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ i.succ + j
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)

Tactic:
rw [Nat.succ_add] at H

Result:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)

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

case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

Tactic:
split

Result:
case isTrue.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 < arr.size
i✝ : Nat
H : arr.size ≤ 0 + j
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

case isTrue.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 < arr.size
i✝ i'✝ : Nat
H : arr.size ≤ i'✝.succ + j
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i'✝ (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)

case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

Proof state:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)

Tactic:
simp [foldlM_toList.aux f arr i (j+1) H]

Result:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ (i + j).succ
⊢ (do
      let __do_lift ← f b arr[j]
      List.foldlM f __do_lift (List.drop (j + 1) arr.toList)) =
    List.foldlM f b (List.drop j arr.toList)

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

Tactic:
split

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

case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b (List.drop j arr.toList)

Proof state:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : arr.size ≤ i + j
b : β
h✝ : ¬j < arr.size
⊢ pure b = List.foldlM f b []

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue.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 < arr.size
i✝ i'✝ : Nat
H : arr.size ≤ i'✝.succ + j
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i'✝ (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)

Tactic:
rename_i i

Result:
case isTrue.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 < arr.size
i✝ i : Nat
H : arr.size ≤ i.succ + j
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b arr[j]
    foldlM.loop f arr arr.size ⋯ i (j + 1) __do_lift) =
    List.foldlM f b (List.drop j arr.toList)