rw [IH, get_as_heapifyDown_of_lt_start lt x n k hlt]
case succ
α : Type u
lt : α → α → Bool
k n : Nat
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hlt : k < x.start
IH : (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = (heapifyDown lt x n).as[k]
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]
no goals