-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_start_stop {m} [Monad m] (l : Array α) (f : β → α → m β) (b) (start stop : Nat) :
    l.foldlM f b start stop = (l.extract start stop).foldlM f b

Proof state:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop : Nat
this :
  ∀ (b : β) (i k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
⊢ foldlM.loop f l (min stop l.size) ⋯ (min stop l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b

Tactic:
simpa using this b (min stop l.size - start) 0 (by omega)

Result:
no goals

Proof state:
case succ.h_2.e_a.h
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
b✝ : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
b : β
ih :
  foldlM.loop f l (min stop l.size) ⋯ i (start + (k + 1)) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b
⊢ foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b

Tactic:
simp [← Nat.add_assoc] at ih

Result:
case succ.h_2.e_a.h
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
b✝ : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
b : β
ih :
  foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b
⊢ foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b

Proof state:
case succ
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
⊢ (if hlt : start + k < min stop l.size then
      match i + 1 with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b l[start + k]
        foldlM.loop f l (min stop l.size) ⋯ i' (start + k + 1) __do_lift
    else pure b) =
    if hlt : k < min stop l.size - start then
      match i + 1 with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b (l.extract start stop)[k]
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i' (k + 1) __do_lift
    else pure b

Tactic:
rw [dif_pos (by omega), dif_pos (by omega)]

Result:
case succ
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
⊢ (match i + 1 with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b l[start + k]
      foldlM.loop f l (min stop l.size) ⋯ i' (start + k + 1) __do_lift) =
    match i + 1 with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b (l.extract start stop)[k]
      foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i' (k + 1) __do_lift

Proof state:
case succ.h_2.e_a.h
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
b✝ : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
b : β
ih :
  foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b
⊢ foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) b

Tactic:
rw [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop : Nat
b : β
i k : Nat
w : i + k = min stop l.size - start
⊢ min stop l.size ≤ l.size

Tactic:
omega

Result:
no goals

Proof state:
case succ.h_2
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
⊢ (do
      let __do_lift ← f b l[start + k]
      foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) __do_lift) =
    do
    let __do_lift ← f b l[start + k]
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) __do_lift

Tactic:
congr

Result:
case succ.h_2.e_a
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
⊢ (fun __do_lift => foldlM.loop f l (min stop l.size) ⋯ i (start + k + 1) __do_lift) = fun __do_lift =>
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i (k + 1) __do_lift

Proof state:
case succ
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
⊢ (match i + 1 with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b l[start + k]
      foldlM.loop f l (min stop l.size) ⋯ i' (start + k + 1) __do_lift) =
    match i + 1 with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b (l.extract start stop)[k]
      foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i' (k + 1) __do_lift

Tactic:
split <;> rename_i h

Result:
case succ.h_1
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ : Nat
h : i + 1 = 0
⊢ pure b = pure b

case succ.h_2
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop i : Nat
ih :
  ∀ (b : β) (k : Nat),
    i + k = min stop l.size - start →
      foldlM.loop f l (min stop l.size) ⋯ i (start + k) b =
        foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i k b
b : β
k : Nat
w : i + 1 + k = min stop l.size - start
i✝ i'✝ : Nat
h : i + 1 = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b l[start + k]
    foldlM.loop f l (min stop l.size) ⋯ i'✝ (start + k + 1) __do_lift) =
    let_fun this := ⋯;
    do
    let __do_lift ← f b (l.extract start stop)[k]
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ i'✝ (k + 1) __do_lift