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

Tactic:
omega

Result:
no goals

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
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
⊢ foldrM.fold f l stop start h✝¹ 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

Tactic:
rw [if_pos (by omega)]

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

Tactic:
intro b i 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 : Nat
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

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 < l.size
h : min start l.size = l.size
⊢ stop ≤ min start l.size

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 :
  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
⊢ (if stop < start then foldrM.fold f l stop start h✝ 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

Tactic:
split

Result:
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
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
⊢ foldrM.fold f l stop start h✝¹ 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

case isTrue.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 :
  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
⊢ 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:
α : 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:
α : 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
⊢ (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

Tactic:
split

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 :
  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
⊢ (if stop < start then foldrM.fold f l stop start h✝ 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

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

Tactic:
omega

Result:
no goals

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

Tactic:
split

Result:
case isFalse.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 :
  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 < l.size
⊢ foldrM.fold f l stop l.size ⋯ 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

case isFalse.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 :
  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 < l.size
⊢ 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