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

State before:
α : Type u
f : Nat → α → α
init : α
n : Nat
⊢ fold f n init = foldM f init n
Tactic:
induction n
State after:
case zero
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero

case succ
α : Type u
f : Nat → α → α
init : α
n✝ : Nat
n_ih✝ : fold f n✝ init = foldM f init n✝
⊢ fold f (succ n✝) init = foldM f init (succ n✝)

State before:
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero
Tactic:
case zero => rfl
State after:
no goals

State before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = foldM f init (succ n)
Tactic:
case succ n h_ind =>
  rw [foldM_succ_eq_foldM_bind, ←h_ind]; rfl
State after:
no goals

State before:
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero
Tactic:
rfl
State after:
no goals

State before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = foldM f init (succ n)
Tactic:
rw [foldM_succ_eq_foldM_bind, ←h_ind]
State after:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = fold f n init >>= f n

State before:
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = fold f n init >>= f n
Tactic:
rfl
State after:
no goals