by_cases start = stop with
| isTrue heq =>
  cases heq
  rw [foldl_stop] <;> try (exact hstop)
  rw [foldl_stop]; exact hstop
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  have : start < as.size := Nat.lt_of_lt_of_le hstart' hstop
  rw [foldl_step h (h b c)] <;> try (first | exact hstop | exact hstart')
  rw [foldl_step h c] <;> try (first | exact hstop | exact hstart')
  rw [Std.Associative.assoc (op:=h)]
  rw [foldl_assoc as b (h c as[start]) (start+1) stop hstart' hstop]
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
no goals