Theorem: Array.append_size (YatimaStdLib/Array.lean)

State before:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : size arr₁ = n
h2 : size arr₂ = m
⊢ size (arr₁ ++ arr₂) = n + m
Tactic:
unfold Array.size at *
State after:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : List.length arr₁.data = n
h2 : List.length arr₂.data = m
⊢ List.length (arr₁ ++ arr₂).data = n + m

State before:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : List.length arr₁.data = n
h2 : List.length arr₂.data = m
⊢ List.length (arr₁ ++ arr₂).data = n + m
Tactic:
simp [h1, h2]
State after:
no goals