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

State before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (fold' n f init)
Tactic:
dsimp [fold', dfold]
State after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
refine dfold_induction (α := fun i => i ≤ n → α) (motive := fun i a => (h : i ≤ n) → motive i (a h)) _ n (fun _ => init) (fun _ => zero) ?_ .refl
State after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ ∀ (n_1 : Nat) (a : (fun i => i ≤ n → α) n_1),
    (fun i a => ∀ (h : i ≤ n), motive i (a h)) n_1 a →
      (fun i a => ∀ (h : i ≤ n), motive i (a h)) (n_1 + 1) fun hi => f { val := n_1, isLt := hi } (a (_ : n_1 ≤ n))

State before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ ∀ (n_1 : Nat) (a : (fun i => i ≤ n → α) n_1),
    (fun i a => ∀ (h : i ≤ n), motive i (a h)) n_1 a →
      (fun i a => ∀ (h : i ≤ n), motive i (a h)) (n_1 + 1) fun hi => f { val := n_1, isLt := hi } (a (_ : n_1 ≤ n))
Tactic:
intro i a IH hi
State after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
i : Nat
a : i ≤ n → α
IH : ∀ (h : i ≤ n), motive i (a h)
hi : i + 1 ≤ n
⊢ motive (i + 1) (f { val := i, isLt := hi } (a (_ : i ≤ n)))

State before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
i : Nat
a : i ≤ n → α
IH : ∀ (h : i ≤ n), motive i (a h)
hi : i + 1 ≤ n
⊢ motive (i + 1) (f { val := i, isLt := hi } (a (_ : i ≤ n)))
Tactic:
exact succ i hi _ (IH _)
State after:
no goals