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

Tactic:
specialize this (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
h✝¹ : ¬start ≤ l.size
h✝ : stop < l.size
h : min start l.size = l.size
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 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 β
start stop : Nat
b : β
i : Nat
w : stop + i ≤ min start l.size
⊢ stop + i ≤ 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
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

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

Tactic:
unfold foldrM

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

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

Tactic:
rw [if_neg (by 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
h✝¹ : ¬start ≤ l.size
h✝ : stop < l.size
h : min start l.size = l.size
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 l.size ⋯ b = foldrM.fold f (l.extract stop start) 0 (min start l.size - stop) ⋯ 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
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
⊢ stop ≤ min start 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
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:
induction i generalizing b with
| zero =>
  unfold foldrM.fold
  simp
| succ i ih =>
  unfold foldrM.fold
  simp only [beq_iff_eq, Nat.add_right_eq_self, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
    getElem_extract]
  congr
  funext b
  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
⊢ min start l.size ≤ 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 =
    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 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

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

Tactic:
have h : min start l.size = start := 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
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

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

Tactic:
omega

Result:
no goals