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

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
⊢ foldl.loop (n + 1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i

Tactic:
if h' : i < n then
  rw [foldl_loop_lt _ _ h]
  rw [foldl_loop_lt _ _ h', foldl_loop]; rfl
else
  cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
  rw [foldl_loop_lt]
  rw [foldl_loop_eq, foldl_loop_eq]

Result:
no goals

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ foldl.loop (n + 1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i

Tactic:
rw [foldl_loop_lt _ _ h]

Result:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ foldl.loop (n + 1) f (f x ⟨i, h⟩) (i + 1) = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i

Proof state:
case refl
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldl.loop (n + 1) f x n = foldl.loop n (fun x j => f x j.succ) (f x ⟨n, h⟩) n

Tactic:
rw [foldl_loop_lt]

Result:
case refl
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldl.loop (n + 1) f (f x ⟨n, ?refl.h⟩) (n + 1) = foldl.loop n (fun x j => f x j.succ) (f x ⟨n, h⟩) n

case refl.h
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ n < n + 1

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ foldl.loop (n + 1) f (f x ⟨i, h⟩) (i + 1) = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i

Tactic:
rw [foldl_loop_lt _ _ h', foldl_loop]

Result:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ foldl.loop n (fun x j => f x j.succ) (f (f x ⟨i, h⟩) ⟨i + 1, ?h⟩) (i + 1) =
    foldl.loop n (fun x j => f x j.succ) (f (f x ⟨i, h⟩) ⟨i, h'⟩.succ) (i + 1)

case h
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ i + 1 < n + 1

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ foldl.loop n (fun x j => f x j.succ) (f (f x ⟨i, h⟩) ⟨i + 1, ?h⟩) (i + 1) =
    foldl.loop n (fun x j => f x j.succ) (f (f x ⟨i, h⟩) ⟨i, h'⟩.succ) (i + 1)

case h
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : i < n
⊢ i + 1 < n + 1

Tactic:
rfl

Result:
no goals

Proof state:
case refl
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldl.loop (n + 1) f (f x ⟨n, ?refl.h⟩) (n + 1) = foldl.loop n (fun x j => f x j.succ) (f x ⟨n, h⟩) n

case refl.h
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ n < n + 1

Tactic:
rw [foldl_loop_eq, foldl_loop_eq]

Result:
no goals

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin (n + 1) → α
x : α
h : i < n + 1
h' : ¬i < n
⊢ foldl.loop (n + 1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i

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

Result:
case refl
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
h : n < n + 1
h' : ¬n < n
⊢ foldl.loop (n + 1) f x n = foldl.loop n (fun x j => f x j.succ) (f x ⟨n, h⟩) n