Theorem: Array.get_push_old (LeanSAT/AIG/Basic.lean)

State before:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < (as.push a).size
Tactic:
simp
State after:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < as.size + 1

State before:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < as.size + 1
Tactic:
omega
State after:
no goals

State before:
α : Type u_1
i : Nat
as : Array α
a : α
h : i < as.size
⊢ (as.push a)[i] = as[i]
Tactic:
simp [Array.get_push, h]
State after:
no goals