no goals
α : Type u_1
a : Array α
x : α
i : Nat
h : i < size (push a x)
⊢ (push a x)[i] = if h : i < size a then a[i] else x
if h' : i < a.size then
  simp [get_push_lt, h']
else
  simp at h
  simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
no goals
α : Type u_1
a : Array α
x : α
i : Nat
h : i < size (push a x)
h' : i < size a
⊢ (push a x)[i] = if h : i < size a then a[i] else x
simp [get_push_lt, h']
α : Type u_1
a : Array α
x : α
i : Nat
h✝ : i < size (push a x)
h' : ¬i < size a
h : i < size a + 1
⊢ (push a x)[i] = if h : i < size a then a[i] else x
α : Type u_1
a : Array α
x : α
i : Nat
h : i < size (push a x)
h' : ¬i < size a
⊢ (push a x)[i] = if h : i < size a then a[i] else x
simp at h
no goals
α : Type u_1
a : Array α
x : α
i : Nat
h✝ : i < size (push a x)
h' : ¬i < size a
h : i < size a + 1
⊢ (push a x)[i] = if h : i < size a then a[i] else x
simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]