induction n generalizing x with
| zero => exact ⟨k,hk,rfl⟩
| succ n IH =>
  dsimp [mkHeap.loop]
  have ⟨l',hl',IH⟩ := IH (heapifyDown lt x n) (size_heapifyDown lt x n ▸ hk)
  simp only [IH]
  exact exists_get_heapifyDown lt x n l' (size_heapifyDown lt x n ▸ hl')
α : Type u
lt : α → α → Bool
x : Subarray α
n k : Nat
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
no goals