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

State before:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ fold' (n + 1) f init = f (Fin.last n) (fold' n (f ∘ Fin.castSucc) init)
Tactic:
dsimp [fold', dfold]
State after:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ f { val := n, isLt := (_ : Nat.le (n + 1) (n + 1)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1)) =
    f (Fin.last n)
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init)
        (_ : Nat.le n n))

State before:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ f { val := n, isLt := (_ : Nat.le (n + 1) (n + 1)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1)) =
    f (Fin.last n)
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init)
        (_ : Nat.le n n))
Tactic:
apply congrArg
State after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)

State before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
let mot₁ : Nat → Type u := fun i => i ≤ n+1 → α
State after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)

State before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
let mot₂ : Nat → Type u := fun i => i ≤ n → α
State after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)

State before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
suffices ∀ (k : Nat) (hk : k ≤ n), dfold (α:=mot₁) _ k (fun _ => init) (.step hk) = dfold (α:=mot₂) _ k (fun _ => init) hk
from this n .refl
State after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ ∀ (k : Nat) (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk

State before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ ∀ (k : Nat) (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Tactic:
intro k hk
State after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
hk : k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk

State before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
hk : k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Tactic:
induction k with
| zero => rfl
| succ k IH =>
  dsimp [dfold]; apply congrArg
  exact IH (Nat.le_of_succ_le hk)
State after:
no goals

State before:
case h.zero
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
hk : zero ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) zero (fun x => init) (_ : Nat.le zero (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) zero (fun x => init) hk
Tactic:
rfl
State after:
no goals

State before:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) (succ k) (fun x => init)
      (_ : Nat.le (succ k) (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) (succ k) (fun x => init) hk
Tactic:
dsimp [dfold]
State after:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ f { val := k, isLt := (_ : Nat.le (succ k) (succ n)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1)) =
    f (Fin.castSucc { val := k, isLt := hk })
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n))

State before:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ f { val := k, isLt := (_ : Nat.le (succ k) (succ n)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1)) =
    f (Fin.castSucc { val := k, isLt := hk })
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n))
Tactic:
apply congrArg
State after:
case h.succ.h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n)

State before:
case h.succ.h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n)
Tactic:
exact IH (Nat.le_of_succ_le hk)
State after:
no goals