. show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
  clear x; intro n x IH k hk
  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
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
no goals