all_goals simp only [size_mkHeap, stop_mkHeap]
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
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
⊢ x.stop - Subarray.size 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 < x.stop