Theorem: Fin.foldAll_comp_val (Algdata/Data/Fin/Basic.lean)

State before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ foldAll (f ∘ val) init = Nat.fold f n init
Tactic:
unfold foldAll
State after:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (foldAllM (f ∘ val) init) = Nat.fold f n init

State before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (foldAllM (f ∘ val) init) = Nat.fold f n init
Tactic:
rw [Nat.fold_eq_foldM, foldAllM_comp_val]
State after:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (Nat.foldM f init n) = Nat.foldM f init n

State before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (Nat.foldM f init n) = Nat.foldM f init n
Tactic:
rfl
State after:
no goals