if hk' : Descendant n k then
  suffices IsHeap lt (heapifyDown lt x n) n from
    this.descend hk'
  have : n ≤ 2 * n := by
    rewrite [Nat.two_mul]; exact Nat.le_add_left n n
  refine is_heap_heapifyDown lt x n ?_ ?_
  all_goals apply IH; apply Nat.succ_le_succ
  . exact this
  . exact .step this
else
  have : n < k := Nat.lt_of_not_le fun h => by
    cases Nat.le_antisymm hk h
    exact hk' (.refl _)
  refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
  intro i hi hki
  suffices ¬ Descendant n i from
    get_heapifyDown_not_descendant lt x n i this
  intro hni
  exact hk' <| Descendant.ascend_right hk hni hki
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
⊢ IsHeap lt (heapifyDown lt x n) k
no goals