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

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

State before:
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ Id.run (foldAllM f init) = Id.run (foldAllM (f ∘ succ) (f 0 init))
Tactic:
exact foldAllM_succ
State after:
no goals