-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_start_stop {m} [Monad m] (l : Array α) (f : α → β → m β) (b) (start stop : Nat) :
    l.foldrM f b start stop = (l.extract stop start).foldrM f 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
⊢ (if h : start ≤ l.size then if stop < start then foldrM.fold f l stop start h b else pure b
    else if stop < l.size then foldrM.fold f l stop l.size ⋯ b else pure b) =
    if h : (l.extract stop start).size ≤ (l.extract stop start).size then
      if 0 < (l.extract stop start).size then foldrM.fold f (l.extract stop start) 0 (l.extract stop start).size h b
      else pure b
    else
      if 0 < (l.extract stop start).size then foldrM.fold f (l.extract stop start) 0 (l.extract stop start).size ⋯ b
      else pure b

Tactic:
simp only [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 : start ≤ l.size then if stop < start then foldrM.fold f l stop start h b else pure b
    else if stop < l.size then foldrM.fold f l stop l.size ⋯ b else pure b) =
    if 0 < min start l.size - stop then foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b else pure b

Proof state:
case succ.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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b✝ : β
w : stop + (i + 1) ≤ min start l.size
b : β
⊢ foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b

Tactic:
simp [ih b (by 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
⊢ stop ≤ min start l.size →
    foldrM.fold f l stop (min start l.size) ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ 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 : β),
    stop ≤ min start l.size →
      foldrM.fold f l stop (min start l.size) ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b

Proof state:
case isTrue.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
h✝¹ : start ≤ l.size
h✝ : stop < start
h : min start l.size = start
this :
  foldrM.fold f l stop (min start l.size) ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b
⊢ foldrM.fold f l stop start h✝¹ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (fun __do_lift => foldrM.fold f l stop (stop + i) ⋯ __do_lift) = fun __do_lift =>
    foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift

Tactic:
funext b

Result:
case succ.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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b✝ : β
w : stop + (i + 1) ≤ min start l.size
b : β
⊢ foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ 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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (do
      let __do_lift ← f l[stop + i] b
      foldrM.fold f l stop (stop + i) ⋯ __do_lift) =
    do
    let __do_lift ← f l[stop + i] b
    foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift

Tactic:
congr

Result:
case succ.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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (fun __do_lift => foldrM.fold f l stop (stop + i) ⋯ __do_lift) = fun __do_lift =>
    foldrM.fold f (l.extract stop start) 0 i ⋯ __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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ foldrM.fold f l stop (stop + (i + 1)) ⋯ b = foldrM.fold f (l.extract stop start) 0 (i + 1) ⋯ b

Tactic:
unfold foldrM.fold

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 : β) (w : stop + i ≤ min start l.size),
    foldrM.fold f l stop (stop + i) ⋯ b = foldrM.fold f (l.extract stop start) 0 i ⋯ b
b : β
w : stop + (i + 1) ≤ min start l.size
⊢ (if (stop + (i + 1) == stop) = true then pure b
    else
      match stop + (i + 1), ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f l[i] b
        foldrM.fold f l stop i ⋯ __do_lift) =
    if (i + 1 == 0) = true then pure b
    else
      match i + 1, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f (l.extract stop start)[i] b
        foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift

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

Tactic:
simp

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 : Nat
w : stop + i ≤ min start l.size
⊢ i ≤ min start l.size - stop

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 :
  stop ≤ min start l.size →
    foldrM.fold f l stop (min start l.size) ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b
h✝¹ : start ≤ l.size
h✝ : stop < start
⊢ 0 < min start l.size - stop

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 : β
w : stop + 0 ≤ min start l.size
⊢ (if (stop + 0 == stop) = true then pure b
    else
      match stop + 0, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f l[i] b
        foldrM.fold f l stop i ⋯ __do_lift) =
    if (0 == 0) = true then pure b
    else
      match 0, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f (l.extract stop start)[i] b
        foldrM.fold f (l.extract stop start) 0 i ⋯ __do_lift

Tactic:
simp

Result:
no goals