-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem fold_eq_foldTR : @fold = @foldTR :=
  funext fun α => funext fun n => funext fun f => funext fun init =>
  let rec go : ∀ m n f, fold (m + n) f init = foldTR.loop (m + n) f m (by omega) (fold n (fun i h => f i (by omega)) init)
    | 0,      n, f => by
      simp only [foldTR.loop]
      have t : 0 + n = n

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).fold f init = foldTR.loop (m.succ + n) f m.succ ⋯ (n.fold (fun i h => f i ⋯) init)

Tactic:
rw [foldTR.loop]

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).fold f init = foldTR.loop (m.succ + n) f m ⋯ (f (m.succ + n - m.succ) ⋯ (n.fold (fun i h => f i ⋯) init))

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
⊢ m + 1 + n = m + (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m + 1 + n).fold f init = foldTR.loop (m + 1 + n) f m ⋯ (f (m + 1 + n - (m + 1)) ⋯ (n.fold (fun i h => f i ⋯) init))

Tactic:
rw [fold_congr t, foldTR_loop_congr t, go, fold]

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ foldTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯ (f n ⋯ (n.fold (fun i h => f i ⋯) init)) =
    foldTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯ (f (m + 1 + n - (m + 1)) ⋯ (n.fold (fun i h => f i ⋯) init))

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
⊢ (0 + n).fold f init = n.fold (fun i h => f i ⋯) init

Tactic:
have t : 0 + n = n := by omega

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
t : 0 + n = n
⊢ (0 + n).fold f init = n.fold (fun i h => f i ⋯) init

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).fold f init = foldTR.loop (m.succ + n) f m ⋯ (f (m.succ + n - m.succ) ⋯ (n.fold (fun i h => f i ⋯) init))

Tactic:
simp only [succ_eq_add_one, Nat.add_sub_cancel]

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m + 1 + n).fold f init = foldTR.loop (m + 1 + n) f m ⋯ (f (m + 1 + n - (m + 1)) ⋯ (n.fold (fun i h => f i ⋯) init))

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
⊢ 0 + n = n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
⊢ (0 + n).fold f init = foldTR.loop (0 + n) f 0 ⋯ (n.fold (fun i h => f i ⋯) init)

Tactic:
simp only [foldTR.loop]

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
⊢ (0 + n).fold f init = n.fold (fun i h => f i ⋯) init

Proof state:
case e_a.e_i
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ n = m + 1 + n - (m + 1)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ foldTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯ (f n ⋯ (n.fold (fun i h => f i ⋯) init)) =
    foldTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯ (f (m + 1 + n - (m + 1)) ⋯ (n.fold (fun i h => f i ⋯) init))

Tactic:
congr

Result:
case e_a.e_i
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ n = m + 1 + n - (m + 1)

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m + n → α → α
i : Nat
h : i < n
⊢ i < m + n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m + n → α → α
⊢ m ≤ m + n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
n : Nat
f : (i : Nat) → i < 0 + n → α → α
t : 0 + n = n
⊢ (0 + n).fold f init = n.fold (fun i h => f i ⋯) init

Tactic:
rw [fold_congr t]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
⊢ (m.succ + n).fold f init = foldTR.loop (m.succ + n) f m.succ ⋯ (n.fold (fun i h => f i ⋯) init)

Tactic:
have t : (m + 1) + n = m + (n + 1) := by omega

Result:
α : Type u_1
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → α → α
init : α
m n : Nat
f : (i : Nat) → i < m.succ + n → α → α
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).fold f init = foldTR.loop (m.succ + n) f m.succ ⋯ (n.fold (fun i h => f i ⋯) init)