-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) :
    foldrM.loop (n+1) f ⟨i+1, h⟩ x =
      foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : 0 + 1 ≤ n + 1
⊢ f ⟨0, h⟩ x >>= foldrM.loop (n + 1) f ⟨0, ⋯⟩ = f 0 x >>= pure

Tactic:
congr

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
⊢ f ⟨i + 1, h⟩ x >>= foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ =
    f ⟨i, ⋯⟩.succ x >>= fun x => foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0

Tactic:
congr

Result:
case succ.e_a
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
⊢ foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ = fun x => foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0

Proof state:
case succ.e_a
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
⊢ foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ = fun x => foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0

Tactic:
funext

Result:
case succ.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
x✝ : α
⊢ foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ x✝ = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x✝ >>= f 0

Proof state:
case succ.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
x✝ : α
⊢ foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ x✝ = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x✝ >>= f 0

Tactic:
exact ih ..

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : 0 + 1 ≤ n + 1
⊢ f ⟨0, h⟩ x >>= foldrM.loop (n + 1) f ⟨0, ⋯⟩ = f 0 x

Tactic:
conv => rhs; rw [←bind_pure (f 0 x)]

Result:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : 0 + 1 ≤ n + 1
⊢ f ⟨0, h⟩ x >>= foldrM.loop (n + 1) f ⟨0, ⋯⟩ = f 0 x >>= pure

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : 0 + 1 ≤ n + 1
⊢ foldrM.loop (n + 1) f ⟨0 + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨0, ⋯⟩ x >>= f 0

Tactic:
rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]

Result:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : 0 + 1 ≤ n + 1
⊢ f ⟨0, h⟩ x >>= foldrM.loop (n + 1) f ⟨0, ⋯⟩ = f 0 x

Proof state:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
⊢ foldrM.loop (n + 1) f ⟨i + 1 + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i + 1, ⋯⟩ x >>= f 0

Tactic:
rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]

Result:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
i : Nat
ih :
  ∀ (x : α) (h : i + 1 ≤ n + 1), foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0
x : α
h : i + 1 + 1 ≤ n + 1
⊢ f ⟨i + 1, h⟩ x >>= foldrM.loop (n + 1) f ⟨i + 1, ⋯⟩ =
    f ⟨i, ⋯⟩.succ x >>= fun x => foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
i : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m α
x : α
h : i + 1 ≤ n + 1
⊢ foldrM.loop (n + 1) f ⟨i + 1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, ⋯⟩ x >>= f 0

Tactic:
induction i generalizing x with
| zero =>
  rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
  conv => rhs; rw [←bind_pure (f 0 x)]
  congr; funext
| succ i ih =>
  rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
  congr; funext; exact ih ..

Result:
no goals