Theorem: Fin.foldlM_eq_foldl (LeanColls/MathlibUpstream.lean)

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM n init f =
    foldl n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init)
Tactic:
simp [foldl, foldlM]
State after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
suffices ∀ i j (hj : i + j = n) macc,
  (macc >>= fun acc => foldlM.aux n f i acc) =
    foldl.loop n _ macc i
  by
  have := this 0 n (by simp) (pure init)
  simp at this
  exact this
State after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ ∀ (i j : ℕ),
    i + j = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ ∀ (i j : ℕ),
    i + j = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
Tactic:
intro i j hj
State after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i j : ℕ
hj : i + j = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i j : ℕ
hj : i + j = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i
Tactic:
induction j generalizing i with
| zero =>
  intro macc
  simp at hj; cases hj
  unfold foldl.loop; unfold foldlM.aux
  simp
| succ j' ih =>
  intro macc
  rw [Nat.add_succ, ← Nat.succ_add] at hj
  have hi : i < n := by calc
    _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
    _ = n := hj
  have := ih (i+1) hj (macc >>= fun acc => f ⟨i,hi⟩ acc)
  clear ih
  unfold foldl.loop; unfold foldlM.aux
  simp_all
State after:
no goals

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
have := this 0 n (by simp) (pure init)
State after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this :
  (do
      let acc ← pure init
      foldlM.aux n f 0 acc) =
    foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this :
  (do
      let acc ← pure init
      foldlM.aux n f 0 acc) =
    foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
simp at this
State after:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this : foldlM.aux n f 0 init = foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this : foldlM.aux n f 0 init = foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
Tactic:
exact this
State after:
no goals

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
⊢ 0 + n = n
Tactic:
simp
State after:
no goals

State before:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
hj : i + 0 = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i
Tactic:
intro macc
State after:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
hj : i + 0 = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
hj : i + 0 = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
simp at hj
State after:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
macc : m β
hj : i = n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case zero
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i : ℕ
macc : m β
hj : i = n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
cases hj
State after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc n

State before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc n
Tactic:
unfold foldl.loop
State after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc

State before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Tactic:
unfold foldlM.aux
State after:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      if h' : n < n then do
          let acc ← f ⟨n, h'⟩ acc
          foldlM.aux n f (n + 1) acc
        else pure acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc

State before:
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      if h' : n < n then do
          let acc ← f ⟨n, h'⟩ acc
          foldlM.aux n f (n + 1) acc
        else pure acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
Tactic:
simp
State after:
no goals

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i
Tactic:
intro macc
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i + (j' + 1) = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
rw [Nat.add_succ, ← Nat.succ_add] at hj
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
have hi : i < n := by calc
  _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
  _ = n := hj
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
have := ih (i+1) hj (macc >>= fun acc => f ⟨i,hi⟩ acc)
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
clear ih
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      macc i
Tactic:
unfold foldl.loop
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Tactic:
unfold foldlM.aux
State after:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      if h' : i < n then do
          let acc ← f ⟨i, h'⟩ acc
          foldlM.aux n f (i + 1) acc
        else pure acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc

State before:
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      if h' : i < n then do
          let acc ← f ⟨i, h'⟩ acc
          foldlM.aux n f (i + 1) acc
        else pure acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
Tactic:
simp_all
State after:
no goals

State before:
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    i + j' = n →
      ∀ (macc : m β),
        (do
            let acc ← macc
            foldlM.aux n f i acc) =
          foldl.loop n
            (fun macc i => do
              let acc ← macc
              f i acc)
            macc i
i : ℕ
hj : i.succ + j' = n
macc : m β
⊢ i < n
Tactic:
calc
_ ≤ Nat.succ i + j' := Nat.le_add_right _ _
_ = n := hj
State after:
no goals