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

State before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
Tactic:
have : start < ns.size := Nat.lt_of_lt_of_le hstart hstop
State after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop

State before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
Tactic:
simp only [sum]
State after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns start stop = ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop

State before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns start stop = ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [foldl_step] <;> try assumption
State after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (0 + ns[start]) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop

State before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (0 + ns[start]) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [Nat.add_comm 0 ns[start]]
State after:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (ns[start] + 0) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop

State before:
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) (ns[start] + 0) ns (start + 1) stop =
    ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop
Tactic:
rw [ns.foldl_assoc (.+.) ns[start] 0 (start+1) stop (Nat.succ_le_of_lt hstart) hstop]
State after:
no goals

State before:
case hstop
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ stop ≤ ns.size
Tactic:
assumption
State after:
no goals