case mpr =>
  intro h
  split
  case inl => exists as[0]
  case inr hs => exact absurd (Nat.zero_lt_of_ne_zero h) hs
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
no goals