have : n < k := Nat.lt_of_not_le fun h => by
  cases Nat.le_antisymm hk h
  exact hk' (.refl _)
α : 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
hk' : ¬Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) k
α : 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
hk' : ¬Descendant n k
this : n < k
⊢ IsHeap lt (heapifyDown lt x n) k