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

State before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldrM f b as stop stop = pure b
Tactic:
simp only [Array.foldrM]
State after:
α : Type u_1
β : Type u_3
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 if stop < stop then foldrM.fold f as stop stop h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    pure b

State before:
α : Type u_1
β : Type u_3
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 if stop < stop then foldrM.fold f as stop stop h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    pure b
Tactic:
rw [dif_pos hstop]
State after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if stop < stop then foldrM.fold f as stop stop hstop b else pure b) = pure b

State before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if stop < stop then foldrM.fold f as stop stop hstop b else pure b) = pure b
Tactic:
rw [if_neg (by irreflexivity)]
State after:
no goals

State before:
α : Type u_1
β : Type u_3
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