Theorem: Array.foldlM_stop (GMLInit/Data/Array/Basic.lean)

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM f b as stop stop = pure b
Tactic:
simp only [Array.foldlM]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - stop) stop b
    else foldlM.loop f as as.size ⋯ (as.size - stop) stop b) =
    pure b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - stop) stop b
    else foldlM.loop f as as.size ⋯ (as.size - stop) stop b) =
    pure b
Tactic:
rw [dif_pos hstop]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - stop) stop b = pure b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - stop) stop b = pure b
Tactic:
rw [Array.foldlM.loop]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if hlt : stop < stop then
      match stop - stop with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[stop]
        foldlM.loop f as stop ⋯ i' (stop + 1) __do_lift
    else pure b) =
    pure b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if hlt : stop < stop then
      match stop - stop with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[stop]
        foldlM.loop f as stop ⋯ i' (stop + 1) __do_lift
    else pure b) =
    pure b
Tactic:
rw [dif_neg (by irreflexivity)]
State after:
no goals

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ ¬stop < stop
Tactic:
irreflexivity
State after:
no goals