-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_congr {m} [Monad m] {f g : α → β → m β} {b : β} {l l' : Array α}
    (w : l = l')
    (h : ∀ x y, f x y = g x y) (hstart : start = start') (hstop : stop = stop') :
    l.foldrM f b start stop = l'.foldrM g b start' stop'

Proof state:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ foldrM f b (l.extract stop start).toArray = foldrM g b { toList := l } start stop

Tactic:
simp only [size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']

Result:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = foldrM g b { toList := l } start stop

Proof state:
case mk.e_f
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ f = g

Tactic:
funext b a

Result:
case mk.e_f.h.h
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b✝ : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
b : α
a : β
⊢ f b a = g b a

Proof state:
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
l : Array α
h : ∀ (x : α) (y : β), f x y = g x y
⊢ foldrM f b l start stop = foldrM g b l start stop

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ foldrM f b { toList := l } start stop = foldrM g b { toList := l } start stop

Proof state:
case mk.e_f.h.h
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b✝ : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
b : α
a : β
⊢ f b a = g b a

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = foldrM g b { toList := l } start stop

Tactic:
rw [foldrM_start_stop, List.extract_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = foldrM g b (l.extract stop start).toArray

Proof state:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = List.foldrM g b (l.extract stop start)

Tactic:
congr

Result:
case mk.e_f
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ f = g

Proof state:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = foldrM g b (l.extract stop start).toArray

Tactic:
simp only [size_toArray, List.length_take, List.length_drop, List.foldrM_toArray']

Result:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ List.foldrM f b (l.extract stop start) = List.foldrM g b (l.extract stop start)

Proof state:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ foldrM f b { toList := l } start stop = foldrM g b { toList := l } start stop

Tactic:
rw [foldrM_start_stop, List.extract_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
h : ∀ (x : α) (y : β), f x y = g x y
l : List α
⊢ foldrM f b (l.extract stop start).toArray = foldrM g b { toList := l } start stop

Proof state:
α : Type u_1
β : Type u_2
start start' stop stop' : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
l l' : Array α
w : l = l'
h : ∀ (x : α) (y : β), f x y = g x y
hstart : start = start'
hstop : stop = stop'
⊢ foldrM f b l start stop = foldrM g b l' start' stop'

Tactic:
subst hstart hstop w

Result:
α : Type u_1
β : Type u_2
start stop : Nat
m : Type u_2 → Type u_3
inst✝ : Monad m
f g : α → β → m β
b : β
l : Array α
h : ∀ (x : α) (y : β), f x y = g x y
⊢ foldrM f b l start stop = foldrM g b l start stop