-- 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 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
⊢ k < min stop l.size - start

Tactic:
omega

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 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
b : β
⊢ i + (k + 1) = min stop l.size - start

Tactic:
omega

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 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
⊢ start + k < min stop l.size

Tactic:
omega

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
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 : β
⊢ min stop l.size - start + 0 = min stop l.size - start

Tactic:
omega

Result:
no goals

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

Tactic:
subst k

Result:
case zero
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
start stop : Nat
b : β
⊢ foldlM.loop f l (min stop l.size) ⋯ 0 (start + (min stop l.size - start)) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ 0 (min stop l.size - start) b

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

Tactic:
simp [foldlM.loop]

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 β
b : β
start stop : Nat
⊢ min stop l.size - start ≤ (l.extract start stop).size

Tactic:
simp

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

Tactic:
subst 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✝ : 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

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

Tactic:
simp only [Nat.zero_add] at w

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

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
⊢ 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:
revert 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
⊢ ∀ (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_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

Tactic:
rfl

Result:
no goals