Theorem: Nat.fold'_eq_fold'TR (Fifteen/Data/Nat/Basic.lean)

State before:
⊢ @fold' = @fold'TR
Tactic:
funext α n f init
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
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

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
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

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]
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

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
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

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]
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

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]
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))

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
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)

State before:
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)
Tactic:
apply congrFun
State after:
case h.h.h.h.succ.refl.h.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)) } =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }

State before:
case h.h.h.h.succ.refl.h.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)) } =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Tactic:
apply congrArg
State after:
case h.h.h.h.succ.refl.h.h.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
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }

State before:
case h.h.h.h.succ.refl.h.h.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
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Tactic:
apply Fin.eq_of_val_eq
State after:
case h.h.h.h.succ.refl.h.h.h.a
α : 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
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }.val =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }.val

State before:
case h.h.h.h.succ.refl.h.h.h.a
α : 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
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }.val =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }.val
Tactic:
simp only [Nat.succ_sub_succ_eq_sub, Nat.add_sub_cancel_left]
State after:
case h.h.h.h.succ.refl.h.h.h.a
α : 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
⊢ n = (Fin.last n).val

State before:
case h.h.h.h.succ.refl.h.h.h.a
α : 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
⊢ n = (Fin.last n).val
Tactic:
rfl
State after:
no goals