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

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM f init (n + 1) = foldM f init n >>= f n
Tactic:
induction n generalizing f init
State after:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero

case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n✝ : Nat
n_ih✝ : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n✝ + 1) = foldM f init n✝ >>= f n✝
f : Nat → α → m α
init : α
⊢ foldM f init (succ n✝ + 1) = foldM f init (succ n✝) >>= f (succ n✝)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero
Tactic:
case zero =>
  conv =>
    dsimp [foldM, foldM.loop]
    change f 0 init >>= pure = pure init >>= f 0
  simp only [pure_bind, bind_pure]
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (succ n + 1) = foldM f init (succ n) >>= f (succ n)
Tactic:
case succ n h_ind =>
  simp only [Nat.succ_eq_add_one]
  conv => lhs; rw [foldM_succ]; rhs; ext; rw [h_ind]
  conv => rhs; rw [foldM_succ]
  dsimp; rw [bind_assoc]
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero
Tactic:
conv =>
  dsimp [foldM, foldM.loop]
  change f 0 init >>= pure = pure init >>= f 0
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ f 0 init >>= pure = pure init >>= f 0

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ f 0 init >>= pure = pure init >>= f 0
Tactic:
simp only [pure_bind, bind_pure]
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (succ n + 1) = foldM f init (succ n) >>= f (succ n)
Tactic:
simp only [Nat.succ_eq_add_one]
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (n + 1 + 1) = foldM f init (n + 1) >>= f (n + 1)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ foldM f init (n + 1 + 1) = foldM f init (n + 1) >>= f (n + 1)
Tactic:
conv => lhs; rw [foldM_succ]; rhs; ext; rw [h_ind]
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) = foldM f init (n + 1) >>= f (n + 1)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) = foldM f init (n + 1) >>= f (n + 1)
Tactic:
conv => rhs; rw [foldM_succ]
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Tactic:
dsimp
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= f (succ n)) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= f (succ n)) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
Tactic:
rw [bind_assoc]
State after:
no goals