-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
    foldlM.loop f #[] s h i j init = pure init

Proof state:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
h✝ : ¬j < s
⊢ pure init = pure init

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
h✝ : j < s
⊢ (match i with
    | 0 => pure init
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f init #[][j]
      foldlM.loop f #[] s h i' (j + 1) __do_lift) =
    pure init

Tactic:
split

Result:
case isTrue.h_1
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ : Nat
⊢ pure init = pure init

case isTrue.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ i'✝ : Nat
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f init #[][j]
    foldlM.loop f #[] s h i'✝ (j + 1) __do_lift) =
    pure init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
⊢ foldlM.loop f #[] s h i j init = pure init

Tactic:
unfold foldlM.loop

Result:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
⊢ (if hlt : j < s then
      match i with
      | 0 => pure init
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][j]
        foldlM.loop f #[] s h i' (j + 1) __do_lift
    else pure init) =
    pure init

Proof state:
case isTrue.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h✝¹ : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ i'✝ : Nat
h : s = 0
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f init #[][j]
    foldlM.loop f #[] s h✝¹ i'✝ (j + 1) __do_lift) =
    pure init

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ i'✝ : Nat
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f init #[][j]
    foldlM.loop f #[] s h i'✝ (j + 1) __do_lift) =
    pure init

Tactic:
simp at h

Result:
case isTrue.h_2
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h✝¹ : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ i'✝ : Nat
h : s = 0
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f init #[][j]
    foldlM.loop f #[] s h✝¹ i'✝ (j + 1) __do_lift) =
    pure init

Proof state:
case isTrue.h_1
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
j : Nat
h✝ : j < s
i✝ : Nat
⊢ pure init = pure init

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
⊢ (if hlt : j < s then
      match i with
      | 0 => pure init
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][j]
        foldlM.loop f #[] s h i' (j + 1) __do_lift
    else pure init) =
    pure init

Tactic:
split

Result:
case isTrue
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
h✝ : j < s
⊢ (match i with
    | 0 => pure init
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f init #[][j]
      foldlM.loop f #[] s h i' (j + 1) __do_lift) =
    pure init

case isFalse
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
s : Nat
h : s ≤ #[].size
inst✝ : Monad m
f : β → α → m β
init : β
i j : Nat
h✝ : ¬j < s
⊢ pure init = pure init