Theorem: Nat.foldRev_succ (Algdata/Init/Nat.lean)

State before:
α : Type u_1
f : Nat → α → α
n : Nat
init : α
⊢ foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
Tactic:
induction n generalizing f init with
| zero => rfl
| succ n IH =>
  unfold foldRev; simp only [Nat.add, Nat.succ_eq_add_one]
  rewrite [IH]; rfl
State after:
no goals

State before:
case zero
α : Type u_1
f : Nat → α → α
init : α
⊢ foldRev f (zero + 1) init = f 0 (foldRev (f ∘ succ) zero init)
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (succ n + 1) init = f 0 (foldRev (f ∘ succ) (succ n) init)
Tactic:
unfold foldRev
State after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (Nat.add (succ n) 0) (f (Nat.add (succ n) 0) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))

State before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (Nat.add (succ n) 0) (f (Nat.add (succ n) 0) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
simp only [Nat.add, Nat.succ_eq_add_one]
State after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (n + 1) (f (n + 1) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))

State before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (n + 1) (f (n + 1) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
rewrite [IH]
State after:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ f 0 (foldRev (f ∘ succ) n (f (n + 1) init)) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))

State before:
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ f 0 (foldRev (f ∘ succ) n (f (n + 1) init)) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
Tactic:
rfl
State after:
no goals