-- 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 : Nat
b : β
w : stop ≤ min start l.size
this :
  ∀ (w : stop + (min start l.size - stop) ≤ min start l.size),
    foldrM.fold f l stop (stop + (min start l.size - stop)) ⋯ b =
      foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b
⊢ 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:
have h : stop + (min start l.size - stop) = min start l.size := 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 : β
w : stop ≤ min start l.size
this :
  ∀ (w : stop + (min start l.size - stop) ≤ min start l.size),
    foldrM.fold f l stop (stop + (min start l.size - stop)) ⋯ b =
      foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b
h : stop + (min start l.size - 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:
α : 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
⊢ 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 β
start stop : Nat
this :
  ∀ (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
b : β
w : 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:
specialize this b (min start l.size - stop)

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

Tactic:
specialize this (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
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

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 : β
w : stop ≤ min start l.size
this :
  ∀ (w : stop + (min start l.size - stop) ≤ min start l.size),
    foldrM.fold f l stop (stop + (min start l.size - stop)) ⋯ b =
      foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b
⊢ stop + (min start l.size - stop) = min start l.size

Tactic:
omega

Result:
no goals

Proof state:
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 = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ b

Tactic:
have h : min start l.size = l.size := by omega

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
h : min start l.size = l.size
⊢ foldrM.fold f l stop l.size ⋯ 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 β
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
⊢ ¬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
⊢ foldrM.fold f l stop (stop + 0) ⋯ b = foldrM.fold f (l.extract stop start) 0 0 ⋯ b

Tactic:
unfold foldrM.fold

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

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

Tactic:
rw [if_neg (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 β
start stop : Nat
this :
  ∀ (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
⊢ ∀ (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

Tactic:
intro b 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
this :
  ∀ (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
b : β
w : 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