refine .out_of_range _ h
case out_of_range
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
j₁ j₂ : Fin (Subarray.size x)
i✝ : Nat
h : i✝ ≥ Subarray.size x
hj₁ : ↑j₁ < i✝
hj₂ : ↑j₂ < i✝
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i✝
no goals