Theorem: Array.size_append (Algdata/Data/Array/Lemmas.lean)

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

State before:
α : Type u
x y : Array α
⊢ List.length (x ++ y).data = List.length x.data + List.length y.data
Tactic:
rw [append_data' x y]
State after:
α : Type u
x y : Array α
⊢ List.length (x.data ++ y.data) = List.length x.data + List.length y.data

State before:
α : Type u
x y : Array α
⊢ List.length (x.data ++ y.data) = List.length x.data + List.length y.data
Tactic:
exact List.length_append x.data y.data
State after:
no goals