have hk : k < x.size := by
  refine Nat.lt_sub_of_add_lt ?_
  simp only [Nat.sub_add_cancel ge_start]
  exact lt_stop
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ ∃ k hk, x.as[i] = x[k]
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
hk : k < Subarray.size x
⊢ ∃ k hk, x.as[i] = x[k]