induction n generalizing x with
| zero => rfl
| succ n IH =>
  dsimp [mkHeap.loop] at hk ⊢
  conv at hk => rw [size_as_mkHeap_loop, size_as_heapifyDown]
  specialize @IH (heapifyDown lt x n)
    ((size_as_mkHeap_loop lt _ n).symm ▸ size_as_heapifyDown lt x n ▸ hk)
    (start_heapifyDown lt x n ▸ hlt)
  rw [IH, get_as_heapifyDown_of_lt_start lt x n k hlt]
α : Type u
lt : α → α → Bool
x : Subarray α
n k : Nat
hk : k < Array.size (mkHeap.loop lt x n).as
hlt : k < x.start
⊢ (mkHeap.loop lt x n).as[k] = x.as[k]
no goals