dsimp [mkHeap.loop]
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x (Nat.succ n))[k] = x[l]
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]