Theorem: Array.size_append (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
as bs : Array α
⊢ size (as ++ bs) = size as + size bs
Tactic:
dsimp [size]
State after:
α : Type u
as bs : Array α
⊢ List.length (as ++ bs).data = List.length as.data + List.length bs.data

State before:
α : Type u
as bs : Array α
⊢ List.length (as ++ bs).data = List.length as.data + List.length bs.data
Tactic:
rw [append_data, List.length_append]
State after:
no goals