Theorem: Array.foldl_append (LeanSAT/Upstream/ToStd.lean)

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A B : Array α
⊢ foldl f init (A ++ B) 0 = foldl f (foldl f init A 0) B 0
Tactic:
have ⟨A⟩ := A
State after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B : Array α
A : List α
⊢ foldl f init ({ data := A } ++ B) 0 = foldl f (foldl f init { data := A } 0) B 0

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B : Array α
A : List α
⊢ foldl f init ({ data := A } ++ B) 0 = foldl f (foldl f init { data := A } 0) B 0
Tactic:
have ⟨B⟩ := B
State after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ foldl f init ({ data := A } ++ { data := B }) 0 = foldl f (foldl f init { data := A } 0) { data := B } 0

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ foldl f init ({ data := A } ++ { data := B }) 0 = foldl f (foldl f init { data := A } 0) { data := B } 0
Tactic:
simp only [foldl_eq_foldl_data, append_data]
State after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ List.foldl f init (A ++ B) = List.foldl f (List.foldl f init A) B

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ List.foldl f init (A ++ B) = List.foldl f (List.foldl f init A) B
Tactic:
exact List.foldl_append _ _ _ _
State after:
no goals