Theorem: Array.foldl_empty (LeanSAT/Upstream/ToStd.lean)

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ foldl f init #[] start stop = init
Tactic:
simp [foldl, foldlM, Id.run]
State after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
by_cases h : stop = 0
State after:
case pos
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init

case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init

State before:
case pos
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
simp [h, foldlM.loop]
State after:
no goals

State before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
Tactic:
simp [h]
State after:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ foldlM.loop f #[] 0 ⋯ 0 start init = init

State before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ foldlM.loop f #[] 0 ⋯ 0 start init = init
Tactic:
unfold foldlM.loop
State after:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if hlt : start < 0 then
      match 0 with
      | 0 => pure init
      | Nat.succ i' =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][start]
        foldlM.loop f #[] 0 ⋯ i' (start + 1) __do_lift
    else pure init) =
    init

State before:
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if hlt : start < 0 then
      match 0 with
      | 0 => pure init
      | Nat.succ i' =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][start]
        foldlM.loop f #[] 0 ⋯ i' (start + 1) __do_lift
    else pure init) =
    init
Tactic:
simp [Nat.not_lt_zero start]
State after:
no goals