dsimp [mkHeap.loop] at hk ⊢
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k ≥ x.stop → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk : k < Array.size (mkHeap.loop lt x (Nat.succ n)).as
hge : k ≥ x.stop
⊢ (mkHeap.loop lt x (Nat.succ n)).as[k] = x.as[k]
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k ≥ x.stop → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hge : k ≥ x.stop
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]