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

State before:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ ns.sum stop stop = 0
Tactic:
simp only [sum]
State after:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns stop stop = 0

State before:
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns stop stop = 0
Tactic:
rw [foldl_stop]
State after:
case hstop
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ stop ≤ ns.size

State before:
case hstop
ns : Array Nat
stop : Nat
hstop : stop ≤ ns.size
⊢ stop ≤ ns.size
Tactic:
exact hstop
State after:
no goals