exact .out_of_range i <| Nat.le_trans hsize hi
case out_of_range
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
hi : i ≥ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
no goals