internlm/Lean-Github huggingface dataset:
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let init' : α' 0 := fun _ => init
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
suffices ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init') by
  rw [this n]
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Tactic:
intro k
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Tactic:
refine dfold_hom f' g₁' g₂' k init' ?_
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ ∀ (n : Nat) (a : α' n), g₂' n (f' n a) = f' (n + 1) (g₁' n a)
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ ∀ (n : Nat) (a : α' n), g₂' n (f' n a) = f' (n + 1) (g₁' n a)
Tactic:
intro i x
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ g₂' i (f' i x) = f' (i + 1) (g₁' i x)
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ g₂' i (f' i x) = f' (i + 1) (g₁' i x)
Tactic:
dsimp
Proof state after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ (fun hi => g₂ { val := i, isLt := hi } (f (x (_ : i ≤ n)))) = fun hi =>
    f (g₁ { val := i, isLt := hi } (x (_ : i ≤ n)))
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ (fun hi => g₂ { val := i, isLt := hi } (f (x (_ : i ≤ n)))) = fun hi =>
    f (g₁ { val := i, isLt := hi } (x (_ : i ≤ n)))
Tactic:
simp only [H]
Proof state after:
no goals
Theorem: Nat.fold'_hom
Proof state before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
this : ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
rw [this n]
Proof state after:
no goals
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
⊢ @fold' = @fold'TR
Tactic:
funext α n f init
Proof state after:
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ fold' n f init = fold'TR n f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ fold' n f init = fold'TR n f init
Tactic:
suffices ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α), fold'TR.loop k f m (h ▸ m.le_add_right n) (fold' n (fun i => f ⟨i.1, trans i.2 (h ▸ n.le_add_left m)⟩) init) = fold' k f init
from (this n 0 _ rfl f).symm
Proof state after:
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
Tactic:
clear n f
Proof state after:
case h.h.h.h
α : Type u_1
init : α
⊢ ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h
α : Type u_1
init : α
⊢ ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
Tactic:
intro m n k h f
Proof state after:
case h.h.h.h
α : Type u_1
init : α
m n k : Nat
h : m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) = fold' k f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h
α : Type u_1
init : α
m n k : Nat
h : m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) = fold' k f init
Tactic:
induction m generalizing n k init with
| zero =>
  rewrite [zero_eq, Nat.zero_add] at h; cases h
  simp only [fold'TR.loop, zero_eq]
| succ m IH =>
  rewrite [Nat.succ_add] at h; cases h
  dsimp [fold'TR.loop]
  have := fun a => IH a (n+1) (m+n+1) rfl f
  conv at this =>
    ext a; lhs; arg 5; rewrite [fold'_succ]
  rewrite [← this init]
  apply congrArg; apply congrFun; apply congrArg
  apply Fin.eq_of_val_eq
  simp only [Nat.succ_sub_succ_eq_sub, Nat.add_sub_cancel_left]
  rfl
Proof state after:
no goals
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.zero
α : Type u_1
init : α
n k : Nat
h : zero + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f zero (_ : zero ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Tactic:
rewrite [zero_eq, Nat.zero_add] at h
Proof state after:
case h.h.h.h.zero
α : Type u_1
init : α
n k : Nat
h✝ : zero + n = k
h : n = k
f : Fin k → α → α
⊢ fold'TR.loop k f zero (_ : zero ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.zero
α : Type u_1
init : α
n k : Nat
h✝ : zero + n = k
h : n = k
f : Fin k → α → α
⊢ fold'TR.loop k f zero (_ : zero ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Tactic:
cases h
Proof state after:
case h.h.h.h.zero.refl
α : Type u_1
init : α
n : Nat
h : zero + n = n
f : Fin n → α → α
⊢ fold'TR.loop n f zero (_ : zero ≤ n) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < n) }) init) =
    fold' n f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.zero.refl
α : Type u_1
init : α
n : Nat
h : zero + n = n
f : Fin n → α → α
⊢ fold'TR.loop n f zero (_ : zero ≤ n) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < n) }) init) =
    fold' n f init
Tactic:
simp only [fold'TR.loop, zero_eq]
Proof state after:
no goals
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n k : Nat
h : succ m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f (succ m) (_ : succ m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Tactic:
rewrite [Nat.succ_add] at h
Proof state after:
case h.h.h.h.succ
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n k : Nat
h✝ : succ m + n = k
h : succ (m + n) = k
f : Fin k → α → α
⊢ fold'TR.loop k f (succ m) (_ : succ m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n k : Nat
h✝ : succ m + n = k
h : succ (m + n) = k
f : Fin k → α → α
⊢ fold'TR.loop k f (succ m) (_ : succ m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
Tactic:
cases h
Proof state after:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
⊢ fold'TR.loop (succ (m + n)) f (succ m) (_ : succ m ≤ succ (m + n))
      (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init) =
    fold' (succ (m + n)) f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
⊢ fold'TR.loop (succ (m + n)) f (succ m) (_ : succ m ≤ succ (m + n))
      (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init) =
    fold' (succ (m + n)) f init
Tactic:
dsimp [fold'TR.loop]
Proof state after:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Tactic:
have := fun a => IH a (n+1) (m+n+1) rfl f
Proof state after:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (fold' (n + 1) (fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) a) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (fold' (n + 1) (fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) a) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Tactic:
conv at this =>
  ext a; lhs; arg 5; rewrite [fold'_succ]
Proof state after:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold' (succ (m + n)) f init
Tactic:
rewrite [← this init]
Proof state after:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
      (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
        (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init))
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
      (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
        (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init))
Tactic:
apply congrArg
Proof state after:
case h.h.h.h.succ.refl.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
      (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init) =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
      (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init)