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

Tactic:
simp

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
⊢ foldlM f b l start stop = foldlM f b (l.extract start stop)

Tactic:
unfold foldlM

Result:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
⊢ (let fold := fun stop h => foldlM.loop f l stop h (stop - start) start b;
    if h : stop ≤ l.size then fold stop h else fold l.size ⋯) =
    let fold := fun stop_1 h => foldlM.loop f (l.extract start stop) stop_1 h (stop_1 - 0) 0 b;
    if h : (l.extract start stop).size ≤ (l.extract start stop).size then fold (l.extract start stop).size h
    else fold (l.extract start stop).size ⋯

Proof state:
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

Tactic:
funext b

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
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 : β
⊢ 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:
α : 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 = stop

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : 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 stop ⋯ (stop - 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 = stop := by omega

Result:
case isTrue
α : 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 = stop
⊢ foldlM.loop f l stop ⋯ (stop - 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.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
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 : β
⊢ 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:
specialize ih b (k + 1) (by omega)

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

Tactic:
suffices ∀ (b : β) (i k) (w : i + k = min stop l.size - start),
  foldlM.loop f l (min stop l.size) (by omega) i (start + k) b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) (by simp) i k b by
  intro b
  simpa using this b (min stop l.size - start) 0 (by omega)

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),
    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

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

Tactic:
simp_all

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 ≤ 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 β
b : β
start stop : Nat
⊢ (let fold := fun stop h => foldlM.loop f l stop h (stop - start) start b;
    if h : stop ≤ l.size then fold stop h else fold l.size ⋯) =
    let fold := fun stop_1 h => foldlM.loop f (l.extract start stop) stop_1 h (stop_1 - 0) 0 b;
    if h : (l.extract start stop).size ≤ (l.extract start stop).size then fold (l.extract start stop).size h
    else fold (l.extract start stop).size ⋯

Tactic:
simp only [Nat.sub_zero, size_extract, Nat.le_refl, ↓reduceDIte]

Result:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
⊢ (if h : stop ≤ l.size then foldlM.loop f l stop ⋯ (stop - start) start b
    else 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