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

State before:
m : Type u → Type v
inst✝ : Monad m
n : Nat
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init n
Tactic:
induction n generalizing f init
State after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
n✝ : Nat
n_ih✝ : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n✝
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n✝)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero
Tactic:
case zero => rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n)
Tactic:
case succ n h_ind =>
  rw [foldAllM_succ]; dsimp
  have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
    funext fun x => rfl
  conv => lhs; rhs; rw [this]; ext x; rw [h_ind]
  conv => rhs; rw [Nat.foldM_succ]
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero
Tactic:
rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n)
Tactic:
rw [foldAllM_succ]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ (f ∘ val) 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ (f ∘ val) 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
dsimp
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
  funext fun x => rfl
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
conv => lhs; rhs; rw [this]; ext x; rw [h_ind]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ (do
      let x ← f 0 init
      Nat.foldM (f ∘ Nat.succ) x n) =
    Nat.foldM f init (Nat.succ n)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ (do
      let x ← f 0 init
      Nat.foldM (f ∘ Nat.succ) x n) =
    Nat.foldM f init (Nat.succ n)
Tactic:
conv => rhs; rw [Nat.foldM_succ]
State after:
no goals