-- 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:
intro b

Result:
α : 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

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
⊢ (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

Tactic:
simp only [getElem_extract]

Result:
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

Proof state:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this :
  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
h✝ : ¬stop ≤ l.size
⊢ min stop l.size = l.size

Tactic:
omega

Result:
no goals

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
⊢ foldlM.loop f l (min stop l.size) ⋯ (i + 1) (start + k) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (i + 1) k b

Tactic:
unfold foldlM.loop

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
⊢ (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

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✝ 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

Tactic:
simp at h

Result:
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 = i'✝
⊢ (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

Proof state:
case isFalse
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this :
  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
h✝ : ¬stop ≤ l.size
⊢ foldlM.loop f l l.size ⋯ (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:
have : min stop l.size = l.size := by omega

Result:
case isFalse
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this✝ :
  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
h✝ : ¬stop ≤ l.size
this : min stop l.size = l.size
⊢ foldlM.loop f l l.size ⋯ (l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 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
⊢ ∀ (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

Tactic:
intro b i k w

Result:
α : 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
⊢ 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