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

State before:
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ x ++ y ++ push z c = x ++ (y ++ push z c)
Tactic:
simp only [append_push]
State after:
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ push (x ++ y ++ z) c = push (x ++ (y ++ z)) c