-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) :
    foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i)

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
⊢ foldlM.loop (n + 1) f x i = do
    let x ← f x ⟨i, h⟩
    foldlM.loop n (fun x j => f x j.succ) x i

Tactic:
if h' : i < n then
  rw [foldlM_loop_lt _ _ h]
  congr; funext
  rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
else
  cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
  rw [foldlM_loop_lt]
  congr; funext
  rw [foldlM_loop_eq, foldlM_loop_eq]

Result:
no goals

Proof state:
case refl
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ (do
      let x ← f x ⟨n, ?refl.h⟩
      foldlM.loop (n + 1) f x (n + 1)) =
    do
    let x ← f x ⟨n, h⟩
    foldlM.loop n (fun x j => f x j.succ) x n

case refl.h
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ n < n + 1

Tactic:
congr

Result:
case refl.e_a
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ (fun x => foldlM.loop (n + 1) f x (n + 1)) = fun x => foldlM.loop n (fun x j => f x j.succ) x n

Proof state:
case refl.e_a
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ (fun x => foldlM.loop (n + 1) f x (n + 1)) = fun x => foldlM.loop n (fun x j => f x j.succ) x n

Tactic:
funext

Result:
case refl.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
x✝ : α
⊢ foldlM.loop (n + 1) f x✝ (n + 1) = foldlM.loop n (fun x j => f x j.succ) x✝ n

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
⊢ (do
      let x ← f x ⟨i, h⟩
      foldlM.loop (n + 1) f x (i + 1)) =
    do
    let x ← f x ⟨i, h⟩
    foldlM.loop n (fun x j => f x j.succ) x i

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
⊢ (fun x => foldlM.loop (n + 1) f x (i + 1)) = fun x => foldlM.loop n (fun x j => f x j.succ) x i

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : ¬i < n
⊢ foldlM.loop (n + 1) f x i = do
    let x ← f x ⟨i, h⟩
    foldlM.loop n (fun x j => f x j.succ) x i

Tactic:
cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')

Result:
case refl
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldlM.loop (n + 1) f x n = do
    let x ← f x ⟨n, h⟩
    foldlM.loop n (fun x j => f x j.succ) x n

Proof state:
case refl
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldlM.loop (n + 1) f x n = do
    let x ← f x ⟨n, h⟩
    foldlM.loop n (fun x j => f x j.succ) x n

Tactic:
rw [foldlM_loop_lt]

Result:
case refl
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ (do
      let x ← f x ⟨n, ?refl.h⟩
      foldlM.loop (n + 1) f x (n + 1)) =
    do
    let x ← f x ⟨n, h⟩
    foldlM.loop n (fun x j => f x j.succ) x n

case refl.h
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
⊢ n < n + 1

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ foldlM.loop (n + 1) f x✝ (i + 1) = foldlM.loop n (fun x j => f x j.succ) x✝ i

Tactic:
rw [foldlM_loop_lt _ _ h', foldlM_loop]

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ (do
      let x ← f x✝ ⟨i + 1, ?e_a.h.h✝⟩
      foldlM.loop n (fun x j => f x j.succ) x (i + 1)) =
    do
    let x ← f x✝ ⟨i, h'⟩.succ
    foldlM.loop n (fun x j => f x j.succ) x (i + 1)

case e_a.h.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ i + 1 < n + 1

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
⊢ (fun x => foldlM.loop (n + 1) f x (i + 1)) = fun x => foldlM.loop n (fun x j => f x j.succ) x i

Tactic:
funext

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ foldlM.loop (n + 1) f x✝ (i + 1) = foldlM.loop n (fun x j => f x j.succ) x✝ i

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ (do
      let x ← f x✝ ⟨i + 1, ?e_a.h.h✝⟩
      foldlM.loop n (fun x j => f x j.succ) x (i + 1)) =
    do
    let x ← f x✝ ⟨i, h'⟩.succ
    foldlM.loop n (fun x j => f x j.succ) x (i + 1)

case e_a.h.h
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
x✝ : α
⊢ i + 1 < n + 1

Tactic:
rfl

Result:
no goals

Proof state:
case refl.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : n < n + 1
h' : ¬n < n
x✝ : α
⊢ foldlM.loop (n + 1) f x✝ (n + 1) = foldlM.loop n (fun x j => f x j.succ) x✝ n

Tactic:
rw [foldlM_loop_eq, foldlM_loop_eq]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
⊢ foldlM.loop (n + 1) f x i = do
    let x ← f x ⟨i, h⟩
    foldlM.loop n (fun x j => f x j.succ) x i

Tactic:
rw [foldlM_loop_lt _ _ h]

Result:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin (n + 1) → m α
x : α
h : i < n + 1
h' : i < n
⊢ (do
      let x ← f x ⟨i, h⟩
      foldlM.loop (n + 1) f x (i + 1)) =
    do
    let x ← f x ⟨i, h⟩
    foldlM.loop n (fun x j => f x j.succ) x i