refine (heapSort.Intermed.mkHeap lt x).of_spec (.mk lt (mkHeap lt x) _) .refl i j ?_ hij ?_
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ lt (heapSort lt x)[j] (heapSort lt x)[i] = false
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ (mkHeap lt x).stop - Subarray.size (mkHeap lt x) ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop