-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) :
    dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x

Proof state:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x : α
⊢ (fun x => dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x) = foldlM n fun x j => f j.succ x

Tactic:
ext

Result:
case succ.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x x✝ : α
⊢ dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x✝ = foldlM n (fun x j => f j.succ x) x✝

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
f : Fin 0 → α → m α
x : α
⊢ dfoldlM 0 (fun x => α) f x = foldlM 0 (fun x i => f i x) x

Tactic:
simp only [dfoldlM_zero, foldlM_zero]

Result:
no goals

Proof state:
case succ.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x x✝ : α
⊢ dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x✝ = foldlM n (fun x j => f j.succ x) x✝

Tactic:
simp only [ih]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝ : Monad m
f : Fin n → α → m α
x : α
⊢ dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x

Tactic:
induction n generalizing x with
| zero => simp only [dfoldlM_zero, foldlM_zero]
| succ n ih =>
  simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def]
  congr; ext; simp only [ih]

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x : α
⊢ (do
      let x ← f 0 x
      dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x) =
    f 0 x >>= foldlM n fun x j => f j.succ x

Tactic:
congr

Result:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x : α
⊢ (fun x => dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x) = foldlM n fun x j => f j.succ x

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x : α
⊢ dfoldlM (n + 1) (fun x => α) f x = foldlM (n + 1) (fun x i => f i x) x

Tactic:
simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldlM n (fun x => α) f x = foldlM n (fun x i => f i x) x
f : Fin (n + 1) → α → m α
x : α
⊢ (do
      let x ← f 0 x
      dfoldlM n (fun x => α) (fun x1 x2 => f x1.succ x2) x) =
    f 0 x >>= foldlM n fun x j => f j.succ x