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

State before:
α : Type u
as : Array α
a : α
⊢ (push as a)[size as] = a
Tactic:
simp only [get_push', size_push, dif_neg (Nat.lt_irrefl as.size)]
State after:
no goals