induction h with
| @zero x =>
  let k := i - x.start
  have hki : i = x.start + k := by
    rw [Nat.add_comm, Nat.sub_add_cancel ge_start]
  have hk : k < x.size := by
    refine Nat.lt_sub_of_add_lt ?_
    simp only [Nat.sub_add_cancel ge_start]
    exact lt_stop
  exists k, hk
  exact getElem_eq (x:=x.as) (y:=x.as) rfl hki
| @succ x n y h IH =>
  specialize IH (start_popMax lt x ▸ ge_start)
  have hrng : x.start < x.stop := trans ge_start lt_stop
  cases Nat.lt_or_eq_of_le (Nat.le_pred_of_lt lt_stop) with
  | inl hlt =>
    have ⟨k,hk,hy⟩ := IH (stop_popMax lt x hrng ▸ hlt)
    have ⟨l,hl,_,hx⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
    simp only [hy, hx]
    exact ⟨l, hl, rfl⟩
  | inr heq =>
    cases heq
    rewrite [h.get_eq_of_ge_stop (x.stop-1) (stop_popMax lt x hrng ▸ .refl)]
    rewrite [get_as_popMax_stop_sub_one lt x hrng]
    exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
ge_start : x.start ≤ i
lt_stop : i < x.stop
⊢ ∃ k hk, y[i] = x[k]
no goals