simp only [hy, hx]
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, y[i] = x[k]
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, x[l] = x[k]