-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_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.foldlM f b start stop = l'.foldlM g b start' stop'

Proof state:
β : Type u_1
α : Type u_2
start start' stop stop' : Nat
m : Type u_1 → 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'
⊢ foldlM f b l start stop = foldlM g b l' start' stop'

Tactic:
subst hstart hstop w

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

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

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

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

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

Tactic:
congr

Result:
case mk.e_f
β : Type u_1
α : Type u_2
start stop : Nat
m : Type u_1 → 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_1 → Type u_3
inst✝ : Monad m
f g : β → α → m β
b : β
h : ∀ (x : β) (y : α), f x y = g x y
l : List α
⊢ foldlM f b { toList := l } start stop = foldlM g b { toList := l } start stop

Tactic:
rw [foldlM_start_stop, List.extract_toArray]

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

Proof state:
β : Type u_1
α : Type u_2
start stop : Nat
m : Type u_1 → Type u_3
inst✝ : Monad m
f g : β → α → m β
b : β
l : Array α
h : ∀ (x : β) (y : α), f x y = g x y
⊢ foldlM f b l start stop = foldlM 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_1 → Type u_3
inst✝ : Monad m
f g : β → α → m β
b : β
h : ∀ (x : β) (y : α), f x y = g x y
l : List α
⊢ foldlM f b { toList := l } start stop = foldlM g b { toList := l } start stop

Proof state:
case mk.e_f
β : Type u_1
α : Type u_2
start stop : Nat
m : Type u_1 → 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_1 → 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:
case mk
β : Type u_1
α : Type u_2
start stop : Nat
m : Type u_1 → Type u_3
inst✝ : Monad m
f g : β → α → m β
b : β
h : ∀ (x : β) (y : α), f x y = g x y
l : List α
⊢ List.foldlM f b (l.extract start stop) = foldlM g b { toList := l } start stop

Tactic:
rw [foldlM_start_stop, List.extract_toArray]

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

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

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

Result:
case mk
β : Type u_1
α : Type u_2
start stop : Nat
m : Type u_1 → Type u_3
inst✝ : Monad m
f g : β → α → m β
b : β
h : ∀ (x : β) (y : α), f x y = g x y
l : List α
⊢ List.foldlM f b (l.extract start stop) = foldlM 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_1 → 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